System modelling
Contents
1. INIT a TRUE amp b in 0 2 4 TRANS next a a TRANS next b in case next a 10 2 4 5 I next a 11595 esac CTLSPEC AG a gt b in 10 2 4 INVARSOPEC ha gt D in 1 3 Indirect modelling e Behaviour of an automaton is defined by specifying initial and next values of state variables e Example ASSIGN init a TRUE next a a Ine Bb 10 254 425 next b case next a Ly xd Inext a 1 3 esac e Operator init defines the initial value of a variable Operator next defines the value of a variable in the next state Indirect modelling e f the initial value of a variable is not given it will get any value from its range of values There exists at least 1 initial state e f the next value of a variable is not given it will get any value from its range of values There exists at least 1 next state for every state Remark e Every model defined indirectly can be defined directly e Not every model defined directly can be defined indirectly Direct modelling Behaviour of an automaton is defined by logic expressions Logic expressions express initial states reachable states e transitions between states Results of lack of expressions or of their mutual contradiction e an empty set of initial states unreachable states e lack of reachable states 10 Direct modelling e Specification of initial values of variables INIT logic expression e2. The expression given after INIT describes initial values of variables e Example of specification of values of variables a and b INIT a TRUE amp b in 0 2 4 e f the initial value of a variable is not given it will get any value from its range of values e f an untrue expression is given then there are no initial states model verification may be incorrect e Using the operator next is not allowed 11 Direct modelling e Specification of reachable states by state invariants INVAR logic expression e The expression given after INVAR describes the values of variables that characterise every state e Example of specification of values of variables a and b INVAR a TRUE a FALSE INVAR la gt b in 11 3 e f an untrue expression is given then there are no reachable states model verification may be incorrect e Invariant definitions are not mandatory e Using the operator next is not allowed 12 Direct modelling e Specification of allowed transitions between states TRANS logic expression e The expression given after TRANS describes allowed values of variables in the next state e Example of specification of next values of variables a and b TRANS next a a TRANS next b in case next a 0 2 4 Inext a 1 3 esac e If an untrue expression is given then there may be no next state model verification may be incorrect 13 Direct modelling e INVAR or INIT combined with TRAN
3. module Check Anvar p invariane IN module 48 Model simulation e Choose an initial state randomly Pick Stare f e Choose an initial state from the list of available states Puck Xu ees euh 49 Model simulation e Make a simulation from a chosen state sSxm late P pl vwv I r u k number of states e show changed state variables p e Show all state variables V e randomly choose from available states r e manually choose from available states i e give length of path of states e g 4 k 4 The simulation consists of 10 state paths by default e Examples simulate p r ek 5 simulate v i 50 Model simulation A chosen path of states analysis e Paths of states are created in result of a negative verification of a formula and in result of a simulation e Show generated paths al show traces v a achosenone show traces v path number e a chosen one with states from to Show Eraces ev path number tfromn State number to state number Show a number of generated paths Show traces L 51 Model simulation A chosen path of states analysis e Go to a chosen state of a chosen path goto State pali numDer state number Show description of the current state of the current path prine OQUIIONU stare 52 Restart and end of work Restart of work reset of adjustments reset e End of work reset of adjustments Gul 53 Execu
4. Information Systems Analysis Temporal Logic and Timed Automata 8 System model verification in NUSMV Pawet Gluchowski Wroctaw University of Technology version 2 3 System modelling e Indirect modelling Direct modelling FAIRNESS constraints e Synchronous and asynchronous model of a system e Nondeterminism Example aircraft intruder model Mistakes in system modelling e Different definitions of a variable e Recursive definition of a variable Mutual dependency of variables Contradictions in expressions INIT INVAR and TRANS System verification e Possibilities Property kinds to verify e Counting a minimal and maximal path of states e Example for the aircraft intruder model Interactive work e Initial operations e Model verification Model simulation Restart and end of work e Executions of a script with operations Description of operations performed by Nus System modelling Indirect modelling e Direct modelling FAIRNESS constraints e Synchronous and asynchronous model of Nondeterminism Example aircraft intrud Indirect modelling MODULE main VAR a boolean D 2 04 ASSIGN init a TRUE next a a inNIC b r 10 274 13 next b case next a eee Ep Le Ca Lod esac CILSPEC AG a gt b in 10 2 4 INVARSPEC la gt b an L 3 Direct modelling MODULE main VAR a boolean D Dus
5. S e 1st way invariantly a 1 INVAR a 1 e 2nd way in the initial and every following state a 1 INIT a l TRANS next a 1 The effect seems to be the same but the 1st way is more effective n this situation it is recommended to use an invariant 14 FAIRNESS constraints e Constraint JUSTICE expression e Alternatively FAIRNESS expression e Model verification consists of these paths only where the expression is true infinitely many times e g VAR a boolean JUSTICE La e t corresponds to the formula AG AF a e Using the operator next in the expression is not allowed 15 FAIRNESS constraints e Constraint COMPASSION expressioni expression2 Model verification consists of these paths only where if the expression is true infinitely many times then the expression 2 is also true infinitely many times on the same paths e g VAR a boolean b boolean COMPASSION a b e t corresponds to the formula AG AG AF a gt AG AF b e Using the operator next in the expressions is not allowed e NuSMV does not fully support the COMPASSION yet 16 system modelling Synchronous and asynchronous model of a system e In the synchronous model in one step e a change of state of every module takes place in parallel asimultaneous change of values of variables according to the specification in every module e In the asynchronous model in one st
6. alues of variables in the same state cannot be mutually dependent e Wrong a btl D t asl e wrong nextia 1 nexL09 next b next a e But values of variables in different states may be mutually dependent e good next a se bi next b a e good Hext a 3e next bjj next b ay 33 Contradictions in expressions INIT INVAR and TRANS If an untrue expression INIT is given then there are no initial states If an untrue expression INVAR is given then there are no reachable states If an untrue expression TRANS is given then there may not be a next state These mistakes are reported by NuSMV These mistakes may lead to an incorrect model verification 34 system verification Possibilities e Property kinds to verify Counting a minimal and maximal path of Example for the aircraft intruder m system verification Possibilities e Verification is automatic e Specification of a system is given by temporal logic formulas e Available logics LTL CTL LTL RTCTL with upper and lower bounds for temporal operators and PSL e All well formed formulas are allowed Every formulas is verified independently of the others e Verification of a formula returns true or false e The false result is returned with a counterexample a path of states if it can be generated e Length of minimal and maximal path between two determined states can by counted 36 Property kin
7. chable states compute reachable e Show reachable states print reachable States y 44 Model verification e Show all properties show property e Add a property of a given kind to the verification add property kind p formula e Add the property to verification in the context of a given module add property Kind ep Lormuld IN module Kind c CTL formula 1 LTL formula s PSL formula i invariant q counting a path 45 Model verification e Verify a CTL specification of a given number check ctlspec n numoer Verify a given formula with a CTL specification Check cLLSpec p formuda Verify a given formula with a CTL specification in the context of a given module check CUlspec p formula IN module Similarly for LTL specification check 1tlspec 46 Model verification e Check possibility of a deadlock of the system check fsm e Count length of a path between given states for a given number of an expression Check compute n numoer e Count the minimal path between given states check Compute p MINIStatel state2 e Count the maximal path between given states in the context of a given module check compute P MAX stacel states IN module 47 Model verification e Verify an invariant of a given number check invar n number e Verify a given invariant check invar p invariant e Verify a given invariant in the context of a given
8. city after time 6 8 CTLSPEC EF vl amp movement accelerating gt EX vl CTLSPEC AG vl amp movement accelerating amp t 8 gt AX vl CTLSPEC AG vl amp movement accelerating amp t 6 gt AX v1 CTLSPEC AG vl amp movement accelerating amp t 6 amp t 8 gt EX vl correct CTLSPEC AG vl amp movement accelerating amp t gt 6 amp t 8 gt AX vl incorrect 40 Interactive work Initial operations Model verification Model simulation Restart and end of work Executions of a script with ope Description of operations perfo Initial operations The order of the operations is optimal e Start working with a smv file in the interactive mode NuSMV int file e Read the model of a system read model e Create modules and processes flatten hierarchy e Show a list of input variables and state variables optional show vars 42 Initial operations Show variables that are dependent on a given expression optional show dependencies e expession Create variables to compile the model into BDD binary decision diagrams encode variables Write the order of variables to a file optional write order Compile the model into BDD build model 43 Initial operations e Initialise the system ready to be verified go e Read and compile the model into BDD verify the model and count a set of reachable states Process model e Count a set of rea
9. ds to verify Properties described in LTL logic dealing with linear time bis PEC LTL formula e Properties described in CTL logic dealing with branching time CPBOEEBCG CEL LOrmula e Properties described in logics LTL PSL RTCTL e Invariants dealing with every state of the model INVARSPEC JOUIC Expression 37 Counting a minimal and maximal path of states Expression COMPUTE counts length of a path number of states between two specified states Specification of a state is a logic expression expressing values of selected state variables in this state Counting the minimal path COMPUTE MIN statel state2 Counting the maximal path COMPUTE MAX statel stateZ2 The result is a number of states or INFINITY 38 Example for the aircraft intruder model Verification of correct behaviour of the clock Incrementation of the clock with every state change mod 10 CTLSPEC AG t 0 gt AX t 1 CTLSPEC AG t 9 AX t 0 COMPUTE MIN t 0 t 1 should be 1 COMPUTE MAX t 0 t 1 should be 1 Change of a kind of movement of the aircraft resets the clock e g change from decelerating to standing CTLSPEC AG movement decelerating amp AX movement standing gt AX t 0 CTLSPEC AG movement decelerating amp AX movement standing amp t 0 AX t 0 39 Example for the aircraft intruder model Verification of behaviour of the velocity V1 Accelerating aircraft reaches the vl velo
10. ep e a change of state of one module process takes place achange of values of variables according to the specification in one module e Sequence of processes is random e Variables of other processes remain unchanged in this step e Processes are nod used now they are deprecatea 17 Nondeterminism e Definition of a variable requires to give a set of its values e g VAR a DU D dsl SZ SI e If no instruction assigns any value to a variable then the variable gets a random value of the range of its values e f an instruction assigns a subset of a variable s set of values to the variable then the variable gets a random value of this subset e g a sl s3 18 system modelling Example aircraft intruder model Description of the situation A runway intersects a taxiway An aircraft begins moving before the intersection accelerating The aircraft accelerating reaches the V1 velocity after time 6 8 and then takes off after time 1 3 The take off of the aircraft may happen before on or after the intersection An intruder may appear on the intersection at any moment The intruder when appears on the intersection does not disappear from it If the aircraft accelerates before on or after the intersection where the intruder appears it decelerate if its velocity V1 Decelerating aircraft stops after time 3 4 before on or after the intersection If the aircra
11. ft and the intruder are on the intersection a collision may happen Final states the aircraft takes off the aircraft stands there is a collision m MODULE main VAR location of the aircraft i1n relation toO the intersection location before on after kind of a movement of the aircraft movement accelerating decelerating standing taking off time of the movement reset to zero at the moment of the beginning of a new movement kind DD intruder on the intersection intruder boolean collision with the antruder collision boolean aircraft s velocity gt vl deceleration is forbidden vl boolean 20 LNITLAL STATE INIT the aircraft is before the intersection location before amp the aircraft is accelerating movement accelerating amp the time of acceleration begins t 0 amp here is no intruder on the intersection intruder FALSE amp there is no collision collision FALSE amp the aircraft s velocity vl vl FALSE 21 BEHAVIODUR OF THE CLOCK TRANS next t in case resetting the clock when taking off starts movement accelerating amp next movement taking off 0 resetting the clock when decelerating start movement accelerating amp next movement decelerating 0 resetting the clock when standing starts movement decelerating amp next movement standing 0 in other case with any automat
12. on state change one time unit passes TRUE t 1 mod 10 esac 22 BEHAVIOUR Or THE INTRUDER TRANS next intruder in case the intruder may appear at any moment intruder FALSE TRUE the intruder cannot disappear from the intersection if it already is there TRUE intruder esac 23 BEHAVIOUR OF THE vl VELOCITY TRANS next vl in case the vl cannot be reached in the time t lt 6 Ivl amp movement accelerating amp t 6 FALSE the vl may be reached in the time t lt 8 Ivl amp movement accelerating amp t 8 TRUE FALSE the vl is reached at most in the time t 8 Ivi amp movement accelerating amp t 8 TRUE once reached the vl velocity does not get smaller TRUE vl esac 24 BEHAVIOUR OF THE COLLICION the collision is impossible if there is no intruder or the aircraft is before the intersection INVAR intruder location before gt collision TRANS next collision in case if there is the collision it will not pass away collision TRUE if there is no collision it is possible then if the intruder and the aircraft are on the intersection intruder amp location on FALSE TRUE other states do not affect the collision TRUE collision esac 25 BEHAVIOUR OF THE LOCATION OF THE AIRCRAFT TRANS next location in case the standing or taking off aircraft does not change its location final state movement s
13. section movement accelerating amp vl amp intruder decelerating 28 BEHAVIOUR OF THE MOVEMENT OF THE AIRCRAFT 3 the decelerating aircraft cannot stop in the time t lt 3 movement decelerating amp t lt 3 decelerating the decelerating aircraft may stop in the time t lt 4 movement decelerating amp t lt 4 decelerating standing the decelerating aircraft will stop at last in the time t 4 movement decelerating amp t 4 standing the standing or taking off aircraft does not change its kind of movement movement standing movement taking off movement other states do not affect the movement TRUE movement esac 29 Mistakes in system modelling e Different definitions of a variable Recursive definition of a variable e Mutual dependency of variables Contradictions in expressions INIT INVAR Different definitions of a variable e Every variable should have one definition only that defines its value for a given state e Wrong init a TRUE init a FALSE e Wrong b a D lt ofl e wrong init c a C t D e good init a TRUE FALSE 31 Recursive definition of a variable e Value of a variable cannot depend on its value from the same state e Wrong ge atl e Wrong next a next a 1 e But it may depend on its value from the next state e good next a atl 32 Mutual dependency of variables e V
14. tanding movement taking off location the aircraft being before the intersection may enter it location before before on the aircraft being on the intersection may leave it location on on after the aircraft being after the intersection does not change cents JXIOCSBtrob location after after esac 26 BEHAVIOUR OF THE MOVEMENT OF THE AIRCRAFT 1 TRANS next movement in case the aircraft accelerating with the velocity gt vl cannot take off if there is the collision no change of movement kind movement accelerating amp vl amp collision accelerating the aircraft accelerating with the velocity gt vl cannot take off in time t 1 movement accelerating amp vl amp t 1 accelerating the aircraft accelerating with the velocity gt vl may take off in time t 3 if there is no collision movement accelerating amp vl amp t lt 3 accelerating taking off 27 BEHAVIOUR OF THE MOVEMENT OF THE AIRCRAFT 2 the aircraft accelerating with the velocity gt vl takes off at last in the time t 3 if there is no collision movement accelerating amp vl amp t 3 taking off the aircraft accelerating with the velocity vl still accelerates if there is no intruder movement accelerating amp vl amp intruder accelerating the aircraft accelerating with the velocity lt vl decelerates if there is the intruder on the inter
15. tions of a script with operations e Automatically make a given sequence of operations from a file NuSMV source file e f an error occurs further operations cannot be executed Description of operations performed by NuSMV e Set verbosity of operations performed by NuSMV NuSMV v N int file N level of verbosity from 0 nothing to 4 54 Literature e K L McMillan The SMV system 2001 A Cimatti et al NUSMV a new symbolic model checker e R Cavada et al NuSMV 2 5 User Manual 2010 e R Cavada et al NuSMV 2 5 Tutorial
Download Pdf Manuals
Related Search