Acknowledgements

Dr. Hariharan Ramasangu of MSRSAS, Bangalore college is highly acknowledged for providing help in solving this assignment.This solution was done as part of solving the assignment of CSN2505 (Applied Formal Methods) module of the course MSc[Engg.] in Computer Science and Networking branch in M S Ramaiah School of Advanced Studies under Coventry University,United Kingdom.

Introduction

In this part the implementation of composite web service is done using a tool called NuSMV. Here the formal specifications that are mentioned in previous post are expressed in symbolic language using LTL and CTL. NuSMV is a software tool for formal verifications of finite state systems against the specifications in LTL and CTL.

Model development in SMV language

To verify the specifications and model NUSMV tool needs the specifications and the code written in .smv format. The syntax of a NUSMV program is:

program :: module_list

module_list ::

module

| module_list module

There must be one module with the name main and no formal parameters. The module main is the one evaluated by the interpreter. As other programs the smv code also has a main function to start with.Here the term mudule is used which is same a functions in C

MODULE main

VAR

state : { Na,Re,Su,Ac,Pr,Do,En};

After the main module declaration the variable declaration is done. The statement VAR denotes the variable declaration in the smv language. The statement

VAR state : { Na,Re,Su,Ac,Pr,Do,En};

Declares the variable state as well as the symbolic constants Na,Re,Su,Ac,Pr,Do,En. Here the symbols represents the following states that is mentioned in PartB. Na = Not activated, Re= Received, Su = Suspended ,Ac= Active, Pr = Process, Do = Done, En = End state.

ASSIGN

init(state) := Na;

next(state) :=

case

          (state = Na ):{Re,En};

          (state = Re): {Su,Ac,Pr};

          (state = Su): {Re,Ac,Na};

          (state = Ac):  {Ac,Pr};

          (state = Pr): {Do};

          (state = Do): {En};

          (state = En): {Na};

          TRUE:state;

esac;

The above statement is the assignment statement.in NuSMV it is termed as ASSIGN constraint. An assignment has the form:

assign_constraint :: ASSIGN assign_list

assign_list :: assign ;

| assign_list assign ;

assign ::

complex_identifier := simple_expr

| init ( complex_identifier ) := simple_expr

| next ( complex_identifier ) := next_expr

On the left hand side of the assignment, identifier denotes the current value of a variable, init(state) denotes the initial value and in the code it is assigned to Na state i.e. the not activated state, and next (state) denotes its state in the next state. In the code to assign the next (state) the case expression is used which is another way of the if –then else expression. A case expression has the following syntax:

case_expr :: case case_body      

case_body :: basic_expr : basic_expr ;

| case_body basic_expr : basic_expr ;

A case expr returns the value of the first expression on the right hand side of ‘:’, such that the corresponding condition on the left hand side evaluates to TRUE. For example, the in the expression

next(state):=

case

          (state = Na ):{Re,En};

esac;

means if state = Na is true then the next state can be Re or En. With this the model is formed . Now to verify the specifications LTLSPEC or CTLSPEC keywords are used. LTL specifications are introduced by the keyword LTLSPEC. The syntax of this specification is: LTLSPEC ltl_expr [;].

For example: LTLSPEC ((state=Na) -> X(state=Re | state = En));

The section 3.2 describes the specifications used for verification.

The syntax of LTL formulas recognized by NUSMV is as follows: as per [16]

 

Similarly to build CTL specifications CTLSPEC keyword is used. The syntax of this

specification is: CTLSPEC ctl_expr [;]

For example :

CTLSPEC AG((state=Re -> AX(state=Ac|state=Pr|state=Su|state=Do)));

The syntax of CTL formulas recognized by NUSMV is as follows: as per [16]

 

Development of LTL and CTL specifications

The properties to be checked are extracted from the control behaviour based on the control behaviour states are shown in section 2.5 and their associated LTL

and CTL properties defined in section 2.5 are defined in this section using LTL and CTL methods, and then the specification are converted to LTL and CTL specification of smv code. In the following, LTL and CTL formulae are represented using known symbols and operators as summarized below:

FФ: sometimes in the Future, Ф is true in some future moment.

ФUΨ: Until, Ф is true until Ψ is true.

GФ: Globally in the future, Ф is true in all future moment.

XФ: neXt time, Ф is true in the next moment in time. As CTL permits only branching-time operators, each of the LTL operators defined above (G;F;X, and U) must be immediately preceded by a path quantifier (i.e., A for All paths, and ϵ for Existing a path). The following initials are used to specify the control behavior states when defining the logical properties to

be checked: (1) Na: Not Activated, (2) Re: Received, (3) Ac: Activated, (4) Su: Suspended, (5) Pr: Process, (6) Do: Done, and (7) En: End. Let → be the logical implication. So considering all the above conditions the LTL and CTL specifications for the specifications mentioned in section 2.5 are as follows.

LTL Specifications:

1. Ф = G(Na → X(Re|En)) – There exists always a received state or an end state after not activate state.
2. Ф = G(Re→XF(Ac ∨ Pr ∨ Su ∨ Do))- There is always a activated,processed,suspended, or done state after received state.
3. Ф = (Su→XF(Na ∧ En)) -There is a not activated and end state in future after a suspended state.
4. Ф = G(Do→XF(En)) – There is always an end state in future after done state.
5. Ф = G(En→X(Na)) – There is always a not activated state after end state.
6. Ф = (Ac → X(Pr ∨ Su))- There is a process or suspended state after activated state.
7. Ф =((Re ∨ Pr) →X(Do∨ Su))- There is a done or suspended state in a path after received or processed state

CTL Specifications:

1. Ф = AG(Re →AXAF(Ac ∨ Pr ∨ Su ∨ Do))- There is always a path from state received to state activated or processed or suspended or done.
2. Ф = AG((Do → AXAF(En)) – There is always a path to end state from done state.
3. Ф = AG(Na → AXAF(Re ∨ En)) – there is always a path to receive state or end state from not activated state.
4. Ф = AG ((Re → EX(Su)) ∨ (Re→EX(Pr))) – A path from received to next state suspended or from received to next state processed is always potentially reachable.

Model checking using NuSMV

The specifications written in LTL and CTL as mentioned in section 3.2 has to be converted to the respective LTL and CTL specifications using SMV language syntax. So the following specifications has been deduced from section 3.2 using NuSMV syntax.

1. LTLSPEC G((state=Na) -> X(state=Re | state = En)); is the statement in NuSMV for Ф = (Na → X(Re|En))
2. LTLSPEC G((state=Re -> X(state=Ac|state=Pr|state=Su|state=Do))); is the statement in NuSMV for Ф = G(Re→XF(Ac ∨ Pr ∨ Su ∨ Do))
3. LTLSPEC ((state=Su) -> X(state= Na&state=En)); is the statement in NuSMV for Ф = (Su→XF(Na ∧ En))
4. LTLSPEC G((state=Do) -> X(state=En)); is the statement in NuSMV for Ф = G(Do→XF(En))
5. LTLSPEC G((state=En) -> X(state=Na)); is the statement in NuSMV for Ф = G(En→X(Na))
6. LTLSPEC ((state=Ac) -> X(state=Pr|state=Su)); is the statement in NuSMV for Ф = (Ac → X(Pr ∨ Su))
7. LTLSPEC (((state=Re|state=Pr)-> X(state=Do|state=Su))); is the statement in NuSMV for Ф =((Re ∨ Pr) →X(Do∨ Su))
8. CTLSPEC AG((state=Re -> AX(state=Ac|state=Pr|state=Su|state=Do))); is the statement in NuSMV for Ф = AG(Re →AXAF(Ac ∨ Pr ∨ Su ∨ Do))
9. CTLSPEC AG((state=Do) -> AX(state=En)); is the statement in NuSMV for Ф = AG((Do → AXAF(En))
10. CTLSPEC AG(state=Na -> AX(state = Re |state = En)); is the statement in NuSMV for Ф = AG(Na → AXAF(Re ∨ En))
11. CTLSPEC AG((state = Re -> EX state = Su)|(state = Re -> EX state = Pr)); is the statement in NuSMV for Ф = AG ((Re → EX(Su)) ∨ (Re→EX(Pr)))

Combining the methods as described in section 3.1 to section 3.3 the smv code is generated to check the model and to verify its specifications. The complete code is in Apendix section. The file is then saved in .smv format. Here the file is named as compwebserv.smv. Then to run this file the following commands needs to be executed in the NuSMV command terminal.

1. Nusmv> read_model –i compwebserv.smv

Reads a NuSMV file into NuSMV. If the -i option is not specified, it reads from the file specified in the environment variable input_file. The –I option Sets the environment variable compwebserv.smv  to model-file, and reads the model from the specified file.if there isn’t any syntax error then the NuSmv will read the code and go to the next line to accept further command else it will pop out errors with the line number where the error is there.

2. Nusmv> flatten_hierarchy

It flattens the hierarchy of modules which means it is responsible for the instantiation of modules and processes. The instantiation is performed by substituting the actual parameters for the formal parameters, and then by prefixing the result via the instance name.If there isn’t any error in the code it will flatten the hierarchy else it will show the error line number with error description.

 

3. Nusmv> encode_variables

 

This command builds the BDD variables necessary to compile the model into BDD. It generates the boolean BDD variables and the ADD, needed to encode propositionally the (symbolic) variables declared in the model.The variables are created as default in the order in which they appear in a depth first traversal of the hierarchy.

4. Nusmv> build_model

 

This command compiles the flattened hierarchy into BDD.

5. NuSmv> check_ltlspec (to check the ltl spec)

6.Nusmv> check_ctlspec (to check the ctl spec)

Analysis using NuSMV

The command check_ltlspec is used to check the LTL specifications mentioned in the smv code. This command performs model checking of LTL formulas. If the specifications are true it will list out the specifications are true if there is any error in the specifications i.e. any of the specification is false then the tool will mention that the specification is false and will also give you the example in what way the specification is false.

 

Simillairly check_ctlspec command is used to check the ctl specifications mentioned in the smv code. This command performs fair CTL model checking.If all the ctl spec mentioned in the snv file are true then it says that the specifications are true and if it is false then it displays that the specification is false and also gives a counter example showing how the specification is false.

 

The specifications are nothing but the test cases to verify the design.Here it ran all specification to true which says that design is true.But this doesnot say whether we can really depend on this to confirm the validity of the design.So to check this lets write a wrong specification and see if it gives error or not. So this is discussed in next section.

Influence of modified specifications on verifications

For this modify some specification of the smv code of this model to check whether the tool finds the error or not. Let the spec LTLSPEC G((state=Na) -> X(state=Re | state = En)); which says that – There exists always a received state or an end state after not activate state be modified to Always there exists a received state  after not activate state. So the modified LTLSPEC would be LTLSPEC G((state=Na) -> X(state=Re )); So lets see what the NuSMV tools says.

 

The tool clearly says that the specification is false and not only it states it is false ,it also gives the counter example stating that how the specification is false. This says that the tool and formal verification can be used for the verification of design.

Conclusion

As the world getting more and more automatized and the spree to connect the world increases ,the need to use the internet and web services to help the user to connect remotely increases. And for this security is a major concern and so there cannot be any loop holes in the design and in this assignment we had provided a noble way to verify the model which is very robust than the manual testing.

 

Click : Developing a formal model  of a composite web service system

Complete NuSmv code for the above system

 References

[1] Alicendra,C.et al.,”Formalization and Validation of Safety-Critical Requirements”,Creative Common Arts.

[2] Antti,J.,et al.,(1998)”Verification of Safety-Critical Systems: A Case Study Report on Using Modern Model Checking Tools”,1998,Dagasthul,Germany.

[3] Brown,D.,et al.,(2010)”Guidance for Using Formal Methods in a Certification Context”,May 2010.

[4] Decision and Information Analysis, Goizueta Business School(2001),”Model Checking – A Rigorous and Efficient Tool for E-Commerce Internal Control and Assurance”,17 September 2001,W.Wang,et al.

[5] Department of Computing, Imperial College London (2003),”Model-based Verification of Web Service Compositions”,2003,F.Howard,et al.

[6] Department of Computing, University of Surrey, Guildford, UK (2007),”An Automatic Test Case Generation Framework for Web Services”,3 september 2007,Z.Yongyan,Z.Jiong,K.Paul.

[7] Georgia, M.K.,et al.(2009)”Model-driven development of composite context-aware web applications”,27 March 2009,Software and Service Engineering Laboratory, Technological Education Institute of Piraeus, Dept. of Electronic Computing Systems, Petrou Ralli & Thivon 250, 12244 Athens, Greece

[8] Hoyt, L.,(2012)”Transitioning to RTCA DO-178C/DO-278A:A Business Manager Brief”,August 2012,Foliage

[9] Huth,M.,Ryan,M.,(2004)”LOGIC IN COMPUTER SCIENCE”,Second Edition,2004,Cambridge University Press

[10] Jamal,B.et al.,(2013)”Symbolic model checking composite Web services using operational and control behaviors”,2013,Concordia University.

[11] Laurent,P.et al.,”DO-178C/ED-12C versus DO-178B/ED-12B Changes and Improvements”,September 2012,ACG Solutions.

[12] Maddireddy,S.R.,”The Impact of RTCA DO-178C on Software Development”,Cognizant

[13] Melissa,K.(2009)”A formal verification approach of conversations in composite web”,August 2009,Concordia University

[14] NASA Ames Research Center, Moffett Field, CA 94035, USA (2010),”Linear Temporal Logic Symbolic Model Checking”,29 June 2010,Y.R.Kristin.

[15] Raman,K.,et al.(2006)”Verification and Validation of Web Service Compositions “,27 June  2006,DIT, University of Trento, Italy.

[16]Roberto,C. et al.“NuSMV 2.5 Tutorial”, First Edition, FBK publisher

[17] School of Computing,University of Utah ,”Model Checking Web Services”,Shrigondekar,Amit.,De Silva,L.,Thulasinathan,A.

[18] Stephen A.J.,”Certification of Safety-Critical Software Under DO-178C and DO-278A”,NASA Ames Research Center, Moffett Field, CA, 94035

[19] Wlad,J.,(2012)”Architectural Trends in Avionics Systems: Multi-core and DO-178C”,April 2012,Aerospace and Defense FAA DER Systems and Software.

[20] Xian,F.(2004)”Formal Specification and Verification of Asynchronously Communicating Web Services”,September 2004,UNIVERSITY of CALIFORNIA.

[21]Yanick,M. et al.(2013) “Testing or Formal Verification: DO-178C Alternatives

and Industrial Experience”,2013,IEEE computer society

[22] Zoltan,T.H.(2007)”Model Checking – A Rigorous and Efficient Tool for Preventing E-business Failures”,August 2007,THE UNIVERSITY OF TEXAS AT AUSTIN

[23] 21st International Joint Conference on Artificial Intelligence (IJCAI)(2009),”Behavioral Description Based Web Service Composition Using Abstraction and refinement”,2009,H.Kil,et al.