Home

NuSMV 2.1 User Manual

1. 00 0 38 print sage tia Boe Ae GNOME ae a 56 process modelis i denies to oe aaa 37 UG cla e ie hallo ione A ate dd 56 read Modelo js e s sais cala nes Magn ae ok 34 TOSOG ried cos o ae cbs Ge week albus Pave ieee eased 56 SCI ede Gere atid DE Ladies LA 56 set_bdd_parameters 00 53 SHOWLtTACESs 3 resti Oy oe hic dra 48 Show varsih sii sol deed tn cbse ae oleae cee 34 SIMULA esr eee re wa dealers Ra lated a ia orn aaia ak 49 SOULRCC A E ee ea 58 UMS rta a oa BOs tee el se 59 UDALLAS s isa ini a Ds ee SS 59 O ha neds oo alia 59 USAge Seca dis ok Tye te tine tea hia ata A artes Sues eet 59 WHICH ae asad oes han Ades E Be ee hE 59 write ordera t ohea Seed Fe he a 35 Variable Index Variable Index A affinityo oo Ay Ss bh ihe Ae lia ne 36 ag only search io ili lio lisi aut 39 AULOCXEC ni e n 60 B bmc_dimacs_filename 46 bmc_invar_dimacs_filename 47 bmcwlengthy seira a deed dh ee 46 BIG L OOPDACK tici sa he adits ia 46 C check trans iaa bela 38 conj_part_threshold 000 0 36 E H historyechari i 208054214 a A 60 I image_cluster_size image_W 1 2 3 4 36 image_verbosity 000 37 inp t fileren entote eine Bae dis da de 34 67 input order file lu oil 35 iwls95preorder 00000 36 NuSMV_LIBRARY_ PATH ol oa ana dean ete dea as 60 61 nusmvastdert rbt ale i
2. 0oooooooomooo 50 LOTO UC init pu e a a cals 1 INVAR declaration ooooooocoooocccroccc ooo 25 ISA declarations Li 26 IVAR creare beh eee tele el See am ate i 24 Justice CONStraints 27 2 fe chee ds 29 L LTL model checking i 13 LTL Specifications LL 30 M main MOAUle ce adh ALL 28 master o ssi i 61 model compiling LL 34 model parida rei 34 model reading lire i eee EA 34 MODULE declarations 0s eee eee eee 26 Index N next expressions 00 0 cece eee eee eee 22 O OPINAS Gite LA oe ide Bie et 61 P process keyword ier ua sree oa ea 29 PLOCESSES tai ica 29 R Real Time CTL Specifications and Computations S 69 A iaia 28 set eXPIessiOOS 0oooocococcocrcocr eee eee eee 22 Shell configuration Variables 60 simple expressionS 0 00 cece cence neces 21 Simulation eee ot ies tada i eth ia 6 Simulation Commands 0 00 ee eee 48 state variables syntax 0 000000 23 BMG et ee hl abe e e pd dl e 21 alr COMP SOLE ttt lie lashed seein fy aie 35 Traces Inspection Commands 50 TRANS declarations 0 0 0 e eee eee ee 25 Tutorials cnt ed fore Se i eek ia 2 type declarations iia reas Halt 23 type specifiers riisu e iaie iera eee cee een eee 23 V VAR declaration 5 isane misie cianat ia na ie ei 23
3. 0 TRANS case y 7 next y 0 1 next y y 1 mod 16 esac This slightly artificial model has only the state variable y ranging from 0 to 15 The values of y are limited by the transition relation to the 0 7 interval The counter starts from 0 deterministically increments by one the value of y at each transition up to 7 and then restarts from zero We would like to check with BMC the LTL specification G y 4 gt X y 6 expressing that each time the counter value is 4 the next counter value will be 6 This specification is obviously false and our first step is to use NuSMV BMC to demonstrate its falsity To this purpose we add the following specification to file modulo8 smv LTLSPEC G y 4 gt X y 6 and we instruct NuSMV to run in BMC by using command line option bmc eo prompt gt NuSMV bmc modulo8 smv no arte found with bound 0 for specification G y 4 gt X y 6 no li found with bound 1 for no counterexample found with bound 2 for no counterexample found with bound 3 for no counterexample found with bound 4 for specification G y 4 gt X y 6 is Taipe as demonstrated by the following execution sequence State 1 1 y 0 State 1 2 y 1 State 1 3 y 2 State 1 4 y 3 State 1 5 y 4 State 1 6 y 5 system_prompt gt NuSMV has found that the specification is false and is showing us a counterexample i e a trace where the value of y become
4. m Pipes the output generated by the program in processing INVARSPECs to the program specified by the PAGER shell variable if defined else through the UNIX command more o output file Writes the output generated by the command in processing INVARSPECs to the file output file p invar expr IN context The command line specified invariant formula to be verified context is the module instance name which the variables in invar expr must be evaluated in check_ltlspec Performs LTL model checking Command check_ltlspec h m o output file n number p ltl expr IN context Performs model checking of LTL formulas LTL model checking is reduced to CTL model checking as described in the paper by CGH97 A 1t1 expr to be checked can be specified at command line using option p Alternatively option n can be used for checking a particular formula in the property database If neither n nor p are used all the LILSPEC formulas in the database are checked Command options Chapter 4 Running NuSMV interactively 40 m Pipes the output generated by the command in processing LTLSPECs to the program specified by the PAGER shell variable if defined else through the Unix command more o output file Writes the output generated by the command in processing LTLSPECs to the file output file p 1tl expr IN context An LTL formula to be checked context is the module instance name which the variables in 1tl_expr must b
5. simple_expr simple_expr simple_expr simple_expr esac A case_simple_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 1 Thus if simple_expr on the left side is true then the result is the corresponding simple_expr on the right side If none of the expressions on the left hand side evaluates to 1 the result of the case_expression is the numeric value 1 It is an error for any expression on the left hand side to return a value other than the truth values 0 or 1 3 1 1 2 Set Expressions A set expression has the following syntax set_expr set_elem set_elem set definition simple_expr in simple_expr set inclusion test simple_expr union simple_expr 33 set union set_elem simple_expr A set can be defined by enumerating its elements inside curly braces The inclusion operator in tests a value for membership in a set The union operator union takes the union of two sets If either argument is a number or a symbolic value instead of a set it is coerced to a singleton set 3 1 2 Next Expressions While simple expressions can represent sets of states next expressions relate current and next state variables to express transitions in the FSM The structure of next expressions is similar to the structure of simple expressions See Section 3 1 1 Simple Expressions p
6. a This is precisely analogous to accessing a component of a structured data type Note that an actual parameter of module a can identify another module instance b allowing a to access components of b as in the following example MODULE main VAR Chapter 3 Syntax 28 a foo b b bar a MODULE foo x DEFINE c x p x q MODULE bar x VAR p boolean q boolean Here the value of c is the logical or of p and q If a identifies an array the expression a b identifies element b of array a It is an error for the expression b to evaluate to a number outside the subscript bounds of array a or to a symbolic value It is possible to refer the name the current module has been instantiated to by using the self builtin identifier MODULE element above below token VAR Token boolean ASSIGN init Token token next Token token in DEFINE above token in Token grant out below grant out MODULE cell VAR e2 element self el 0 ei element el self 1 DEFINE el token in token in grant out grant in el grant out MODULE main VAR ci cell In this example the name the cell module has been instantiated to is passed to the sub module element In the main module declaring c1 to be an instance of module cell and defining above token in in module e2 really amounts to defining the symbol c1 token
7. m Method Compiles the flattened hierarchy into BDD initial states invariants and transition re lation using the method specified in the environment variable partition_method for building the transition relation Command options m Method Sets the environment variable partition_method to the value Method and then builds the transition relation Available methods are Monolithic Threshold and Iwls95CP f Forces model construction By default only one partition method is allowed This option allows to overcome this default and to build the transition relation with different partitioning methods partition_method Environment Variable The method to be used in building the transition relation and to compute images and preimages Possible values are e Monolithic No partitioning at all e Threshold Conjunctive partitioning with a simple threshold heuristic Assignments are collected in a single cluster until its size grows over the value specified in the variable conj_part_threshold It is possible default to use affinity clustering to improve model checking performance See affinity variable e Iwls95CP Conjunctive partitioning with clusters generated and ordered according to the heuristic described in RAP 95 Works in conjunction with the variables image_ cluster_size image_W1 image_W2 image_W3 image_W4 It is possible default to use affinity clustering to improve model checking performance See affinity variable
8. state busy DASS request 0 state ready SS Choose a state from the above 0 3 0 Chosen state is request 1 state ready NuSMV gt show_traces 3 HHHHHHHHHHHHHHHHHHH Trace number 3 HHT gt State 3 1 lt request 0 state ready gt State 3 2 lt request 1 The user can also specify some constraints to restrict the set of states from which the simulator will pick out Constraints can be set for both the pick_state command and the simulate command using option c For example the following command picks an initial state by defining a simple constraint NuSMV gt pick_state c request 1 i FoR ORK AVAILABLE FUTURE STATES RRR request 1 state ready There s only one future state Press Return to Proceed Chosen state is 0 Chapter 2 Tutorial 10 NuSMV gt quit system_prompt gt Note how the set of possible states to choose has being restricted in this case there is only one future state so the system will automatically pick it waiting for the user to press the key We remark that in the case of command simulate the constraints defined using option c are global for the actual trace to be generated in the sense that they are always included in every step of the simulation They are hence complementary to the constraints entered with the pick_state command or during an interactive simulation session when the number of future states to be displayed is too high since these are lo
9. 0 Case k 9 1 1 instead allows for a counter example k 9 1 1 0 gt 0 gt 0 gt 0 gt 0 gt 0 gt 0 gt 0 gt 0 gt o bound 0 1 2 3 4 5 6 T 8 9 y value 0 1 2 3 4 5 6 T 0 1 Chapter 2 Tutorial 19 In NuSMV it is possible to specify the loopback condition in four different ways The loop as a precise time point Use a natural number as the argument of option 1 The loop length Use a negative number as the argument of option 1 The negative number is the loop length and you can also imagine it as a precise time point loop relative to the path bound No loopback Use symbol X as the argument of option 1 In this case NuSMV will not find infinite counterexamples All possible loops Use symbol as the argument of option 1 In this case NuSMV will search counterexamples for paths with any possible loopback structure A counterexample with no loop will be also searched This is the default value for option 1 In the following example we look for a counter example of length 12 with a loop of length 8 system_prompt gt NuSMV int modulo8 smv NuSMV gt go_bmc NuSMV gt check_ltlspec_bmc_onepb k 12 1 7 specification G Fy 2 is false as demonstrated by the following execution sequence State 1 1 y 0 State 1 2 y 1 State 1 3 y 2 State 1 4 y 3 loop starts here State 1 5 y 4 State 1 6 y 5 State 1 7 y 6 State 1 8 y 7 State 1 9 y 0 State 1 10 y 1 Sta
10. 2 6 INVAR declarations 0 0000 cece cece eee eee 25 3 2 7 DEFINE declarations 0000 cece cece cece eens 25 IDO ESA declaratoria hoe he da det ete ss 26 3 2 9 MODULE declarations 00 0 cece cece cece eens 26 3 210 A heise et be te ee Be ate Jang 27 32 11 Themain module Liri et ek aa tea tee ea 28 3212 Processes lia Se ad HS PG ei 29 3 2 13 FAIRNESS declarations 0 00 0000 cece cece eee 29 3 3 Specifications n shi ts Ba ee li a ed an 29 3 3 1 CTL Specifications 0 0 30 3 3 2 LTL Specifications ee eee ee eee 30 3 3 3 Real Time CTL Specifications and Computations 31 4 Running NuSMV interactively 33 4 1 Model Reading and Building 0 00 00 34 4 2 Commands for Checking SpecificatioNS 00ooo oooooo 37 4 3 Commands for Bounded Model Checking Al 4 4 Simulation Commands 0 00 c ccc ence teens 48 4 5 Traces Inspection Commands 0 cece eee n eens 50 4 6 Interface to the DD Package 0 50 4 7 Administration Commands a aasan 0c cece eee ene eeee 54 4 8 Other Environment VariablesS o ooooooooomooo 60 5 Running NuSMV batch s ovssc c cms mm ue 61 Bibliography ss sivispii id ewe Sas 63 Appendix A Compatibility with CMU SMV 64 Command Ind 6x veh AA eee a 66 Variable Index os isc s conoce centies di 67 Chapter 1 Introduction 1 1 Intr
11. 8 y value 0 1 2 3 4 5 6 7 0 In general BMC can find two kinds of counterexamples depending on the property being analyzed For safety properties e g like the first one used in this tutorial a counterexample is a finite sequence of transitions through different states For liveness properties counterexamples are infinite but periodic sequences and can be represented in a bounded setting as a finite prefix followed by a loop i e a finite sequence of states ending with a loop back to some previous state So a counterexample which demonstrates the falsity of a liveness property as GF p cannot be a finite sequence of transitions It must contain a loop which makes the infinite sequence of transitions as well as we expected O O gt 0 gt 0 gt 0 gt 0 gt time 0 1 tsien 1 1 k 2 k 1 k k 1 Consider the above figure It represents an examples of a generic infinite counterexample with its two parts the prefix part times from 0 to 1 1 and the loop part indefinitely from 1 to k 1 Because the loop always jumps to a previous time it is called loopback The loopback condition requires that state k is identical to state 1 As a consequence state k 1 is forced to be equal to state 1 1 state k 2 to be equal to state 1 2 and so on A fine grained control of the length and of the loopback condition for the counter example can be specified by using command check_1tlspec_bmc_onepb in interactive mode see Sec tion 4 3 Com
12. In the following an atom may be any sequence of characters starting with a character in the set A Za z_ and followed by a possibly empty sequence of characters belonging to the set A Za z0 9_ A number is any sequence of digits A digit belongs to the set 0 9 All characters and case in a name are significant Whitespace characters are space SPACE tab TAB and newline RED Any string starting with two dashes and ending with a newline is a comment Any other tokens recognized by the parser are enclosed in quotes in the syntax expressions below Grammar productions enclosed in square brackets are optional 3 1 Expressions Expressions are constructed from variables constants and a collection of operators includ ing boolean connectives integer arithmetic operators case expressions and set expressions 3 1 1 Simple Expressions Simple expressions are expressions built only from current state variables Simple expres sions can be used to specify sets of states e g the initial set of states The syntax of simple expressions is as follows simple_expr atom a symbolic constant number 3 a numeric constant TRUE 3 The boolean constant 1 FALSE 3 The boolean constant 0 var_id 3 a variable identifier simple_expr 1 simple_expr 33 logical not simple_expr 4 simple_expr logical and simple_expr simple_expr logical or simple_expr xor simple_expr logical exclusive or
13. It is also possible to avoid default preordering of clusters see RAP 95 using iwls95preorder variable conj_part_threshold Environment Variable The limit of the size of clusters in conjunctive partitioning The default value is 0 BDD nodes affinity Environment Variable Enables affinity clustering heuristic described in MOONO00 possible values are 0 or 1 The default value is 1 image_cluster_size image_W1 1 2 3 4 Environment Variables The parameters to configure the behavior of the Jwis95CP partitioning algorithm image_ cluster_size is used as threshold value for the clusters The default value is 1000 BDD nodes The other parameters attribute different weights to the different factors in the algorithm The default values are 6 1 1 2 respectively For a detailed description please refer to RAP 95 iwls95preorder Environment Variable Enables cluster preordering following heuristic described in RAP 95 possible values are 0 or 1 The default value is 0 Preordering can be very slow Chapter 4 Running NuSMV interactively 37 image_verbosity Environment Variable Sets the verbosity for the image method Iwls95CP possible values are 0 or 1 The default value is 0 print_iwls95options Prints the Iwls95 Options Command print_iwls95options h This command prints out the configuration parameters of the IWLS95 clustering algo rithm i e image_verbosity image_cluster_size and image_W1 2 3 4 go Initializes the
14. a sequence of states corresponding to a possible execution of the model Traces are created by NuSMV when a formula is found to be false they are also generated by the simulation feature Section 4 4 Simulation Commands page 48 Each trace has a number and the states are numbered within the trace Trace n has states n 1 n 2 n 3 The trace inspection commands of NuSMV allow to navigate along the traces produced by NuSMV During the navigation there is a current state and the current trace is the trace the current state belongs to The commands are the following goto_state Goes to a given state of a trace Command goto_state h state Makes state the current state This command is used to navigate alongs traces produced by NuSMV During the navigation there is a current state and the current trace is the trace the current state belongs to print_current_state Prints out the current state Command print_current_state h v Prints the name of the current state if defined Command options y Prints the value of all the state variables of the current state 4 6 Interface to the DD Package NuSMV uses the state of the art BDD package CUDD Som98 Control over the BDD package can very important to tune the performance of the system In particular the order of variables is critical to control the memory and the time required by operations over BDDs Reordering methods can be activated to determine better variable order
15. as prefix of the number Any invalid combination of bound and loopback will be skipped during the generation and dumping process a negative number in 1 bmc_length In this case loopback is considered a value relative to maz_length Any invalid combination of bound and loopback will be skipped during the generation process the symbol X which means no loopback the symbol which means all possible loopback from zero to length 1 o filename filename is the name of dumped dimacs files If this options is not specified variable bmc_dimacs_filename will be considered The file name string may contain special symbols which will be macro expanded to form the real file name Possible symbols are F model name with path part f model name without path part Chapter 4 Running NuSMV interactively 45 k current problem bound l current loopback value n index of the currently processed formula in the properties database the character gen_Itlspec_bmc_onepb Dumps into one dimacs file the problem Command generated for the given LTL specification or for all LTL specifications if no formula is explicitly given Generation and dumping parameters are the problem bound and the loopback values gen_ltlspec_bmc_onepb h n idx p formula IN context k length 1 loopback o filename As the gen_itlspec bmc command but it generates and dumps only one problem given its bound and loopb
16. boolean components i e subformulas which evaluate to a value other than 0 or 1 It is also possible to specify invariants i e propositional formulas which must hold invari antly in the model The corresponding command is INVARSPEC with syntax checkinvar_declaration INVARSPEC simple_expr This statement corresponds to SPEC AG simple_expr but can be checked by a specialized algorithm during reachability analysis 3 3 2 LTL Specifications LTL specifications are introduced by the keyword LTLSPEC The syntax of this declaration ltlspec_declaration LTLSPEC ltl_expr where ltl_expr simple_expr 3 a simple boolean expression ltl_expr ltl_expr logical not ltl_expr amp 1tl_expr logical and ltl_expr 1tl_expr logical or ltl_expr xor ltl_expr logical exclusive or ltl_expr gt ltl_expr 33 logical implies ltl_expr lt gt ltl_expr logical equivalence FUTURE Chapter 3 Syntax 31 X ltl_expr next state G ltl_expr globally F ltl_expr finally ltl_expr U 1tl_expr until ltl_expr V ltl_expr releases 3 PAST Y ltl_expr previous state Z 1tl_expr 3 not previous state not H 1tl_expr historically 0 ltl_expr once ltl_expr S 1tl_expr since ltl_expr T ltl_expr triggered In NuSMV LTL specifications can be analyzed both by means of BDD based reasoning or by means
17. cannot be proved and it shows a state satisfying y in 0 12 that has a successor state not satisfying y in 0 12 This two steps sequence of assignments shows why the induction fails Note that NuSMV does not say the given formula is really false but only that it cannot be proven to be true using the inductive reasoning described previously If we try to prove the stronger invariant y in 0 7 we obtain system_prompt gt NuSMV bmc modelo8 smv invariant y in 0 7 is true system_prompt gt In this case NuSMV is able to prove that y in 0 7 is true As a consequence also the weaker invariant y in 0 12 is true even if NuSMV is not able to prove it in BMC mode On the other hand the returned counter example can be used to strengthen the invariant until NuSMV is able to prove it Now we check the false invariant y in 0 6 cannot prove the invariant y in 0 6 the induction fails as demonstrated by the following execution sequence State 1 1 y 6 State 1 2 y 7 NuSMV gt As for property y in 0 12 NuSMV returns a two steps sequence showing that the induction fails The difference is that in the former case state y 12 is NOT reachable while in the latter case the state y 6 can be reached Unfortunately enough the BMC based invariant checker is not able to distinguish these two cases Chapter 3 Syntax 21 3 Syntax We present now the complete syntax of the input language of NuSMV
18. default value is f_k k_1 1_n n dimacs check_invar_bmc Generates and solve the given invariant or all Command invariants if no formula is given check_invar_bmc h n idx p formula IN context o filename Command options n index index is the numeric index of a valid INVAR specification formula actually located in the properties database The validity of index value is checked out by the system p formula IN context Checks the formula specified on the command line context is the module instance name which the variables in formula must be evaluated in o filename filename is the name of the dumped dimacs file It may contain special symbols which will be macro expanded to form the real file name Possible symbols are F model name with path part f model name without path part n index of the currently processed formula in the properties database the character Chapter 4 Running NuSMV interactively 47 gen_invar_bmc Generates the given invariant or all invariants if no Command formula is given gen_invar_bmc h n idx p formula IN context o filename Command options n index index is the numeric index of a valid INVAR specification formula actually located in the properties database The validity of index value is checked out by the system p formula IN context Checks the formula specified on the command line context is the module instance name wh
19. file It may contain special symbols which will be macro expanded to form the real file name Possible symbols are F model name with path part f model name without path part k current problem bound Chapter 4 Running NuSMV interactively 43 l current loopback value n index of the currently processed formula in the properties database the character check_Itlspec_bmc_onepb Checks the given LTL specification or all Command LTL specifications if no formula is given Checking parameters are the single problem bound and the loopback values check_ltlspec_bmc_onepb h n idx p formula IN context k length 1 loopback o filename As command check_Itlspec_bmc but it produces only one single problem with fixed bound and loopback values with no iteration of the problem bound from zero to max length Command options n index index is the numeric index of a valid LTL specification formula actually located in the properties database The validity of index value is checked out by the system p formula IN context Checks the formula specified on the command line context is the module instance name which the variables in formula must be evaluated in k length length is the problem bound used when generating the single problem Only natural number are valid values for this option If no value is given the environment variable bmc_length is considered instead 1 loopback loopback
20. initial value and next atom denotes its value in the next state If the expression on the right hand side evaluates to an integer or symbolic constant the as signment simply means that the left hand side is equal to the right hand side On the other hand if the expression evaluates to a set then the assignment means that the left hand side is contained in that set It is an error if the value of the expression is not contained in the range of the variable on the left hand side In order for a program to be implementable there must be some order in which the assign ments can be executed such that no variable is assigned after its value is referenced This is not the case if there is a circular dependency among the assignments in any given process Hence Chapter 3 Syntax 25 such a condition is an error It is also an error for a variable to be assigned more than once at any given time More precisely it is an error if 1 the next or current value of a variable is assigned more than once in a given process or 2 the initial value of a variable is assigned more than once in the program or 3 the current value and the initial value of a variable are both assigned in the program or 4 the current value and the next value of a variable are both assigned in the program 3 2 4 TRANS declarations The transition relation R of the model is a set of current state next state pairs Whether or not a given pair is in this set is determi
21. negation of the input or to the current value of the output Thus in effect each gate can choose non deterministically whether or not to delay Using TRANS and INIT it is possible to specify inadmissible FSMs where the set of initial states is empty or the transition relation is not total This may result in logical absurdities 2 2 Simulation Simulation offers to the user the possibility of exploring the possible executions traces from now on of a NuSMV model In this way the user can get familiar with a model and can acquire confidence with its correctness before the actual verification of properties This section describes the basic features of simulation in NuSMV Further details on the simulation commands can be found in Section 4 4 Simulation Commands page 48 In order to achieve maximum flexibility and degrees of freedom in a simulation session NuSMV permits three different trace generation strategies deterministic random and interactive Each of them corresponds to a different way a state is picked from a set of possible choices In deterministic simulation mode the first state of a set whatever it is is chosen while in the random one the choice is performed nondeterministically In these two first modes traces are automatically generated by NuSMV the user obtains the whole of the trace in a time without control over the generation itself except for the simulation mode and the number of states entered via command line I
22. respect to a previous item Tf the num ber of possible states is too high then the user has to specify some further constraints as simple expression Displays all state variables changed and unchanged with respect to a previous item in an interactive picking This option works only if the i options has been specified c constraints Uses constraints to restrict the set of initial states in which the state has to be picked constraints must be enclosed between double quotes show_traces Shows the traces generated in a NuSMV session Command show_traces h v m o output file t a trace_number Shows the traces currently stored in system memory if any By default it shows the last generated trace if any Command Options v Verbosely prints traces content all state variables otherwise it prints out only those variables that have changed their value from previous state sb Prints only the total number of currently stored traces a Prints all the currently stored traces Chapter 4 Running NuSMV interactively 49 m Pipes the output through the program specified by the PAGER shell variable if defined else through the UNIX command more o output file Writes the output generated by the command to output file trace_number The ordinal identifier number of the trace to be printed showed_states Environment Variable Controls the maximum number of states showed during an interactive si
23. simple_expr gt simple_expr logical implication simple_expr lt gt simple_expr logical equivalence simple_expr simple_expr equality simple_expr simple_expr inequality simple_expr simple_expr simple_expr lt simple_expr gt simple_expr lt simple_expr set_simple_expr case_simple_ expr less than greater than less than or equal simple_expr gt simple_expr greater than or equal simple_expr simple_expr integer addition simple_expr simple_expr integer subtraction simple_expr simple_expr integer multiplication simple_expr simple_expr integer division simple_expr mod simple_expr integer remainder a set simple_expression a case expression A var_id see Section 3 2 10 Identifiers page 27 or identifier is a symbol or expression which identifies an object such as a variable or a defined symbol Since a var_id can be an atom there is a possible ambiguity if a variable or defined symbol has the same name as a symbolic constant Such an ambiguity is flagged by the interpreter as an error The order of parsing precedence for operators from high to low is Chapter 3 Syntax 22 Operators of equal precedence associate to the left except gt that associates to the right Parentheses may be used to group expressions 3 1 1 1 Case Expressions A case expression has the following syntax case_simple_expr case simple_expr simple_expr
24. state critical executing process proci gt State 1 6 lt executing process proc2 gt State 1 7 lt proc2 state exiting executing process proc2 gt State 1 8 lt semaphore 0 proc2 state idle executing process proc2 NuSMV tells us that the first CTL specification is true it is never the case that the two processes will be at the same time in the critical region On the other hand the second specification is false NuSMV produces a counter example path where initially proc1 goes to state entering state 1 3 and then a loop starts in which proc2 repeatedly enters its critical region state 1 5 and then returns to its idle state state 1 8 in the loop proc1 is activated only when proc2 is in the critical region and is therefore not able to enter its critical region state 1 6 This path Chapter 2 Tutorial 13 not only shows that the specification is false it also points out why can it happen that proc1 never enters its critical region Note that in the printout of a cyclic infinite counter example the starting point of the loop is marked by loop starts here Moreover in order to make it easier to follow the action in systems with a large number of variables only the values of variables that have changed in the last step are printed in the states of the trace 2 4 LTL model checking NuSMV allows for specifications expressed in LTL Intuitively while CTL specifications ex press properties
25. system for the verification Command go h This command initializes the system for verification It is equivalent to the command sequence read_model flatten_hierarchy encode_variables build_model build_ flat_model build_boolean_model If some commands have already been executed then only the remaining ones will be invoked Command options h Prints the command usage process_model Performs the batch steps and then returns control to the Command interactive shell process_model h i model file m Method Reads the model compiles it into BDD and performs the model checking of all the speci fication contained in it If the environment variable forward_search has been set before then the set of reachable states is computed If the environment variables enable_reorder and reorder_method are set then the reordering of variables is performed accordingly This command simulates the batch behavior of NuSMV and then returns the control to the interactive shell Command options i model file Sets the environment variable input_file to file model file and reads the model from file model file m Method Sets the environment variable partition_method to Method and uses it as partitioning method 4 2 Commands for Checking Specifications The following commands allow for the BDD based model checking of a NuSMV model compute_reachable Computes the set of reachable states Command compute_reachable h Computes the se
26. the beginning of a comment This can be changed using the set command In this description is used as the history_char The can appear anywhere in a line A line containing a history substitution is echoed to the screen after the substitution takes place can be preceded by a V in order to escape the substitution for example to enter a into an alias or to set the prompt Each valid line typed at the prompt is saved If the history variable is set see help page for set each line is also echoed to the history file You can use the history command to list the previously typed commands Substitutions At any point in a line these history substitutions are available 0 Initial word of last command Zn n th argument of last command 23 Last argument of last command Chapter 4 Running NuSMV interactively 56 All but initial word of last command Last command stuf Last command beginning with stuf n Repeat the n th command n Repeat the n th previous command old new Replace old with new in previous command Trailing spaces are signifi cant during substitution Initial spaces are not significant print_usage Prints processor and BDD statistics Command quit print_usage h Prints a formatted dump of processor specific usage statistics and BDD usage statistics For Berkeley Unix this includes all of the information in the getrusage structure Command op
27. types of fairness constraints namely justice constraints and compassion constraints A justice constraint consists of a formula f which is assumed to be true infinitely often in all the fair paths In NuSMV justice constraints are identified by keywords JUSTICE and for backward compatibility FAIRNESS A compassion constraint consists of a pair of formulas p q if property p is true infinitely often in a fair path then also formula q has to be true infinitely often in the fair path In NuSMV compassion constraints are identified by keyword COMPASSION Fairness constraints are declared using the following syntax fairness_declaration FAIRNESS simple_expr JUSTICE simple_expr COMPASSION simple_expr simple_expr A path is considered fair if and only if it satisfies all the constraints declared in this manner 3 3 Specifications The specifications to be checked on the FSM can be expressed in two different temporal logics the Computation Tree Logic CTL and the Linear Temporal Logic LTL extended with Past Operators It is also possible to analyze quantitative characteristics of the FSM by spec ifying real time CTL specifications Specifications can be positioned within modules in which case they are preprocessed to rename the variables according to the containing context CTL and LTL specifications are evaluated by NuSMV in order to determine their truth or falsity in the FSM When a specification is dis
28. user can activate the various NuSMV computation steps as system commands with different options These steps can therefore be invoked separately possibly undone or repeated under different modalities These steps include the construction of the model under different partitioning techniques model checking of specifications and the configuration of the BDD package The interactive shell of NuSMV is activated from the system prompt as follows NuSMV gt is the default NuSMV shell prompt system_prompt gt NuSMV int NuSMV gt A NuSMV command is a sequence of words The first word specifies the command to be executed The remaining words are arguments to the invoked command Commands separated by a are executed sequentially the NuSMV shell waits for each command to terminate in turn The behavior of commands can depend on environment variables similar to csh environment variables reset Edi read_model go go_bmc flatten_hierarchy encode_variables build_model eit compute_reachable t a check_spec check_ltlspec check_invar check_trans compute_reachable simulate check_Itlspec_bmc gen_Itlspec_bmc check_invar_bmc gen_invar_bmc bmc_simulate Chapter 4 Running NuSMV interactively 34 In the following we present the possible commands followed by the related environment variables classified in different categories Every com
29. you can explic itly specify by the l option or by its default value stored in the environment variable bmc_loopback The property to be checked may be specified using the n idr or the p formula options If you need to generate a dimacs dump file of all generated problems you must use the option o filename Command options n index index is the numeric index of a valid LTL specification formula actually located in the properties database p formula IN context Checks the formula specified on the command line context is the module instance name which the variables in formula must be evaluated in k maz_length maz_length is the maximum problem bound must be reached Only natural number are valid values for this option If no value is given the environment variable bmc_length is considered instead 1 loopback loopback value may be a natural number in 0 maz_length 1 Positive sign can be also used as prefix of the number Any invalid combination of length and loopback will be skipped during the generation solving process a negative number in 1 bmc_length In this case loopback is considered a value relative to max_length Any invalid combination of length and loopback will be skipped during the generation solving process the symbol X which means no loopback the symbol which means all possible loopback from zero to length 1 o filename filename is the name of the dumped dimacs
30. 50 mono Enables monolithic transition relation thresh cp_t conjunctive partitioning with threshold of each partition set to cpt DEFAULT with cp_t 1000 cp cpt DEPRECATED use thresh instead iwls95 cp_t Enables Iwls95 conjunctive partitioning and sets the threshold of each partition to cpt coi Enables cone of influence reduction noaffinity Disables affinity clustering iwls95preoder Enables iwls95 preordering bmc Enables BMC instead of BDD model checking bmc k Sets bmc_length variable used by BMC ofm fm_file prints flattened model to file fn_file obm bm_file Prints boolean model to file bn_file Bibliography 63 Bibliography BCCZ99 A Biere A Cimatti E Clarke and Y Zhu Symbolic Model Checking with out BDDs Tools and Algorithms for Construction and Analysis of Systems In TACAS 99 March 1999 CCG 02 A Cimatti E Clarke E Giunchiglia F Giunchiglia M Pistore M Roveri R Sebastiani and A Tacchella NuSMV 2 An OpenSource Tool for Symbolic Model Checking Proceedings of Computer Aided Verification CAV 02 2002 CCGR00 A Cimatti E Clarke F Giunchiglia and M Roveri NuSMV a new symbolic model checker International Journal on Software Tools for Technology Transfer STTT 2 4 March 2000 BCLM 94 J R Burch E M Clarke D E Long K L McMillan and D L Dill Symbolic Model Checking for Sequential Circuit Verification IEEE Transactions on Computer Aided De
31. ASSIGN init output 0 next output input MODULE main VAR gatel process inverter gate3 output gate2 process inverter gatel output gate3 process inverter gate2 output Among all the modules instantiated with the process keyword one is nondeterministically chosen and the assignment statements declared in that process are executed in parallel It is implicit that if a given variable is not assigned by the process then its value remains unchanged Because the choice of the next process to execute is non deterministic this program models the ring of inverters independently of the speed of the gates We remark that the system is not forced to eventually choose a given process to execute As a consequence the output of a given gate may remain constant regardless of its input In order to force a given process to execute infinitely often we can use a fairness constraint A fairness constraint restricts the attention of the model checker to only those execution paths along which a given formula is true infinitely often Each process has a special variable called running which is 1 if and only if that process is currently executing By adding the declaration FAIRNESS running to the module inverter we can effectively force every instance of inverter to execute infinitely often An alternative to using processes to model an asynchronous circuit is to allow all gates to execute simultaneously but to allow each gate to choose no
32. AVEAT Currently there is no check to see if there is a circular dependency in the alias definition e g NuSMV gt alias foo echo print_bdd_stats foo creates an alias which refers to itself Executing the command foo will result an infinite loop during which the command print_bdd_stats will be executed echo Merely echoes the arguments Command echo h lt args gt Echoes its arguments to standard output help Provides on line information on commands Command help a h lt command gt If invoked with no arguments help prints the list of all commands known to the command interpreter If a command name is given detailed information for that command will be provided Command options a Provides a list of all internal commands whose names begin with the under score character _ by convention history list previous commands and their event numbers Command history h lt num gt Lists previous commands and their event numbers This is a UNIX like history mechanism inside the NuSMV shell Command options lt num gt Lists the last lt num gt events Lists the last 30 events if lt num gt is not specified History Substitution The history substitution mechanism is a simpler version of the csh history substitution mechanism It enables you to reuse words from previously typed commands The default history substitution character is the is default for shell escapes and marks
33. NuSMV 2 1 User Manual Roberto Cavada Alessandro Cimatti Emanuele Olivetti Marco Pistore and Marco Roveri IRST Via Sommarive 18 38055 Povo Trento Italy Email nusmv irst itc it This document is part of the distribution package of the NuSMV model checker available at http nusmv irst itc it Parts of this documents have been taken from The SMV System Draft by K McMillan available at http www cs cmu edu modelcheck smv smvmanual r2 2 ps Copyright 1998 2002 by CMU and ITC irst Table of Contents I Antroduction ss isso telato e 1 A il A lana 2 2 1 Examples isa ia a eee a 2 2 2 OIL ALO a ADA EEA CGE nie a 6 2 3 CTL model checking 00 0 ttt eens 10 2 4 LTL model checking 13 2 5 Bounded Model Checking 15 dv Syntax tale erariale letale 21 Sed Expressions siii e AL ina 21 3 1 1 Simple Expressions 0 00 00 cece ee eee eee 21 3 1 1 1 Case Expressions 0 22 3 1 1 2 Set Expressions L 00 ceeeeeee 22 3 1 2 Next Expressions 0 0 cece eens 22 3 2 Definition of the FSM 23 3 2 1 State Variables o ooooooororommoo oo 23 3 2 1 1 Type Specifiers 0 0 c cee eee eee 23 3 2 2 Input Variables 0 0 cece eee eee eee 24 3 2 3 ASSIGN declarations 0 000 ccc cece cece ence 24 3 2 4 TRANS declarations 0 00 e cece cece eee eee 25 3 2 5 INIT declarations 0 000 cece cece cece eee eee 25 3
34. NuSMV gt echo foo bar foobar The variable foo is extended with the value foobar Whitespace characters may be present within quotes However variable interpolation lays the restriction that the characters and may not be used within quotes This is to allow for recursive interpolation So for example the following is allowed NuSMV gt set foo bar this NuSMV gt echo foo bar this The last line will be the output produced by NuSMV But in the following the value of the variable foo bar will not be interpreted correctly NuSMV gt set foo bar this NuSMV gt echo foo bar foo bar If a variable is not set by the set command then the variable is returned unchanged Different commands use environment information for different purposes The command interpreter makes use of the following parameters autoexec Defines a command string to be automatically executed after every command processed by the command interpreter This is useful for things like timing commands or tracing the progress of optimization open_path open_path in analogy to the shell variable PATH is a list of colon separated strings giving directories to be searched whenever a file is opened for read Typically the current directory is the first item in this list The standard system library typically NuSMV_LIBRARY_PATH is always im plicitly appended to the current path This provides a convenient short hand mechanism for reach
35. T solvers This makes NuSMV very robust portable efficient and easy to understand by other people than the developers This document is structured as follows e In Chapter 2 Tutorial page 2 we give an introduction to the usage of the main function alities of NuSMV e In Chapter 3 Syntax page 21 we define the syntax of the input language of NuSMV e In Chapter 4 Running NuSMV interactively page 33 the commands of the interaction shell are described e In Chapter 5 Running NuSMV batch page 61 we define the batch mode of NuSMV NuSMV is available at http nusmv irst itc it Chapter 2 Tutorial 2 2 Tutorial In this chapter we give a short introduction to the usage of the main functionalities of NuSMV In Section 2 1 Examples page 2 we describe the input language of NuSMV by presenting some examples of NuSMV models Section 2 2 Simulation page 6 shows how the user can get familiar with the behavior of a NuSMV model by exploring its possible executions Section 2 3 CTL model checking page 10 and Section 2 4 LTL model checking page 13 give an overview of BDD based model checking while Section 2 5 Bounded Model Checking page 15 presents SAT based model checking in NuSMV 2 1 Examples In this section we describe the input language of NuSMV by presenting some examples of NuSMV models A complete description of the NuSMV language can be found in Chapter 3 Syntax page 21 The input language of NuSMV is des
36. a specification to build the problem because only the model is used to build it The problem length is represented by the k command parameter or by its default value stored in the environment variable bmc_length Command options k length length is the length of the generated simulation Chapter 4 Running NuSMV interactively 48 4 4 Simulation Commands In this section we describe the commands that allow to simulate a NuSMV specification pick_state Picks a state from the set of initial states Command pick_state h v r i a c constraints Chooses an element from the set of initial states and makes it the current state re placing the old one The chosen state is stored as the first state of a new trace ready to be lengthened by steps states by the simulate command The state can be chosen according to different policies which can be specified via command line options By default the state is chosen in a deterministic way Command Options v Verbosely prints out chosen state all state variables otherwise it prints out only the label t 1 of the state chosen where t is the number of the new trace that is the number of traces so far generated plus one E Randomly picks a state from the set of initial states Enables the user to interactively pick up an initial state The user is requested to choose a state from a list of possible items every item in the list doesn t show state variables unchanged with
37. ack Command options n index index is the numeric index of a valid LTL specification formula actually located in the properties database The validity of index value is checked out by the system p formula IN context Checks the formula specified on the command line context is the module instance name which the variables in formula must be evaluated in k length length is the single problem bound used to generate and dump it Only natural number are valid values for this option If no value is given the environment variable bmc_length is considered instead 1 loopback loopback value may be a natural number in 0 length 1 Positive sign can be also used as prefix of the number Any invalid combination of length and loopback will be skipped during the generation and dumping process a negative number in 1 length Any invalid combination of length and loopback will be skipped during the generation process the symbol X which means no loopback the symbol which means all possible loopback from zero to length 1 o filename filename is the name of the dumped dimacs file If this options is not specified variable bmc_dimacs_filename will be considered The file name string may contain special symbols which will be macro expanded to form the real file name Possible symbols are F model name with path part f model name without path part k current problem bound l curre
38. age 21 The difference is that next expression allow to refer to next state variables The grammar is depicted below next_expr atom 33 a symbolic constant Chapter 3 Syntax number TRUE FALSE var_id n m next_expr next wen simple_expr nyi I next_expr next_expr next_expr next_expr next_expr next_expr next_expr next_expr next_expr next_expr next_expr next_expr next_expr next_expr next_expr next_expr amp next_expr next_expr xor next_expr gt next_expr lt gt next_expr next_expr I next_expr lt next_expr gt next_expr lt next_expr gt next_expr next_expr next_expr x next_expr next_expr mod next_expr set_next_expr next_expr case_next_ expr 23 a numeric constant The boolean constant 1 The boolean constant 0 a variable identifier next value of an expression logical not logical and logical or logical exclusive or logical implication logical equivalence equality inequality less than greater than less than or equal greater than or equal integer addition integer subtraction integer multiplication integer division integer remainder a set next_expression a case expression set_next_expr and case_next_expr are the same as set_simple_expr see Section 3 1 1 2 Set Expressions page 22 and cas
39. al operators Differently from stan dard temporal operators that allow to express properties over the future evolution of the FSM past temporal operators allow to characterize properties of the path that lead to the current situation The typical past operators are O p read once p stating that a certain condition p holds in one of the past time instants H p read historically p stating that a certain condition p holds in all previous time instants p S q read p since q stating that condition p holds since a previous state where condition q holds Y p read yesterday p stating that condition p holds in the previous time instant Past temporal operators can be combined with future temporal operators and allow for the compact characterization of complex properties A detailed description of the syntax of LTL formulas can be found in Section 3 3 2 LTL Specifications page 30 Chapter 2 Tutorial 15 2 5 Bounded Model Checking In this section we give a short introduction to the use of Bounded Model Checking BMC in NuSMV Further details on BMC can be found in Section 4 3 Commands for Bounded Model Checking page 41 For a more in depth introduction to the theory underlying BMC please refer to BCCZ99 Consider the following model representing a simple deterministic counter modulo 8 we assume that the following specification is contained in file modulo8 smv MODULE main VAR y 0 15 ASSIGN init y
40. ariant specifications IVAR It is used to introduce input variables JUSTICE It is used to introduce justice fairness constraints COMPASSION It is used to introduce compassion fairness constraints The IMPLEMENTS INPUT OUTPUT statements are not supported by NuSMV They are parsed from the input file but are internally ignored NuSMV differs from CMU SMV also in the controls that are performed on the input formulas Several formulas that are valid for CMU SMV but that have no clear semantics are not accepted by NuSMV In particular e It is no longer possible to write formulas containing nested next TRANS next alpha amp next beta next gamma gt delta e It is no longer possible to write formulas containing next in the right hand side of normal and init assignments they are allowed in the right hand side of next assignments and with the statements INVAR and INIT INVAR next alpha amp beta INIT next beta gt alpha ASSIGN delta alpha amp next gamma normal assignments init gamma alpha amp next delta init assignments e It is no longer possible to write SPEC FAIRNESS statements containing next FAIRNESS next running SPEC next x y e The check for circular dependencies among variables has been done more restrictive We say that variable x depends on variable y if x f y We say that there is a circular dependency in the definit
41. btained Force dynamic ordering to be invoked immediately The values for lt method gt are the same as in option e print_bdd_stats Prints out the BDD statistics and parameters print_bdd_stats h Prints the statistics for the BDD package The amount of information depends on the BDD package configuration established at compilation time The configurtion parameters are printed out too More information about statistics and parameters can be found in the documentation of the CUDD Decision Diagram package set_bdd_parameters Creates a table with the value of all currently active NuSMV flags and change accordingly the configurable parameters of the BDD package set_bdd_parameters h s Command Command Chapter 4 Running NuSMV interactively 54 Applies the variables table of the NuSMV environnement to the BDD package so the user can set specific BDD parameters to the given value This command works in conjunction with the print_bdd_stats and set commands print_bdd_stats first prints a report of the parameters and statistics of the current bdd_manager By using the command set the user may modify the value of any of the parameters of the underlying BDD package The way to do it is by setting a value in the variable BDD parameter name where parameter name is the name of the parameter exactly as printed by the print_bdd_stats command Command options s Prints the BDD parameter and statistics after the modificatio
42. cal only to a single simulation step and are forgotten in the next one 2 3 CTL model checking The main purpose of a model checker is to verify that a model satisfies a set of desired properties specified by the user In NuSMV the specifications to be checked can be expressed in two different temporal logics the Computation Tree Logic CTL and the Linear Temporal Logic LTL extended with Past Operators CTL and LTL specifications are evaluated by NuSMV in order to determine their truth or falsity in the FSM When a specification is discovered to be false NuSMV constructs and prints a counterexample i e a trace of the FSM that falsifies the property In this section we will describe model checking of specifications expressed in CTL while the next section we consider the case of LTL specifications CTL is a branching time logics its formulas allow for specifying properties that take into account the non deterministic branching evolution of a FSM More precisely the evolution of a FSM from a given state can be described as an infinite tree where the nodes are the states of the FSM and the branching in due to the non determinism in the transition relation The paths in the tree that start in a given state are the possible alternative evolutions of the FSM from that state In CTL one can express properties that should hold for all the paths that start in a state as well as for properties that should hold just for some of the paths Consider f
43. ce 60 nusmvestdini ila ra MER As eee 60 NUsmv_stdout illa dans 60 OPEN Path sb or ee che e elio 60 OUtpPUt Order files wees aii asian di ee 35 partition method idilio nicas 36 reorder method 51 BatusOlvers sita iii alle ve dei 47 SheLUschar 6 05 sl a as 60 Showed States i an a ae eeu 49 verbose Level iii Re ted AGG i bali ea 34 Index Index PAG Sw tiie bed Me ie Deep Lode hd babel yh deen 62 DMC liti A i 62 ble koala be Se EAO 62 FOOL TA A ESE li i cirie 62 A EO E eni rire ala tie Saath ons aa 62 AC DD csr etna dai de eda 61 Fett ao A i IA dii 61 MMM Chins io sori ili pic aa ea LE 62 S AE i oli ari e dl 61 shine A ESC daa ia 61 NGL pie see SLA ah este Bat a Pine esl elt cicle 61 A AU E o ese aus tabs oreo Ea yb ee vane Be 61 SU CLS ns the Bek itch lie PA Beeb racee Dara Re 61 1A LOD E NE E analisi 61 an D E A ee Bs Te ee Aol lol 61 SING toi fee a el ees ae an tote ee ha 61 SAS idee stain bee a Piece DA ep bun oe raat dd ERE 61 SIUWUS IS SCD teh sie cts Bidet eae ets E oe ee 62 iwlsQbpreorder ti di et eed 62 load emd fle iti Sis see ii Mente ra fae 62 Spi And hohe ici Sacer rt coni 61 I methods en ile gti Lia eae EA 62 MONO xa sesh eee teaser i cca ies Seed ta 62 SE 00s hs sah deed gedaan digits pbs ORE Oe ee 61 n6affinity s isos dale Yeu decode tel add 62 POO UPL she Boas sai eee pal DELI pe 61 SODMED INE Ue sass sth ON eee LE ec Loi 62 AA ied ate Beason aisles t
44. covered to be false NuSMV constructs and prints a counterexample i e a trace of the FSM that falsifies the property 1 In the current version of NuSMV compassion constraints are supported only for BDD based LTL model checking We plan to add support for compassion constraints also for CTL specifications and in Bounded Model Checking in the next releases of NuSMV Chapter 3 Syntax 30 3 3 1 CTL Specifications A CTL specification is given as a formula in the temporal logic CTL introduced by the keyword SPEC The syntax of this declaration is spec_declaration SPEC spec_expr spec_expr ctl_expr The syntax of CTL formulas recognized by the NuSMV parser is as follows ctl_expr simple_expr 3 a simple boolean expression ctl_expr ctl_expr 35 logical not ctl_expr amp ctl_expr 33 logical and ctl_expr ctl_expr logical or ctl_expr xor ctl_expr logical exclusive or ctl_expr gt ctl_expr 33 logical implies ctl_expr lt gt ctl_expr logical equivalence EG ctl_expr 33 exists globally EX ctl_expr exists next state EF ctl_expr 33 exists finally AG ctl_expr forall globally AX ctl_expr 3 forall next state AF ctl_expr forall finally E ctl_expr U ctl_expr exists until A ctl_expr U ctl_expr forall until It is an error for an expressions in a CTL formula to contain a next operator or to have non
45. ction Schedule in Image Computation to appear at FMCADO00 RAP 95 R K Ranjan A Aziz B Plessier C Pixley and R K Brayton Efficient BDD algorithms for FSM synthesis and verification In IEEE ACM Proceedings Interna tional Workshop on Logic Synthesis Lake Tahoe NV May 1995 Som98 F Somenzi CUDD CU Decision Diagram package release 2 2 0 Department of Electrical and Computer Engineering University of Colorado at Boulder May 1998 Vis96 VIS A system for Verification and Synthesis The VIS Group In the Proceed ings of the 8th International Conference on Computer Aided Verification p428 432 Springer Lecture Notes in Computer Science 1102 Edited by R Alur and T Henzinger New Brunswick NJ July 1996 Appendix A Compatibility with CMU SMV 64 Appendix A Compatibility with CMU SMV The NuSMV language is mostly source compatible with the original version of SMV distributed at Carnegie Mellon University from which we started In this appendix we describe the most common problems that can be encountered when trying to use old CMU SMV programs with NuSMV The main problem is variable names in old programs that conflicts with new reserved words The list of the new reserved words of NuSMV w r t CMU SMV is the following F G X U V W H 0 Y Z 5 T B These names are reserved for the LTL temporal operators LTLSPEC Itis used to introduce LTL specifications INVARSPEC It is used to introduce inv
46. dd the two corresponding LTL specification to the program as follows MODULE main VAR semaphore boolean proci process user semaphore proc2 process user semaphore ASSIGN init semaphore 0 LTLSPEC G proci state critical amp proc2 state critical LTLSPEC G proci state entering gt F proci state critical MODULE user semaphore VAR state idle entering critical exiting ASSIGN 2 In NuSMV a LTL specification are introduced by the keyword LTLSPEC see Section 3 3 2 LTL Specifications page 30 Chapter 2 Tutorial 14 init state idle next state case state idle idle entering state entering amp semaphore critical state critical critical exiting state exiting idle 1 State esac next semaphore case state entering 1 state exiting 0 1 semaphore esac FAIRNESS running NuSMV produces the following output specification G proci state critical amp proc2 state critical is true specification G procl state entering gt F proci state critical is false as demonstrated by the following execution sequence gt State 1 1 lt semaphore 0 proci state idle proc2 state idle executing process proc2 gt State 1 2 lt IA That is the first specification is true while the second is false and a counter example path is generated In NuSMV LTL properties can also include past tempor
47. dentified by a dot notation for example state 1 3 is the third state of the first generated trace Now the user can start a new simulation by choosing a new starting state In the next example for instance the user extends trace 1 by first choosing state 1 4 as the current state and by then running a random simulation of length 3 NuSMV gt goto_state 1 4 The starting state for new trace is gt State 2 4 lt request 1 state busy NuSMV gt simulate r 3 eeeKKKKK Simulation Starting From State 2 4 k NuSMV gt show traces 2 HEHHHHHHHHHHHHHHHHE Trace number 2 HHHHHHHHHHHHHHHHH gt State 2 1 lt request 1 state ready gt State 2 2 lt state busy gt State 2 3 lt request 0 gt State 2 4 lt request 1 gt State 2 5 lt request 0 gt State 2 6 lt state ready gt State 2 7 lt NuSMV gt As the reader can see from the previous example the new trace is stored as trace 2 The user is also able to interactively choose the states of the trace he wants to build an example of an interactive simulation is shown below NuSMV gt pick_state i FoR AVATLABLE FUTURE STATES HGO request 1 state ready Chapter 2 Tutorial request 0 Choose a state from the above 0 1 1 Chosen state is 1 NuSMV gt simulate i 1 eeeKKKKK Simulation Starting From State 3 1 kkk Fe AVAILABLE FUTURE STATES RRR RRR x 0 79 375 55574 request 1 state ready 1 Sea tae TO
48. e evaluated in n number Checks the LTL property with index number in the property database compute Performs computation of quantitative characteristics Command compute h m 0o output file n number p compute expr IN context This command deals with the computation of quantitative characteristics of real time systems It is able to compute the length of the shortest longest path from two given set of states MAX alpha beta MIN alpha beta Properties of the above form can be specified in the input file via the keyword COMPUTE or directly at command line using option p Option n can be used for computing a particular expression in the model If neither n nor p are used all the COMPUTE specifications are computed Command options m Pipes the output generated by the command in processing COMPUTEs to the program specified by the PAGER shell variable if defined else through the UNIX command more o output file Writes the output generated by the command in processing COMPUTEs to the file output file p compute expr IN context A COMPUTE formula to be checked context is the module instance name which the variables in compute expr must be evaluated in n number Computes only the property with index number add_property Adds a property to the list of properties Command add_property h c 1 i q p formula IN context Adds a property in the list of properties It is possib
49. e_simple_expr see Section 3 1 1 1 Case Expressions page 22 respectively with the replacement of simple with next The only additional production is next simple_expr which allows to shift all the variables in simple_expr to the next state The next operator distributes on every operator For instance the formula next A amp B C is a shorthand for the formula next A next B next C It is an error if in the scope of the next operator occurs another next operator 3 2 Definition of the FSM 3 2 1 State Variables A state of the model is an assignment of values to a set of state variables These variables and also instances of modules are declared by the notation var_declaration VAR atom n type atom n type The type associated with a variable declaration can be either a boolean a scalar a user defined module or an array of any of these including arrays of arrays 3 2 1 1 Type Specifiers A type specifier has the syntax type boolean nyu val a val ml E val Chapter 3 Syntax 24 number number array number number of type atom simple_expr simple_expr process atom simple_expr simple_expr val atom number A variable of type boolean can take on the numerical values 0 and 1 representing false and true respectively In the case of a list of values enclosed in quotes where ato
50. ea 62 ST shes dig ae esas Gand RASOI E Di ent 61 STEOFdEr iii indi okie te ea dle ees cide 62 E de area send leet hae end TE eal aa 61 thresh Cpto eric eae hh hac pa alal n 62 v verbose level m init A eek Bee 61 M SICA da cia 61 process_selector_ 0 2 cece cece ee eee ee eee 65 O ni a ydre ie el Mand etek 61 A administration commands 54 B batch running NUSMV LL 61 Bounded Model Checking 15 68 case expressions s s 0c eee eee eee eee 22 Commands for Bounded Model Checking 41 comments in NuSMV language 21 compassion constraints LL 29 CTL model checking 10 CTL Specifications 0 0 ee eee ee eee 30 D DD package interface 000000 50 DEFINE declaration eee e eee eee 25 E Examples cs tiglio Ree hie eee eh ee 2 EXPLESSIONS sii a eta ica oe eat 21 F fall paths oc cae weighed eee Geode ees aoe eas 29 fairness constraint 00 eee cece ee eee 4 fairness constraints 0 0 c eee eee ee eee 29 fairness constraints declaration 29 FAIRNESS declarations 00 eee eee 29 I identifiers ossia least rodi Lene 27 INIT declaration speise riv Ketan Pie ee ee 25 input variables i e dat 24 interactive shell 0 0 cee eee eee i 33 interactive running NUSMV 005 33 interface to DD Package
51. ecks whether the CTL formula is true in all the initial states of the model If this is not a case then NuSMV generates a counter example that is a finite or infinite trace that exhibits a valid behavior of the model that does not satisfy the specification Traces are very useful for identifying the error in the specification that leads to the wrong behavior We remark that the generation of a counter example trace is not always possible for CTL specifications Temporal operators corresponding to existential path quantifiers cannot be proved false by a showing of a single execution path Similarly sub formulas preceded by universal path quantifier cannot be proved true by a showing of a single execution path Consider the case of the semaphore program described in Section 2 1 Examples page 2 A desired property for this program is that it should never be the case that the two processes proci and proc2 are at the same time in the critical state this is an example of a safety property This property can be expressed by the following CTL formula AG proci state critical amp proc2 state critical Another desired property is that if proc1 wants to enter its critical state it eventually does this is an example of a liveness property This property can be expressed by the following CTL formula AG proci state entering gt AF proci state critical In order to verify the two formulas on the semaphore model we add the two correspo
52. ed at the end of the given ordering list according to the default ordering Command options i order file Sets the environment variable input_order_file to order file and reads the variable ordering to be used from file order file This can be combined with the write_order command The variable ordering is written to a file which can be inspected and reordered by the user and then read back in input_order_file Environment Variable Indicates the file name containing the variable ordering to be used in building the model by the encode_variables command There is no default value write_order Writes variable order to file Command write_order h o f order file Writes the current order of BDD variables in the file specified via the o option If no option is specified the environment variable output_order_file will be considered If the variable output_order_file is unset or set to an empty value then standard output will be used Command options o order file Sets the environment variable output_order_file to order file and then dumps the ordering list into that file f order file Alias for o option Supplied for backward compatibility output_order _file Environment Variable The file where the current variable ordering has to be written The default value is temp ord Chapter 4 Running NuSMV interactively 36 build_model Compiles the flattened hierarchy into BDD Command build_model h f
53. ent on the last command line typed In other words command substitution in a script file depends on how the script file was invoked Switches passed to a command are also counted as positional parameters Therefore if you type st x short smv bozo you will execute read_model i short smv Chapter 4 Running NuSMV interactively 59 flatten_hierarchy build_variables build_model compute_fairness To pass the x switch or any other switch to source when the script uses positional parameters you may define an alias For instance alias srcx source x time Provides a simple CPU elapsed time value Command time h Prints the processor time used since the last invocation of the time command and the total processor time used since NuSMV was started unalias Removes the definition of an alias Command unalias h lt alias names gt Removes the definition of an alias specified via the alias command Command options lt alias names gt Aliases to be removed unset Unsets an environment variable Command unset h lt variables gt A variable environment is maintained by the command interpreter The set command sets a variable to a particular value and the unset command removes the definition of a variable Command options h Prints the command usage lt variables gt Variables to be unset usage Provides a dump of process statistics Command usage h Prints a formatted dump of processor specif
54. eyword DEFINE is used to assign the expression value amp carry_in to the symbol carry_out A definition can be thought of as a variable with value functionally depending on the current values of other variables The same effect could have been obtained as follows notice that the current value of the variable is assigned rather than the next value VAR carry_out boolean ASSIGN carry_out value amp carry_in Defined symbols do not require introducing a new variable and hence do not increase the state space of the FSM On the other hand it is not possible to assign to a defined symbol a value non deterministically Another difference between defined symbols and variables is that while the type of variables is declared a priori for definitions this is not the case The previous examples describe synchronous systems where the assignments statements are taken into account in parallel and simultaneously NuSMV allows to model asynchronous systems It is possible to define a collection of parallel processes whose actions are interleaved Chapter 2 Tutorial 4 following an asynchronous model of concurrency This is useful for describing communication protocols or asynchronous circuits or other systems whose actions are not synchronized in cluding synchronous circuits with more than one clock region The following program represents a ring of three asynchronous inverting gates MODULE inverter input VAR output boolean
55. g the process_ model call Possible values are 0 or 1 Default value is 0 check_spec Performs fair CTL model checking Command check_spec h m o output file n number p ctl expr IN context Performs fair CTL model checking A ctl expr to be checked can be specified at command line using option p Alternatively option n can be used for checking a particular formula in the property database If neither n nor p are used all the SPEC formulas in the database are checked Command options m Pipes the output generated by the command in processing SPECs to the pro gram specified by the PAGER shell variable if defined else through the UNIX command more o output file Writes the output generated by the command in processing SPECs to the file output file p ctl expr IN context A CTL formula to be checked context is the module instance name which the variables in ctl expr must be evaluated in n number Checks the CTL property with index number in the property database If the ag_only_search environment variable has been set and the set of reachable states has been already computed then a specialized algorithm to check AG formulas is used instead of the standard model checking algorithms Chapter 4 Running NuSMV interactively 39 ag_only_search Environment Variable Enables the use of an ad hoc algorithm for checking AG formulas The algorithm given a formula of the form AG alpha computes the set of state
56. ic usage statistics For Berkeley Unix this includes all of the information in the getrusage structure which Looks for a file called filename Command which h lt file_name gt Looks for a file in a set of directories which includes the current directory as well as those in the NuSMV path If it finds the specified file it reports the found file s path The searching path is specified through the set open_path command in nusmvrc Command options lt file_name gt File to be searched Chapter 4 Running NuSMV interactively 60 4 8 Other Environment Variables The behavior of the system depends on the value of some environment variables For instance an environment variable specifies the partitioning method to be used in building the transition relation The value of environment variables can be inspected and modified with the set command Environment variables can be either logical or utility autoexec Environment Variable Defines a command string to be automatically executed after every command processed by the command interpreter This may be useful for timing commands or tracing the progress of optimization filec Environment Variable Enables file completion a la csh If the system has been compiled with the readline library the user is able to perform file completion by typing the key in a way similar to the file completion inside the bash shell If the system has not been compiled with the readli
57. ich the variables in formula must be evaluated in o filename filename is the name of the dumped dimacs file If you do not use this option the dimacs file name is taken from the environment variable bmc_invar_dimacs_filename File name may contain special symbols which will be macro expanded to form the real dimacs file name Possible symbols are F model name with path part f model name without path part n index of the currently processed formula in the properties database the character bmc_invar_dimacs filename Environment Variable This is the default file name used when generating DIMACS invar dumps This variable may be taken into account by the command gen invar bmc DIMACS file name can contain special symbols which will be expanded to represent the actual file name Possible symbols are e F The currently loaded model name with full path e f The currently loaded model name without full path e n The numerical index of the currently processed formula in the properties database The default value is f_invar_n n dimacs sat_solver Environment Variable The SAT solver s name actually to be used Default SAT solver is SIM Depending on the NuSMV configuration also the Zchaff SAT solver can be available or not Notice that Zchaff is for non commercial purposes only bmc_simulate Generates a trace of the model from 0 zero to k Command bmc_simulate h k bmc_simulate does not require
58. igh then the user has to specify some constraints as simple expression These constraints are used only for a single simulation step and are forgotten in the following ones They are to be intended in an opposite way with respect to those constraints eventually entered with the pick_state command or during an interactive simulation session when the number of future states to be displayed is too high that are local only to a single step of the simulation and are forgotten in the next one Chapter 4 Running NuSMV interactively 50 Displays all the state variables changed and unchanged during every step of an interactive session This option works only if the i option has been specified c constraints Performs a simulation in which computation is restricted to states satisfying those constraints The desired sequence of states could not exist if such con straints were too strong or it may happen that at some point of the simulation a future state satisfying those constraints doesn t exist in that case a trace with a number of states less than steps trace is obtained Note constraints must be enclosed between double quotes steps Maximum length of the path according to the constraints The length of a trace could contain less than steps states this is the case in which simula tion stops in an intermediate step because it may not exist any future state satisfying those constraints 4 5 Traces Inspection Commands A trace is
59. igned to allow for the description of Finite State Machines FSM from now on which range from completely synchronous to completely asynchronous and from the detailed to the abstract One can specify a system as a synchronous Mealy machine or as an asynchronous network of nondeterministic processes The language provides for modular hierarchical descriptions and for the definition of reusable components Since it is intended to describe finite state machines the only data types in the language are finite ones booleans scalars and fixed arrays Static data types can also be constructed The primary purpose of the NuSMV input is to describe the transition relation of the FSM this relation describes the valid evolutions of the state of the FSM In general any propositional expression in the propositional calculus can be used to define the transition relation This provides a great deal of flexibility and at the same time a certain danger of inconsistency For example the presence of a logical contradiction can result in a deadlock a state or states with no successor This can make some specifications vacuously true and makes the description unimplementable While the model checking process can be used to check for deadlocks it is best to avoid the problem when possible by using a restricted description style The NuSMV system supports this by providing a parallel assignment syntax The semantics of assignment in NuSMV is similar to that of si
60. in When you in the cell module declare e1 to be an instance of module element and you define grant out in module el to be below grant out you are really defining it to be the symbol ci grant out 3 2 11 The main module The syntax of a NuSMV program is Chapter 3 Syntax 29 program module_1 module_2 module_n There must be one module with the name main and no formal parameters The module main is the one evaluated by the interpreter 3 2 12 Processes Processes are used to model interleaving concurrency A process is a module which is instantiated using the keyword process see Section 3 2 1 State Variables page 23 The program executes a step by non deterministically choosing a process then executing all of the assignment statements in that process in parallel It is implicit that if a given variable is not assigned by the process then its value remains unchanged Each instance of a process has a special boolean variable associated with it called running The value of this variable is 1 if and only if the process instance is currently selected for execution A process may run only when its parent is running In addition no two processes with the same parents may be running at the same time 3 2 13 FAIRNESS declarations A fairness constraint restricts the attention only to fair execution paths When evaluating specifications the model checker considers path quantifiers to apply only to fair paths NuSMV supports two
61. in input from NuSMV but the ordering files generated by NuSMV may be not accepted by CMU SMV Notice that there is no guarantee that a good ordering for CMU SMV is also a good ordering for NuSMV In the ordering files for NuSMV identifier _process_selector_ can be used to control the position of the variable that encodes process selection In CMU SMV it is not possible to control the position of this variable in the ordering it is hard coded at the top of the ordering Command Index Command Index lias she A Bach ewok Sat en a ets B DICO UP iti eae tte A ates bDMG Simul at Omnia 6 bo he li eee dee all build model ici Ed Prado he as ata C CHECK Inv ii Yenc be oe i check invar DMG ssi ao breve lave ale re laa Blow check ttl spe s o J0 0a the daa dd dit check_ltlspec_bmc o ooocooooococmo oo check_ltlspec_bmc_onepb Check POCA RT lari da AA COMPUT Ces ccc eit aaa rai Mia PRE ere ra e ee compute_reachable D G gen Invar DM Sic e ii eil gen Ttlspec bie enie tes gen ltlspec Dmc suing a ithe cage a eee Seeds gen_ltlspec_bmc_onepb 66 MOD Dh bend aii ro ct di A letale 55 WTS COL Yo ariani pe hacia Bats alle Na ae Moiese dee 55 pick_state rsisonie ie ire EN ideale es 48 print_bdd Stats aio 53 print_current_state eee eee 50 print_iwls9boptioNS o oooo ooccooocmoo 37 print_reachable_states
62. ing standard library files nusmv_stderr Standard error normally stderr can be re directed to a file by setting the variable nusmv_stderr nusmv_stdout Standard output normally stdout can be re directed to a file by setting the variable nusmv_stdout Chapter 4 Running NuSMV interactively 58 source Executes a sequence of commands from a file Command source h p s x lt file gt lt args gt Reads and executes commands from a file Command options P Prints a prompt before reading each command s Silently ignores an attempt to execute commands from a nonexistent file x Echoes each command before it is executed lt file gt File name Arguments on the command line after the filename are remembered but not evaluated Commands in the script file can then refer to these arguments using the history substitu tion mechanism EXAMPLE Contents of test scr read_model i 2 flatten_hierarchy build_variables build_model compute_fairness Typing source test scr short smv on the command line will execute the sequence read_model i short smv flatten_hierarchy build_variables build_model compute_fairness In this case 0 gets source 1 gets test scr and 2 gets short smv If you type alias st source test scr and then type st short smv bozo you will execute read_model i bozo flatten_hierarchy build_variables build_model compute_fairness because bozo was the second argum
63. ion of x if x depends on itself e g x f x y x depends on y and y depends on z e g x f y and y f x or x f z z fly and y f x Appendix A Compatibility with CMU SMV 65 In the case of circular dependencies among variables there is no fixed order in which we can compute the involved variables Avoiding circular dependencies among variables guarantee that there exists an order in which the variables can be computed In NuSMV circular dependencies are not allowed In CMU SMV the test for circular dependencies is able to detect circular dependencies only in normal assignments and not in next assignments The circular dependencies check of NuSMV has been extended to detect circularities also in next assignments For instance the following fragment of code is accepted by CMU SMV but discarded by NuSMV MODULE main VAR y boolean x boolean ASSIGN next x x amp next y next y y amp next x Another difference between NuSMV and CMU SMV is in the variable order file The variable ordering file accepted by NuSMV can be partial and can contain variables not declared in the model Variables listed in the ordering file but not declared in the model are simply discarded The variables declared in the model but not listed in the variable file provided in input are created at the end of the given ordering following the default ordering All the ordering files generated by CMU SMV are accepted
64. iptions more concise a symbol can be associated with a commonly expression The syntax for this kind of declaration is define_declaration DEFINE atom simple_expr atom simple_expr Chapter 3 Syntax 26 atom simple_expr Whenever an identifier referring to the symbol on the left hand side of the in a DEFINE occurs in an expression it is replaced by the expression on the right hand side The expression on the right hand side is always evaluated in its context however see Section 3 2 9 MODULE declarations page 26 for an explanation of contexts Forward references to defined symbols are allowed but circular definitions are not allowed and result in an error It is not possible to assign values to defined symbols non deterministically Another differ ence between defined symbols and variables is that while variables are statically typed definitions are not 3 2 8 ISA declarations There are cases in which some parts of a module could be shared among different modules or could be used as a module themselves In NuSMV it is possible to declare the common parts as separate modules and then use the ISA declaration to import the common parts inside a module declaration The syntax of an ISA declaration is as follows isa_declaration ISA atom where atom must be the name of a declared module The ISA declaration can be thought as a simple macro expansion command because the body of the module
65. itional information on the internal operations of NuSMV Set ting verbose level to 1 gives the basic information Using this option makes you feel better since otherwise the program prints nothing until it finishes and there is no evidence that it is doing anything at all Setting the verbose level higher than 1 enables printing of much extra information cpp Runs preprocessor on SMV files is Does not check SPEC ic Does not check COMPUTE ils Does not check LTLSPEC ii Does not check INVARSPEC r Prints the number of reachable states before exiting If the f option is not used the set of reachable states is computed f Computes the set of reachable states before evaluating CTL expressions int Starts interactive shell help h Prints the command line help i iv_file Reads the variable ordering from file iv_file o ov_file Reads the variable ordering from file ov_file Chapter 5 Running NuSMV batch 62 AG Verifies only AG formulas using an ad hoc algorithm see documentation for the ag_only_search environment variable load cmd file Interprets NuSMV commands from file cmd file reorder Enables variable reordering after having checked all the specification if any dynamic Enables dynamic reordering of variables m method Uses method when variable ordering is enabled Possible values for method are those allowed for the reorder_method environment variable see Section 4 6 Interface to the DD package page
66. le to insert LTL CTL INVAR and quantitative COMPUTE properties Every newly inserted property is initialized to unchecked A type option must be given to properly execute the command Chapter 4 Running NuSMV interactively 41 Command options c Adds a CTL property 1 Adds an LTL property P Adds an INVAR property mel Adds a quantitative COMPUTE property p formula IN context Adds the formula specified on the command line context is the module instance name which the variables in formula must be evaluated in 4 3 Commands for Bounded Model Checking In this section we describe in detail the commands for doing and controlling Bounded Model Checking in NuSMV Bounded Model Checking is based on the reduction of the bounded model checking problem to a propositional satisfiability problem After the problem is generated NuSMV internally calls a propositional SAT solver in order to find an assignment which satisfies the problem Currently NuSMV supplies two SAT solvers SIM and Zchaff Notice that Zchaff is for non commercial purposes only and is therefore not included in the source code distribution as well as in some of the binary distributions of NuSMV It is also possible to generate the satisfiability problem without calling the SAT solver Each generated problem is dumped in DIMACS format into a file DIMACS is the standard format used as input by most external SAT solver so it is possible to use NuSMV with an exte
67. mand answers to the option h by printing out the command usage When output is paged for some commands option m it is piped through the program specified by the UNIX PAGER shell variable if defined or through UNIX command more Environment variables can be assigned a value with the set command Command sequences to NuSMV must obey the partial order specified in the figure depicted in the previous page For instance it is not possible to evaluate CTL expressions before the model is built The verbosity of NuSMV is controlled by the following environment variable verbose _level Environment Variable Controls the verbosity of the system Possible values are integers from 0 no messages to 4 full messages The default value is 0 4 1 Model Reading and Building The following commands allow for the parsing and the compilation of the model into BDD read_model Reads a NuSMV file into NuSMV Command read_model h i model file Reads a NuSMV file If the i option is not specified it reads from the file specified in the environment variable input_file Command options i model file Sets the environment variable input_file to model file and reads the model from the specified file input file Environment Variable Stores the name of the input file containing the model It can be set by the set command or by the command line option i There is no default value flatten_hierarchy Flattens the hierarchy of m
68. mands for Bounded Model Checking page 41 This command accepts options k that specifies the length of the counter example we are looking for and 1 that defines the loopback condition Consider the following interactive session system_prompt gt NuSMV int modulo8 smv NuSMV gt go_bmc NuSMV gt check_ltlspec_bmc_onepb k 9 1 0 no counterexample found with bound 9 and loop at 0 for specification IG Fy 2 NuSMV gt check_Itlspec_bmc_onepb k 8 1 1 no counterexample found with bound 8 and loop at 1 for specification Chapter 2 Tutorial 18 IG Fy 2 NuSMV gt check_Itlspec_bmc_onepb k 9 1 1 specification G Fy 2 is false as demonstrated by the following execution sequence State 1 1 y 0 loop starts here State 1 y State State State State State State State State 1 10 NuSMV gt quit system_prompt gt N Il ONO PUNE FoOAN DOA W lt lt lt lt S lt S lt lt I VHHHHHHWHHH lt Il m NuSMV did not find a counterexample for cases k 9 1 0 and k 8 1 1 The following figures show that these case look for counterexamples that do not match with the model of the counter so it is not possible for NuSMV to satisfy them k 9 1 0 0 gt 0 gt 0 gt 0 gt 0 gt 0 gt 0 gt 0 gt 0 gt 0 bound 0 1 2 3 4 5 6 7 8 9 y value 0 1 2 3 4 5 6 7 0 1 0 gt 0 gt 0 gt 0 gt 0 gt 0 gt 0 gt 0 gt o bound 0 1 2 3 4 5 6 T 8 y value 0 1 2 3 4 5 6 l
69. ms are taken to be symbolic constants the variable is a scalar which take any of these values In the case of an array declaration the first simple_expr is the lower bound on the subscript and the second simple_expr is the upper bound Both of these expressions must evaluate to integer constants Finally an atom optionally followed by a list of expressions in parentheses indicates an instance of module atom See Section 3 2 9 MODULE declarations page 26 The keyword causes the module to be instantiated as an asynchronous process See Section 3 2 12 Processes page 29 3 2 2 Input Variables A state of the model is an assignment of values to a set of state variables These variables and also instances of modules are declared by the notation ivar_declaration IVAR atom n type atom n type 7 n The type associated with a variable declaration can be either a boolean a scalar a user de fined module or an array of any of these including arrays of arrays See Section 3 2 1 State Variables page 23 3 2 3 ASSIGN declarations An assignment has the form assign_declaration ASSIGN assign_body assign_body assign_body atom simple_expr normal assignment init atom simple_expr init assignment next atom next_expr 3 next assignment On the left hand side of the assignment atom denotes the current value of a variable init atom denotes its
70. mulation session Possible values are integers from 1 to 100 The default value is 25 simulate Performs a simulation from the current selected state Command simulate h p v r i a c constraints steps Generates a sequence of at most steps states representing a possible execution of the model starting from the current state The current state must be set via the pick_state or goto_state commands It is possible to run the simulation in three ways according to different command line policies deterministic the default mode random and interactive The resulting sequence is stored in a trace indexed with an integer number taking into account the total number of traces stored in the system There is a different behavior in the way traces are built according to how current state is set current state is always put at the beginning of a new trace so it will contain at most steps 1 states except when it is the last state of an existent old trace In this case the old trace is lengthened by at most steps states Command Options P Prints current generated trace only those variables whose value changed from the previous state v Verbosely prints current generated trace changed and unchanged state vari ables r Picks a state from a set of possible future states in a random way i Enables the user to interactively choose every state of the trace step by step If the number of possible states is too h
71. n 4 7 Administration Commands This section describes the administrative commands offered by the interactive shell of NuSMV shell command Command Executes a shell command The shellcommand is executed by calling bin sh c shell command If the command does not exists or you have not the right to execute it then an error message is printed alias Provides an alias for a command Command alias h lt name gt lt string gt The alias command if given no arguments will print the definition of all current aliases Given a single argument it will print the definition of that alias if any Given two arguments the keyword lt name gt becomes an alias for the command string lt string gt replacing any other alias with the same name Command options lt name gt Alias lt string gt Command string It is possible to create aliases that take arguments by using the history substitution mech anism To protect the history substitution character from immediate expansion it must be preceded by a V when entering the alias For example NuSMV gt alias read read_model i 4 1 smv set input_order_file 1 ord NuSMV gt read short will create an alias read execute read_model i short smv set input order file short ord And again NuSMV gt alias echo2 echo Hi echo NuSMV gt echo2 happy birthday will print Hi happy birthday Chapter 4 Running NuSMV interactively 55 C
72. n built It is possible to save the ordering found using write_order in order to reuse it using build_model i order file in the future Command options d Disable dynamic ordering from triggering automatically e lt method gt Enable dynamic ordering to trigger automatically whenever a certain thresh old on the overall BDD size is reached lt method gt must be one of the following sift Moves each variable throughout the order to find an optimal position for that variable assuming all other variables are fixed This generally achieves greater size reductions than the window method but is slower random Pairs of variables are randomly chosen and swapped in the order The swap is performed by a series of swaps of adjacent variables The best order among those obtained by the series of swaps is retained The number of pairs chosen for swapping equals the number of variables in the diagram random_pivot Same as random but the two variables are chosen so that the first is above the variable with the largest number of nodes and the Chapter 4 Running NuSMV interactively 53 f lt method gt second is below that variable In case there are several variables tied for the maximum number of nodes the one closest to the root is used sift_converge The sift method is iterated until no further improvement is obtained symmetry_sift This method is an implementation of symmetric sifting It is similar to sifting with one addi
73. n deterministically to re evaluate its output or to keep the same output value Such a model of the inverter ring would look like the following MODULE main VAR gatel inverter gate3 output gate2 inverter gate2 output gate3 inverter gatel output SPEC AG AF gatel out amp AG AF gatel out MODULE inverter input VAR output boolean ASSIGN init output 0 next output input union output Chapter 2 Tutorial 5 The union operator set union coerces its arguments to singleton sets as necessary Thus the next output of each gate can be either its current output or the negation of its current input each gate can choose non deterministically whether to delay or not As a result the number of possible transitions from a given state can be as 2 where n is the number of gates This sometimes but not always makes it more expensive to represent the transition relation The following program is another example of asynchronous model It uses a variable semaphore to implement mutual exclusion between two asynchronous processes Each process has four states idle entering critical and exiting The entering state indicates that the process wants to enter its critical region If the variable semaphore is 0 it goes to the critical state and sets semaphore to 1 On exiting its critical region the process sets semaphore to 0 again MODULE main VAR semaphore boolean proci process user semaphore
74. n session could be as follows Suppose to use the model described below Chapter 2 Tutorial 7 MODULE main VAR request boolean state ready busy ASSIGN init state ready next state case state ready amp request busy 1 ready busy esac As a preliminary step this model has to read into the NuSMV system This can be obtained by executing the following commands we assume that the model is saved in file short smv system_prompt gt NuSMV int short smv NuSMV gt go NuSMV gt In order to start the simulation an initial state has to be chosen This can be done in three ways e by default the simulator uses the current state as a starting point of every new simulation this behavior if possible only if a current state is defined e g if we are exploring a trace as described in Section 4 5 Traces Inspection Commands page 50 e if command goto_state is used the user can select any state of an already existent trace as the current state see see Section 4 5 Traces Inspection Commands page 50 e if pick_state is used then the user can choose the starting state of the simulation among the initial states of the model this command has to be used when a current state does not exist yet that is when the system has being reset At this point of the example current state does not exist and there is no trace currently stored in the system Therefore an item from the set of initial states has
75. n the third simulation mode the user has a complete control over traces generation by interactively building the trace During an interactive simulation session the system stops at every step showing a list of possible future states the user is requested to choose one of the items This feature is particularly useful when one wants to inspect some particular reactions of the model to be checked When the number of possible future states exceeds an internal limit rather than confusing the user with a choice from a high number of possible evolutions the system asks the user to guide the simulation via the insertion of some further constraints over the possible future states The system will continue to ask for constraints insertion until the number of future states will be under the predefined threshold The constraints entered during this phase are accumulated in a logical product in a single big constraint This constraint is used only for the current step of the simulation and is discarded before the next step The system checks the expressions entered by the user and does not accept them whenever an inconsistency arises Cases of inconsistency i e empty set of states may be caused by e the entered expressions i e a amp a e the result of the entered expressions conjoined with previous accumulated ones e the result of accumulated constraints conjoined with the set of possible future states A typical execution sequence of a simulatio
76. nding CTL specification to the program as follows MODULE main VAR semaphore boolean proci process user semaphore proc2 process user semaphore ASSIGN init semaphore 0 SPEC AG procl state critical amp proc2 state critical SPEC AG proci state entering gt AF procl state critical MODULE user semaphore VAR state idle entering critical exiting ASSIGN init state idle next state case state idle idle entering state entering amp semaphore critical state critical critical exiting state exiting idle 1 state esac next semaphore case state entering 1 state exiting 0 1 semaphore esac FAIRNESS Chapter 2 Tutorial 12 running By running NuSMV with the command system_prompt gt NuSMV semaphore smv we obtain the following output specification AG proci state critical amp proc2 state critical is true specification AG proci state entering gt AF proci state critical is false as demonstrated by the following execution sequence gt State 1 1 lt semaphore 0 proci state idle proc2 state idle executing process proc2 gt State 1 2 lt executing process proc1 loop starts here gt State 1 3 lt proci state entering executing process proc2 gt State 1 4 lt proc2 state entering executing process proc2 gt State 1 5 lt semaphore 1 proc2
77. ne library a built in method to perform file completion a la csh can be used This method is enabled with the set filec command The csh file completion method can be also enabled if the readline library has been used In this case the features offered by readline will be disabled shell_char Environment Variable shell_char specifies a character to be used as shell escape The default value of this environment variable is history char Environment Variable history_char specifies a character to be used in history substitutions The default value of this environment variable is open_path Environment Variable open_path in analogy to the shell variable PATH is a list of colon separated strings giving directories to be searched whenever a file is opened for read Typically the current directory is first in this list The standard system library NuSMV_LIBRARY_PATH is always implicitly appended to the current path This provides a convenient short hand mechanism for reaching standard library files nusmv_stderr Environment Variable Standard error normally stderr can be re directed to a file by setting the variable nusmv_stderr nusmv_stdout Environment Variable Standard output normally stdout can be re directed to a file by setting the internal variable nusmv_stdout nusmv_stdin Environment Variable Standard input normally stdin can be re directed to a file by setting the internal variable nusmv_s
78. ned by a boolean valued expression T introduced by the TRANS keyword The syntax of a TRANS declaration is trans_declaration TRANS trans_expr trans_expr next_expr It is an error for the expression to yield any value other than 0 or 1 If there is more than one TRANS declaration the transition relation is the conjunction of all of TRANS declarations 3 2 5 INIT declarations The set of initial states of the model is determined by a boolean expression under the INIT keyword The syntax of a INIT declaration is init_declaration INIT init_expr init_expr simple_expr It is an error for the expression to contain the next operator or to yield any value other than 0 or 1 If there is more than one INIT declaration the initial set is the conjunction of all of the INIT declarations 3 2 6 INVAR declarations The set of invariant states i e the analogous of normal assignments as described in Section 3 2 3 ASSIGN declarations page 24 can be specified using a boolean expression under the INVAR keyword The syntax of a INVAR declaration is invar_declaration INVAR invar_expr invar_expr simple_expr It is an error for the expression to contain the next operator or to yield any value other than 0 or 1 If there is more than one INVAR declaration the invariant set is the conjunction of all of the INVAR declarations 3 2 7 DEFINE declarations In order to make descr
79. ngle assignment data flow language By checking programs for multiple parallel assignments to the same variable circular assignments and type errors the interpreter insures that a program using only the assignment mechanism is implementable Consequently this fragment of the language can be viewed as a description language or a programming language Consider the following simple program in the NuSMV language MODULE main VAR request boolean state ready busy ASSIGN init state ready next state case state ready amp request 1 busy 1 ready busy esac The space of states of the FSM is determined by the declarations of the state variables in the above example request and state The variable request is declared to be of predefined type boolean This means that it can assume the integer values 0 and 1 The variable state is a Chapter 2 Tutorial 3 scalar variable which can take the symbolic values ready or busy The following assignment sets the initial value of the variable state to ready The initial value of request is completely unspecified i e it can be either 0 or 1 The transition relation of the FSM is expressed by defining the value of variables in the next state i e after each transition given the value of variables in the current states i e before the transition The case segment sets the next value of the variable state to the value busy after the column if its current value is read
80. no counterexample found with bound 4 for system_prompt gt Let us consider now another property G F y 2 stating that y gets the value 2 only a finite number of times Again this is a false property due to the cyclic nature of the model Let us modify the specification of file mode18 smv as follows LTLSPEC G F y 2 and let us run NuSMV in BMC mode system_prompt gt NuSMV bmc modulo8 smv no counterexample found with bound O for specification G Fy 2 no counterexample found with bound 1 for no counterexample found with bound 2 for no counterexample found with bound 3 for no counterexample found with bound 4 for no counterexample found with bound 5 for no counterexample found with bound 6 for no counterexample found with bound 7 for specification G Fy 2 is false as demonstrated by the following execution sequence loop starts here State 2 1 y 0 State 2 2 y 1 State 2 3 y 2 State 2 4 y 3 State 2 5 y 4 Chapter 2 Tutorial 17 State 2 6 y 5 State 2 7 y 6 State 2 8 y 7 State 2 9 y 0 system_prompt gt In this example NuSMV has increased the problem bound until a cyclic behavior of length 8 is found that contains a state where y value is 2 Since the behavior is cyclic state 2 3 is entered infinitely often and the property is false 0 gt 0 gt 0 gt 0 gt 0 gt 0 gt 0 gt 0 gt o bound 0 1 2 3 4 5 6 7
81. nt loopback value n index of the currently processed formula in the properties database the character Chapter 4 Running NuSMV interactively 46 bmc_length Environment Variable Sets the generated problem bound Possible values are any natural number but must be compatible with the current value held by the variable bmc_loopback The default value is 10 bmc_loopback Environment Variable Sets the generated problem loop Possible values are Any natural number but lesser than the current value of the variable bmc_length In this case the loop point is absolute Any negative number but greater or equal than bmc_length In this case specified loop is the loop length The symbol X which means no loopback The symbol which means any possible loopbacks The default value is bmc_dimacs filename Environment Variable This is the default file name used when generating DIMACS problem dumps This variable may be taken into account by all commands which belong to the gen _ltlspec_bmc family DIMACS file name can contain special symbols which will be expanded to represent the actual file name Possible symbols are F The currently loaded model name with full path f The currently loaded model name without full path n The numerical index of the currently processed formula in the properties database k The currently generated problem length l The currently generated problem loopback value The
82. oduction NuSMV is a symbolic model checker originated from the reengineering reimplementation and extension of CMU SMV the original BDD based model checker developed at CMU McMil93 The NuSMV project aims at the development of a state of the art symbolic model checker de signed to be applicable in technology transfer projects it is a well structured open flexible and documented platform for model checking and is robust and close to industrial systems standards CCGROO Version 1 of NuSMV basically implements BDD based symbolic model checking Version 2 of NuSMV NuSMV2 in the following inherits all the functionalities of the previous version and extend them in several directions CCG 02 The main novelty in NuSMV2 is the integration of model checking techniques based on propositional satisfiability SAT BCCZ99 SAT based model checking is currently enjoying a substantial success in several industrial fields and opens up new research directions BDD based and SAT based model checking are often able to solve different classes of problems and can therefore be seen as complementary techniques Starting from NuSMV2 we are also adopting a new development and license model NuSMV2 is distributed with an OpenSource license see http www opensource org that allows anyone interested to freely use the tool and to participate in its development The aim of the NuSMV OpenSource project is to provide to the model checking community a common
83. odules Command flatten_hierarchy h This command is responsible of the instantiation of modules and processes The instanti ation is performed by substituting the actual parameters for the formal parameters and then by prefixing the result via the instance name show_vars Shows model s symbolic variables and their values Command show_vars h s i m o output file Prints symbolic input and state variables of the model with their range of values as defined in the input file Command Options s Prints only state variables Prints only input variables Chapter 4 Running NuSMV interactively 35 m Pipes the output to the program specified by the PAGER shell variable if de fined else through the UNIX command more o output file Writes the output generated by the command to output file encode_variables Builds the BDD variables necessary to compile the Command model into BDD encode_variables h i order file 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 The input order file can be partial and can contain variables not declared in the model Variables not declared in the model are simply discarded Variables declared in the model which are not listed in the ordering input file will be created and append
84. of SAT based bounded model checking In the first case NuSMV proceeds along the lines described in CGH97 For each LTL specification a tableau able to recognize the behaviors falsifying the property is constructed and then synchronously composed with the model With respect to CGH97 the approach is fully integrated within NuSMV and allows for full treatment of past temporal operators In the case of BDD based reasoning the counterexample generated to show the falsity of a LTL specification may contain state variables which have been introduced by the tableau construction procedure In the second case a similar tableau construction is carried out to encode the existence of a path of limited length violating the property NuSMV generates a propositional satisfiability problem that is then tackled by means of an efficient SAT solver BCCZ99 In both cases the tableau constructions are completely transparent to the user 3 3 3 Real Time CTL Specifications and Computations NuSMV allows for Real Time CTL specifications EMSS90 NuSMV assumes that each tran sition takes unit time for execution RTCTL extends the syntax of CTL path expressions with the following bounded modalities rtctl_expr ctl_expr EBF range rtctl_expr ABF range rtctl_expr EBG range rtctl_expr ABG range rtctl_expr A rtctl_expr BU range rtctl_expr E rtctl_expr BU range rtctl_expr range number number Intuitivel
85. or instance CTL formula AF p It expresses the condition that for all the paths A stating from a state eventually in the future F condition p must hold That is all the possible evolutions of the system will eventually reach a state satisfying condition p CTL formula EF p on the other hand requires than there exists some path E that eventually in the future satisfies p Similarly formula AG p requires that condition p is always or globally true in all the states of all the possible paths while formula EG p requires that there is some path along which condition p is continuously true Other CTL operators are e A pUq and E p U q requiring condition p to be true until a state is reached that satisfies condition q e AX pand EX p requiring that condition p is true in all or in some of the next states reachable from the current state CTL operators can be nested in an arbitrary way and can be combined using logic operators amp gt lt gt Typical examples of CTL formulas are AG p condition p is absent in all the evolutions AG EF p it is always possible to reach a state where p holds and AG p gt AF q each occurrence of condition p is followed by an occurrence of condition q Chapter 2 Tutorial 11 In NuSMV a CTL specification is given as CTL formula introduced by the keyword SPEC see Section 3 3 1 CTL Specifications page 30 Whenever a CTL specification is processed NuSMV ch
86. ormed by a series of swaps of adjacent variables The best order among those obtained by the series of swaps is retained The number of pairs chosen for swapping equals the number of variables in the diagram random_pivot Same as random but the two variables are chosen so that the first is above the variable with the largest number of nodes and the second is below that variable In case there are several variables tied for the maximum number of nodes the one closest to the root is used sift_converge The sift method is iterated until no further improvement is obtained symmetry_sift This method is an implementation of symmetric sifting It is similar to sifting with one addition Variables that become adjacent during sifting are tested for symmetry If they are symmetric they are linked in a group Sifting then continues with a group being moved instead of a single variable symmetry_sift_converge The symmetry_sift method is iterated until no further improvement is ob tained window 2 3 4 Permutes the variables within windows of n adjacent variables where n can be either 2 3 or 4 so as to minimize the overall BDD size window 2 3 4 _converge The window 2 3 4 method is iterated until no further improvement is ob tained Chapter 4 Running NuSMV interactively 52 group_sift This method is similar to symmetry_sift but uses more general criteria to create groups group_sift_converge The group_sift method is itera
87. over the computation tree of the FSM branching time approach LTL char acterizes each linear path induced by the FSM linear time approach The two logics have in general different expressive power but also share a significant intersection that includes most of the common properties used in practice Typical LTL operators are e Fp read in the future p stating that a certain condition p holds in one of the future time instants e Gp read globally p stating that a certain condition p holds in all future time instants e pUq read p until q stating that condition p holds until a state is reached where condition q holds e Xp read next p stating that condition p is true in the next state We remark that differently from CTL LTL temporal operators do not have path quantifiers In fact LTL formulas are evaluated on linear paths and a formula is considered true in a given state if it is true for all the paths starting in that state Consider the case of the semaphore program and of the safety and liveness properties already described in Section 2 3 CTL model checking page 10 These properties correspond to LTL formulas G proci state critical amp proc2 state critical expressing that the two processes cannot be in the critical region at the same time and G proci state entering gt F proci state critical expressing that whenever a process wants to enter its critical session it eventually does If we a
88. platform for the research the implementation and the comparison of new symbolic model checking techniques Since the release of NuSMV2 the NuSMV team has received code contributions for different parts of the system Several research institutes and commercial companies have express interest in collaborating to the development of NuSMV The main features of NuSMV are the following e Functionalities NuSMV allows for the representation of synchronous and asynchronous finite state systems and for the analysis of specifications expressed in Computation Tree Logic CTL and Linear Temporal Logic LTL using BDD based and SAT based model checking techniques Heuristics are available for achieving efficiency and partially controlling the state explosion The interaction with the user can be carried on with a textual interface as well as in batch mode e Architecture A software architecture has been defined The different components and functionalities of NuSMV have been isolated and separated in modules Interfaces between modules have been provided This reduces the effort needed to modify and extend NuSMV e Quality of the implementation NuSMV is written in ANSI C is POSIX compliant and has been debugged with Purify in order to detect memory leaks Furthermore the system code is thoroughly commented NuSMV uses the state of the art BDD package developed at Colorado University and provides a general interface for linking with state of the art SA
89. proc2 process user semaphore ASSIGN init semaphore 0 MODULE user semaphore VAR state idle entering critical exiting ASSIGN init state idle next state case state idle idle entering state entering amp semaphore critical state critical critical exiting state exiting idle 1 State esac next semaphore case state entering 1 state exiting 0 1 semaphore esac FAIRNESS running NuSMV allows to specify the FSM directly in terms of propositional formulas The set of possible initial states is specified as a formula in the current state variables A state is initial if it satisfies the formula The transition relation is directly specified as a propositional formula in terms of the current and next values of the state variables Any current state next state pair is in the transition relation if and only if it satisfies the formula These two functions are accomplished by the INIT and TRANS keywords As an example here is a description of the three inverter ring using only TRANS and INIT MODULE main VAR gatel inverter gate3 output Chapter 2 Tutorial 6 gate2 inverter gatel output gate3 inverter gate2 output MODULE inverter input VAR output boolean INIT output 0 TRANS next output input next output output According to the TRANS declaration for each inverter the next value of the output is equal either to the
90. referenced by an ISA command is replaced to the ISA declaration 3 2 9 MODULE declarations A module is an encapsulated collection of declarations Once defined a module can be reused as many times as necessary Modules can also be so that each instance of a module can refer to different data values A module can contain instances of other modules allowing a structural hierarchy to be built The syntax of a module declaration is as follows module MODULE atom atom atom atom var_declaration ivar_declaration assign_declaration trans_declaration init_declaration invar_declaration spec_declaration checkinvar_declaration ltlspec_declaration compute_declaration fairness_declaration define_declaration isa_declaration FAENZA mm The atom immediately following the keyword MODULE is the name associated with the module Module names are drawn from a separate name space from other names in the program and hence may clash with names of variables and definitions The optional list of atoms in parentheses are the formal parameters of the module Whenever these parameters occur in expressions within the module they are replaced by the actual parameters which are supplied when the module is instantiated see below Chapter 3 Syntax 27 An instance of a module is created using the VAR declaration see Section 3 2 1 State Variables page 23 This declaration supplies a name for
91. rnal SAT solver separately bmc_setup Builds the model in a Boolean Epression format Command bmc_setup h You must call this command before use any other bmc related command Only one call per session is required go_bmc Initializes the system for the BMC verification Command go_bmc h This command initializes the system for verification It is equivalent to the command sequence read_model flatten_hierarchy encode_variables build_boolean_model bmc_setup If some commands have already been executed then only the remaining ones will be invoked Command options h Prints the command usage Chapter 4 Running NuSMV interactively 42 check_ltlspec_bmc Checks the given LTL specification or all LTL Command specifications if no formula is given Checking parameters are the maximum length and the loopback values check_ltlspec_bmc h n idx p formula IN context k max_length 1 loopback o filename This command generates one or more problems and calls SAT solver for each one Each problem is related to a specific problem bound which increases from zero 0 to the given maximum problem length Here length is the bound of the problem that system is going to generate and or solve In this context the maximum problem bound is represented by the k command parame ter or by its default value stored in the environment variable bmc_length The single generated problem also depends on the loopback parameter
92. s in order to reduce the size of the existing BDDs Reordering methods can be activated either Chapter 4 Running NuSMV interactively 51 Reordering of the variables can be triggered in two ways by the user or by the BDD package In the first way reordering is triggered by the interactive shell command dynamic_ var_ordering with the f option Reordering is triggered by the BDD package when the number of nodes reaches a given threshold The threshold is initialized and automatically adjusted after each reordering by the package This is called dynamical reordering and can be enabled or disabled by the user Dynamic reordering is enabled with the shell command dynamic_var_ordering with the option e and disabled with the d option enable_reorder Environment Variable Specifies whether dynamic reordering is enabled when value is 0 or disabled when value is 1 reorder_method Environment Variable Specifies the ordering method to be used when dynamic variable reordering is fired The possible values corresponding to the reordering methods available with the CUDD pack age are listed below The default value is sift sift Moves each variable throughout the order to find an optimal position for that variable assuming all other variables are fixed This generally achieves greater size reductions than the window method but is slower random Pairs of variables are randomly chosen and swapped in the order The swap is perf
93. s 4 at time 4 and at the next step is not 6 Chapter 2 Tutorial 16 bound 0 1 2 3 4 5 0 gt 0 gt 0 gt 0 gt 0 gt o state y 0 y 1 y 2 y 3 y 4 y 5 The output produced by NuSMV shows that before the counterexample of length 5 if found NuSMV also tried to finds counterexamples of lengths 0 to 4 However there are no such coun terexamples For instance in the case of bound 4 the traces of the model have the following form bound 0 1 2 3 4 0 gt 0 gt 0 gt 0 gt o state y 0 y 1 y 2 y 3 y 4 In this situation y gets the value 4 but it is impossible for NuSMV to say anything about the following state In general in BMC mode NuSMV tries to find a counterexample of increasing length and immediately stops when it succeeds declaring that the formula is false The maximum number of iterations can be controlled by using command line option bmc_length The default value is 10 If the maximum number of iterations is reached and no counter example is found then NuSMV exits and the truth of the formula is not decided We remark that in this case we cannot conclude that the formula is true but only that any counter example should be longer than the maximum length system prompt gt NuSMV bmc bmc length 4 modulo8 smv no counterexample found with bound 0 for no counterexample found with bound 1 for no counterexample found with bound 2 for no counterexample found with bound 3 for
94. s from zero 0 to the given maximum problem bound In this short description length is the bound of the problem that system is going to dump out In this context the maximum problem bound is represented by the maz_length parameter or by its default value stored in the environment variable bmc_length Each dumped problem also depends on the loopback you can explicitly specify by the l option or by its default value stored in the environment variable bmc_loopback The property to be checked may be specified using the n idr or the p formula options You may specify dimacs file name by using the option o filename otherwise the default value stored in the environment variable bmc_dimacs_filename will be considered Command options n index index is the numeric index of a valid LTL specification formula actually located in the properties database The validity of index value is checked out by the system p formula IN context Checks the formula specified on the command line context is the module instance name which the variables in formula must be evaluated in k max_length mazx_length is the maximum problem bound used when increasing problem bound starting from zero Only natural number are valid values for this option If no value is given the environment variable bmc_length value is considered instead 1 loopback loopback value may be a natural number in 0 maz_length 1 Positive sign can be also used
95. s satisfying alpha and checks whether it contains the reachable states is the empty set If this is the case then the property is verified else a counterexample is printed forward_search Environment Variable Enables the computation of the reachable states during the process_model command and when used in conjunction with the ag_only_search environment variable enables the use of an ad hoc algorithm to verify invariants check_invar Performs model checking of invariants Command check_invar h m o output file n number p invar expr IN context Performs invariant checking on the given model An invariant is a set of states Checking the invariant is the process of determining that all states reachable from the initial states lie in the invariant Invariants to be verified can be provided as simple formulas without any temporal operators in the input file via the INVARSPEC keyword or directly at command line using the option p Option n can be used for checking a particular invariant of the model If neither n nor p are used all the invariants are checked During checking of invariant all the fairness conditions associated with the model are ignored If an invariant does not hold a proof of failure is demonstrated This consists of a path starting from an initial state to a state lying outside the invariant This path has the property that it is the shortest path leading to a state outside the invariant Command options
96. sign of Integrated Circuits and Systems 13 4 401 424 April 1994 CGH97 E Clarke O Grumberg and K Hamaguchi Another Look at LTL Model Checking Formal Methods in System Design 10 1 57 71 February 1997 CMB90 O Coudert C Berthet and J C Madre Verification of synchronous sequential machines based on symbolic execution In J Sifakis editor Proceedings of the In ternational Workshop on Automatic Verification Methods for Finite State Systems volume 407 of LNCS pages 365 373 Berlin June 1990 Springer Dil88 D Dill Trace Theory for Automatic Hierarchical Verification of Speed Independent Circuits ACM Distinguished Dissertations MIT Press 1988 EMSS91 E Allen Emerson A K Mok A Prasad Sistla and Jai Srinivasan Quantitative temporal reasoning In Edmund M Clarke and Robert P Kurshan editors Pro ceedings of Computer Aided Verification CAV 90 volume 531 of LNCS pages 136 145 Berlin Germany June 1991 Springer McMil92 K L McMillan The SMV system DRAFT 1992 Available at http www cs cmu edu modelcheck smv smvmanual r2 2 ps McMil93 K L McMillan Symbolic Model Checking Kluwer Academic Publ 1993 Mart85 A J Martin The design of a self timed circuit for distributed mutual exclusion In H Fuchs and W H Freeman editors Proceedings of the 1985 Chapel Hill Conference on VLSI pages 245 260 New York 1985 MOONO0 Moon Hachtel Somenzi Border Block Tringular Form and Conjun
97. t of reachable states The result is then used to simplify image and preim age computations This can result in improved performances for models with sparse state spaces Sometimes this option may slow down the performances because the computation of reachable states may be very expensive The environment variable forward_search is set during the execution of this command Chapter 4 Running NuSMV interactively 38 print_reachable_states Prints out the number of reachable states In Command verbose mode prints also the list of reachable states print_reachable_states h v Prints the number of reachable states of the given model In verbose mode prints also the list of all reachable states The reachable states are computed if needed check_trans Checks the transition relation for totality Command check_trans h m o output file Checks if the transition relation is total If the transition relation is not total then a potential deadlock state is shown out Command options m Pipes the output generated by the command to the program specified by the PAGER shell variable if defined else through the UNIX command more o output file Writes the output generated by the command to the file output file At the beginning reachable states are computed in order to guarantee that deadlock states are actually reachable check_trans Environment Variable Controls the activation of the totality check of the transition relation durin
98. tdin Chapter 5 Running NuSMV batch 61 5 Running NuSMV batch When the int option is not specified NuSMV runs as a batch program in the style of SMV performing some of the steps described in previous section in a fixed sequence system_prompt gt NuSMV command line options input file The program described in input file is processed and the corresponding finite state machine is built Then if input file contains formulas to verify their truth in the specified structure is evaluated For each formula which is not true a counterexample is printed The batch mode can be controlled with the following command line options NuSMV s1 ctt 1p n idx v vl cpp is ic ils ii r f int h help i iv_file 0 ov_file AG load script_file reorder dynamic m method mono thresh cp_t cp cpt iwls95 cp_t coil noaffinity iwls95preorder bmc bmc_length k ofm fm_file obm bm_file imput filel where the meaning of the options is described below If input file is not provided in batch mode then the model is read from standard input s Avoids to load the NuSMV commands contained in nusmvrc or in nusmvrc or in NuSMV_LIBRARY_PATH master nusmvrc ctt Checks whether the transition relation is total 1p Lists all properties in SMV model n idx Specifies which property of SMV model should be checked v verbose level Enables printing of add
99. te 1 11 y 2 State 1 12 y 3 State 1 13 y 4 NuSMV gt This picture illustrates the produced counterexample in a more effective way o 12 4 0 gt 0 gt 0 gt 0 gt 0 gt 0 gt 0 gt 0 gt 0 gt 0 gt 0 gt 0 gt bound 0 1 2 3 4 5 6 7 8 9 10 11 y value 0 1 2 3 4 5 6 7 0 1 2 3 If no loopback is specified NuSMV is not able to find a counterexample for the given liveness property system_prompt gt NuSMV int modulo8 smv NuSMV gt go_bme NuSMV gt check_ltlspec_bmc_onepb k 12 1 X no counterexample found with bound 12 and no loop for NuSMV gt Chapter 2 Tutorial 20 Bounded Model Checking in NuSMV can be used not only for checking LTL specification but also for checking invariants An invariant is a propositional property which must always hold BMC tries to prove the truth of invariants via an inductive reasoning by checking if i the property holds in every initial state and ii if it holds in any state reachable from any state where it holds Let us modify file modulo8 smv by replacing the LTL specification with the following in variant specification INVARSPEC y in 0 12 and let us run NuSMV in BMC mode system_prompt gt NuSMV bmc modelo8 smv cannot prove the invariant y in 0 12 the induction fails as demonstrated by the following execution sequence State 1 1 y 12 State 1 2 y 13 system_prompt gt NuSMV reports that the given invariant
100. ted until no further improvement is obtained annealing This method is an implementation of simulated annealing for variable order ing This method is potentially very slow genetic This method is an implementation of a genetic algorithm for variable ordering This method is potentially very slow exact This method implements a dynamic programming approach to exact reorder ing It only stores a BDD at a time Therefore it is relatively efficient in terms of memory Compared to other reordering strategies it is very slow and is not recommended for more than 16 boolean variables linear This method is a combination of sifting and linear transformations linear_conv The linear method is iterated until no further improvement is obtained dynamic_var_ordering Deals with the dynamic variable ordering Command dynamic_var_ordering d e lt method gt f lt method gt h Controls the application and the modalities of dynamic variable ordering Dynamic ordering is a technique to reorder the BDD variables to reduce the size of the existing BDDs When no options are specified the current status of dynamic ordering is displayed At most one of the options e f and d should be specified Dynamic ordering may be time consuming but can often reduce the size of the BDDs dramatically A good point to invoke dynamic ordering explicitly using the f option is after the commands build_model once the transition relation has bee
101. the instance and also a list of actual parameters which are assigned to the formal parameters in the module definition An actual parameter can be any legal expression It is an error if the number of actual parameters is different from the number of formal parameters The semantic of module instantiation is similar to call by reference For example in the following program fragment MODULE main VAR a boolean b foo a MODULE foo x ASSIGN x 1 the variable a is assigned the value 1 This distinguishes the call by reference mechanism from a call by value scheme Now consider the following program MODULE main DEFINE a 0 VAR b bar a MODULE bar x DEFINE a a y i X In this program the value of y is 0 On the other hand using a call by name mechanism the value of y would be 1 since a would be substituted as an expression for x Forward references to module names are allowed but circular references are not and result in an error 3 2 10 Identifiers An id or identifier is an expression which references an object Objects are instances of modules variables and defined symbols The syntax of an identifier is as follows tds atom self id atom id simple_expr An atom identifies the object of that name as defined in a VAR or DEFINE declaration If a identifies an instance of a module then the expression a b identifies the component object named b of instance
102. tion Variables that become adjacent during sifting are tested for symmetry If they are symmetric they are linked in a group Sifting then continues with a group being moved instead of a single variable symmetry_sift_converge The symmetry_sift method is iterated until no further improvement is obtained window2 3 4 Permutes the variables within windows of n adjacent variables where n can be either 2 3 or 4 so as to minimize the overall BDD size window2 3 4_converge The window2 3 4 method is iterated until no fur ther improvement is obtained group sift This method is similar to symmetry sift but uses more gen eral criteria to create groups group sift_converge The group sift method is iterated until no further improvement is obtained annealing This method is an implementation of simulated annealing for variable ordering This method is potentially very slow genetic This method is an implementation of a genetic algorithm for variable ordering This method is potentially very slow exact This method implements a dynamic programming approach to exact reordering It only stores a BDD at atime Therefore it is relatively efficient in terms of memory Compared to other reordering strategies it is very slow and is not recommended for more than 16 boolean variables linear This method is a combination of sifting and linear transformations linear_converge The linear method is iterated until no further improve ment is o
103. tions h Prints the command usage exits NuSMV Command quit h s Stops the program Does not save the current network before exiting Command options 8 Frees all the used memory before quitting This is slower and it is used for finding memory leaks reset Resets the whole system Command set reset h Resets the whole system in order to read in another model and to perform verification on it Command options h Prints the command usage Sets an environment variable Command set h lt name gt lt value gt A variable environment is maintained by the command interpreter The set command sets a variable to a particular value and the unset command removes the definition of a variable If set is given no arguments it prints the current value of all variables Command options h Prints the command usage lt name gt Variable name Chapter 4 Running NuSMV interactively 57 lt value gt Value to be assigned to the variable Interpolation of variables is allowed when using the set command The variables are referred to with the prefix of So for example what follows can be done to check the value of a set variable NuSMV gt set foo bar NuSMV gt echo foo bar The last line bar will be the output produced by NuSMV Variables can be extended by using the character to concatenate values For example NuSMV gt set foo bar NuSMV gt set foo foo foobar
104. to be picked using command pick_state A simulation session can be started now using the simulate command Consider for instance the following simulation session system_prompt gt NuSMV int short smv NuSMV gt go NuSMV gt pick_state r NuSMV gt print_current_state v Current state is 1 1 request 0 state ready NuSMV gt simulate r 3 ee Starting Simulation From State 1 1 kx NuSMV gt show traces t There is 1 trace currently available NuSMV gt show traces v HHHHHHHHHHHHHHHHHHHE Trace number 1 ttt gt State 1 1 lt request 0 state ready gt State 1 2 lt request 1 1 We assume that every NuSMV command is followed by a keystroke In the following examples NuSMV commands are written in a bold face to distinguish them from system output messages Chapter 2 Tutorial 8 state busy gt State 1 3 lt request 1 state ready gt State 1 4 lt request 1 state busy Command pick_state r requires to pick the starting state of the simulation randomly from the set of initial states of the model Command simulate r 3 asks to build a three steps simulation by picking randomly the next states of the steps As shown by command show traces v the resulting trace contains 4 states the initial one and the three ones that have been added by the random simulation We remark that the generated traces are numbered every trace is identified by an integer number while every state belonging to a trace is i
105. value may be a natural number in 0 maz_length 1 Positive sign can be also used as prefix of the number Any invalid combination of length and loopback will be skipped during the generation solving process a negative number in 1 bmc_length In this case loopback is considered a value relative to length Any invalid combination of length and loopback will be skipped during the generation solving process the symbol X which means no loopback the symbol which means all possible loopback from zero to length 1 o filename filename is the name of the dumped dimacs file It may contain special symbols which will be macro expanded to form the real file name Possible symbols are F model name with path part f model name without path part k current problem bound l current loopback value n index of the currently processed formula in the properties database the character Chapter 4 Running NuSMV interactively 44 gen_Itlspec_bmc Dumps into one or more dimacs files the given LTL Command specification or all LTL specifications if no formula is given Generation and dumping parameters are the maximum bound and the loopback values gen_ltlspec_bmc h n idx p formula IN context k max_length 1 loopback o filename This command generates one or more problems and dumps each problem into a dimacs file Each problem is related to a specific problem bound which increase
106. y in the formula E a BU m n b m n resp represents the minimum maxi mum number of permitted transition along a path of a structure before the eventuality holds Real time CTL specifications can be defined with the following syntax which extends the syntax for CTL specifications spec_declaration SPEC rtctl_expr With the COMPUTE statement it is also possible to compute quantitative information on the FSM In particular it is possible to compute the exact bound on the delay between two specified events expressed as CTL formulas The syntax is the following compute_declaration COMPUTE compute_expr where Chapter 3 Syntax 32 compute_expr MIN rtctl_expr rtctl_expr MAX rtctl_expr rtctl_expr MIN start final computes the set of states reachable from start If at any point we encounter a state satisfying final we return the number of steps taken to reach the state If a fixed point is reached and no states intersect final then infinity is returned MAX start final returns the length of the longest path from a state in start to a state in final If there exists an infinite path beginning in a state in start that never reaches a state in final then infinity is returned Chapter 4 Running NuSMV interactively 33 4 Running NuSMV interactively The main interaction mode of NuSMV is through an interactive shell In this mode NuSMV enters a read eval print loop The
107. y and request is 1 i e true Otherwise the 1 before the column the next value for state can be any in the set ready busy The variable request is not assigned This means that there are no constraints on its values and thus it can assume any value request is thus an unconstrained input to the system The following program illustrates the definition of reusable modules and expressions It is a model of a three bit binary counter circuit The order of module definitions in the input file is not relevant MODULE counter_cell carry_in VAR value boolean ASSIGN init value 0 next value value carry_in mod 2 DEFINE carry_out value amp carry_in MODULE main VAR bitO counter_cell 1 bit counter_cell bit0 carry_out bit2 counter_cell bit1 carry_out The FSM is defined by instantiating three times the module type counter_cell in the module main with the names bit0 bit1 and bit2 respectively The counter_cell module has one formal parameter carry_in In the instance bit0 this parameter is given the actual value 1 In the instance bit1 carry_in is given the value of the expression bit0 carry_out This expression is evaluated in the context of the main module However an expression of the form a b denotes component b of module a just as if the module a were a data structure in a standard programming language Hence the carry_in of module bit1 is the carry_out of module bit0 The k

NuSMV 2.1 User Manual

Contents

Download Pdf Manuals

Related Search

Related Contents