Home

STeP The Stanford Temporal Prover Educational Release USER`S

1.
2.
3.
4. Figure 1 2 Overview of sTeP s interfaces 1 3 INTERACTING WITH STEP 5 Verification Session An Overview A verification session begins by loading a program or a transition system that describes the system of interest and entering a temporal logic formula that expresses one or more system properties to be proved The formula becomes the top or root goal of a proof tree There are now several ways to proceed The most common route is to apply a verification rule Section 4 2 which reduces the formula to simpler first order or temporal formulasl
5. e STeP HT File Properties Tactics Diagrams Logical rules Settings Help Quit mux sem spl 1 goal Equality Auto OFF flo y Previous B INV G INV B WAIT G WAIT B CAUS G CAUS B BACKTO G BACKTO e Interactive Prover E Refresh Tactics Settings Select goal Help Quit Modelcheck Current goal oaeienec hide Unhide Simplify Simplify Diagram Editor B ooo 1 Step Propositional File Edit Node Edge Help Exit STeP e Program mux sem spl E local y int where y 1 Pis Make first order wile rue do I1 noncritical 12 request y Cut onto zyma n BM d i 1 A m Y All Propositional E K0 2 m 0 2 Ay 1 m0 while true do BDD split m1 noncritical Add Axiom a m2 request y m3 critical PTL expansion Y l4 m4 release y 1 phil K3 4 Am 0 2 A y 0 1 ooo S7eP
6. m4 phi2 IOVITVIZ A m3Vm4 A y 0 Figure 9 8 Invariance verification diagram for MUX SEM 99 100 CHAPTER 9 BASIC TUTORIAL The first two subgoals are side verification conditions They state that the label on each of the nodes implies the invariant to be provenl and that the initial condition implies the label of one of the nodes Then the verification conditions corresponding to each of the edges in the diagram are simplified including those for the implicit self loops In this casel all verification conditions simplify to true even without the linear arithmetic decision procedures l and the proof is complete 9 2 5 Using MON I and Linear Invariants Finally we show how we can prove i based on y and automatically generated linear invariants 1 Load the examples mux sem spl program and prove y O y gt 0 using B INVI as described in Section 9 2 1 2 Load the goal p from examples mux spec 3 Select the Get global linear invariants option under the Properties menu This will automatically generate a number of linear invariants which are added to the set of background propertiesl including oth h m3 m4 y Your set of background properties should now contain this formulal as well as yy 4 Make sure that linear decision procedures are enabled with the Simplification Flags option under the Settings menu 5 Select the MON I rule under the Logical rules menu Thi
7. After calling the core model checkerI the log file will contain the list of relevant sys tem variablesI the preprocessed transition system some statistical informationl andl if the formula proved to be invalidl a counterexample computation Environment Variables The search space may be infinite if there are system variables that range over an infinite domainl and in this case the Model Checker may or may not terminate Even if the system is finite statel the state space may prove too large for the time and memory available The following settings can be used to limit the Model Checker resources e STEP MC SPACE Maximum amount of memorylI in Megabytes Default unlimited e STEP MC TIME Maximum amount of user timel in minutes Default unlimited e STEP MC CPU Maximum amount of CPU timel in minutes Default unlimited The Model Checker can be interrupted with sTeP s interrupt button the sTeP logo NOTE This may leave a UNIX process running in the background see the UNIX kill man pages for details on how to kill runaway processes Chapter 5 The Verification Diagram Editor Verification diagrams are a visual representation of a proof A verification diagram describes sets of states given by assertions and possible transitions between them A well formed verification diagram represents a set of verification conditions that are sufficient to establish a given temporal formula Verification diagrams are described in detail
8. Tthe verification condition is terrier No verification conditions are associated with terminal nodes A diagram is called valid over program P P valid if all the verification conditions associated with nodes of the diagram are P state valid Thus a valid diagram provides a succinct representation of the verification conditions of the form v r vH for all combinations of assertions y and v and transitions 7 that appear in the diagram 5 2 Wait for Diagrams A verification diagram is called a WAIT FOR diagram if there is only one terminal node and it is labeled by o and the diagram is weakly acyclicl i e D whenever node i is connected by an edge to node q I gt j P valid WAIT FOR diagrams can be used to establish the P validity of a nested wait for formula A P valid WAIT FOR diagram establishes that the formula ai gt Qu ena IW Yo j 0 is P valid To establish the P validity of P ImWam 1 Wao the following additional verification conditions referred to as side verification conditions have to be established gi gt qi fori 0 1 m W2 5 3 Invariance Diagrams A verification diagram is called an INVARIANCE diagram if it is exit freel i e l it has no terminal node Unlike wAIT FOR diagramsl INVARIANCE diagrams may contain cycles A P valid INVARIANCE diagram with nodes 1 m establishes that the formula 5 4 CHAIN DIAGRAMS x 61 is P valid To establish the validity of 1g t
9. Tuple indices are counted from 1I i e l the first element in a tuple has index 1 2 3 SPECIFICATION FILES 17 of array bind bo then alse E CC ponas Table 2 1 Operator precedences from lowest to highest binding The binding operators ForalllExistsl and Exists correspond to Yrd and d unique existence respectively They bind the variables in their scopel so for instance in Forall x int p x the variable x is bound by the quantifier Forall The binding operators Sum and Prod correspond to the arithmetic operators X and II and bind variables similarly As the syntax indicatesl the type field of the bound variables is optional If no type is givenI where the variable is boundI the variable must have been declared before using a variable declaration priming The primed verision of a flexible variable refers to its value at the next state The parser accepts primed expressionsl and automatically distributes the prime inwards to all its flexible variables Double priming is not supported and results in a parser error The precedence of the various operators is given in Table 2 1 2 3 Specification Files A specification file usually contains three parts declarationsl axioms and properties 1 The declarations define new typesI valuesl macrosl rewrite rulesl and auxiliary vari ables 18 CHAPTER 2 SYSTEMS AND SPECIFICATIONS 2 The axioms define properties that may be assumed by sTeP in a ve
10. Stickel 1989 P McCuneT 1992 ZhangI 1993 6 2 BDD Simplification sTeP includes a package for the creation and manipulation of propositional i e boolean formulas using Binary Decision Diagrams BDDs This package is used in the proof rule as well as in boolean simplification steps Since the amount of memory used by the BDD package can grow indefinitely in the form of accumulated BDD nodes Tthe package can be reset at any time with the Reset BDDs option under the Settings menu This only incurs a usually small short term efficiency lossl and does not affect the soundness of the prover T his option should also be used if the number of BDD nodes reaches the maximum given by the STEP BDD NODES environment variable see Appendix E The number of existing BDD nodes can be obtained through the Sytem Information option A number of environment variables control the amount of memory that BDDs use e STEP BDD NODES The maximum number of BDD nodes kept around at one time e STEP BDD CACHE The size of the BDD result cache e STEP BDD SPLIT The maximum number of subgoals that can be generated by a BDD split operation in both the Top level and Interactive Provers see Section 6 2 1 below For more information on BDDsI see Bryantr1986r Bryantr 1992 6 2 1 BDD split The BDD split proof rule uses BDDs to convert the current goal into a list of subgoalsI each a disjunction of atomic formulas The subgoals correspond to t
11. when statement while statement repeat statement infinite loop block statement grouped statement parameterized selection parameterized cooperation l way conditional 2 5 SPL PROGRAMS basic_group_stmt assignment n left val variable binding N params N param N label n ids decl system var decl mode if p_expn then comp_group_stmt else comp_group_stmt when p_expn do comp_group_stmt comp_group_stmt or comp_group_stmt comp_group_stmt comp_group_stmt skip assignment await p_erpn variable lt p_expn variable gt variable left val p expn id id p_expns p exrpn id params params param param id range id id id type decl datatype decl value decl macro decl system var decl mode ids type where expn in out 1ocal 27 2 way conditional when statement selection statement concatenation skip statement await statement send statement receive statement assignable value variable array variable named binding unnamed binding list of parameters parameter label list of identifiers SPL declaration basic variable declaration mode of variable Assignable expressions are built from system variables declared as local or outl and ar ray references to local or out arrays Composite assignable expressions are obtained by collecting simpler assignable expressions into tuples Example An example of a c
12. y1 gt 0 PROPERTY aux2 y2 gt 0 PROPERTY aux3 gcd y1 y2 gcd a b PROPERTY partial correctness 18 gt g gcd a b Figure 2 1 Specification file with multiple axioms and properties 2 4 Declarations Declarations can be in one of the following formsI which we describe below 2 4 DECLARATIONS 19 declaration i type decl datatype decl declaration of types value decl macro decl declaration of constructs aux var decl system var decl declaration of variables simplify rewrite order rewrite rules 2 4 1 Type Declarations Type declarations are used to define abbreviations for compound types new underspecified typesl and new datatypes Type abbreviations are declared as type id typel where type is a type expression see Section 2 1 Omitting and the type expression declares id as a newl underspecified type type decl type id type type declaration type id ids enumeration type type id underspecified type identifier Datatype Declarations Datatypes are declared using instead of a single T with the following syntax datatype decl type id constructors and id constructors datatype declaration constructors constructor constructor constructor id deconstructors j constructor id and fields deconstructors id type id type datatype deconstructors The enumeration type declaration type id id idp is shorthand for the datatype de
13. 1 of bool int int is parsed as channel 1 of bool int int Note that bool int int I bool int int and bool int int are three different types New underspecified types datatypes and enumeration types can be declared in specifi cation files see Section 2 4 1 2 2 Expressions Expressions are constructed from constantsI identifiersl function applicationl array refer ences tuple expressions binary infix expressionsl prefix expressions and quantification The following well formedness constraints are imposed e The boolean type is treated as a subtype of the integersl where the boolean value false corresponds to the integer value Oland true corresponds to 1 Therefore any expression of boolean type can be used in an integer context This is referred to as arithmetization rationals type rat Similarly the integers type int are treated as a subtype of e The operators conjunction T V disjunction I implication lt gt bi implication T negation land the temporal operators Until Awaits Since Backto gt lt gt O O lt gt lt gt take boolean argumentsl and the resulting ex pression is of type boolean e The operators require integer or rational arguments and produce a value of the corresponding type Division requires arguments of type integer or rationall and results in a value of type rational The operators mod and div require argu
14. Nj 4n flength send length ack I3 m2 Nj Transition I1 Just enable pi0 0 modrel Q0 x assign pi 1 preloc 10 postloc l2 length send length ack I3 m2 N 5 l2 length send length ack I3 m2 Nj Transition I2 Just enable 0 length ack A pid 1 assign pi 2 t head ack ack tail ack preloc I2 postloc I3 flength send length ack I3 m2 Nj Figure 3 7 Goal selection window 44 CHAPTER 3 THE TOP LEVEL INTERFACE Select search Generalizes Next search above to move to any other proof tree A window listing the root nodes of all proof trees is displayed See Figure 3 8 for an example By clicking on the buttonIthe corresponding proof tree is made the current proof tree aux3 lgcd y1 y2 gcd a b part corr I8 gt g gcd a b Cancel Figure 3 8 Proof tree selection window No window will appear if there is nothing to select Abandon search Deletes the current proof tree and makes the next proof tree in the list if anyl the current proof tree A confirmation window appears before this action is taken The following options generate program invariants When the invariant generation is doneT the invariants are displayed in the output window and added to the list of background properties By default they are activel and thus used in the simplification of goals They may be deactivated with the Activate Deactivate menu option above When t
15. Weakest Precondition p Y which implies the original verification condition The symbol p refers to the transition relationl and is the logical form of the transition T The formula y is the primed version of Tin which each system variable occurring free in has been replaced by its primed version Appendix A describes transitions and transition relations in more detail The strengthening rule can be used to strengthen a property that is not inductive The rule is applicable to subgoals of the form teirtys and when applied it generates the subgoal pA pr gt wv while deleting the original verification condition and its siblings from the proof tree 4 4 Logical Rules The Logical rules pull down menu provides inference rules that allow the derivation of new properties from previously proven properties If the current formula does not match the kind of formula that the given rule applies tol a message will appear in the bottom help windowl and the given function will have no effect MON I The monotonicity rule for invariances can be used to prove a property of the form pl where p is a state formula If the current goal is pI the following subgoal is generated Avi p t where y ranges over all the currently active in the background properties 56 CHAPTER 4 VERIFICATION AND LOGICAL RULES TRN C The transitivity of causality rule proves a causality property from two ot
16. of the subgoals System Description and Specification STeP accepts a system description in two different formats namely as an SPL program or as a fair transition system Specifications are entered as linear time temporal logic formulas SPL program A system description may be given in the form of an SPL program Simple Programming Language program The syntax of well formed SPL programs is given in Section 2 5 SPL programs are parsed into fair transition systems The semantics of SPL are given in Appendix A Fair transition system An alternative way to provide a system description is by means of a fair transition system A fair transition system is a tuple with the following components e VTa set of system variables These include all program variables e Ol the initial condition e 7 Ta set of transitions Each transition is a relation between statesI specifying how the system can move from one state to the next Section 2 6 describes how transition systems are specified in STeP Appendix A describes fair transition systems in more detail Auxiliary and system variables Auxiliary variables are declared in specifications Sys tem variables get declared in system descriptions and participate in the transition relations of the described transition system 10 CHAPTER 1 INTRODUCTION Flexible and rigid variables The value of a flexible variable may change over timel while that of a rigid variable is assumed to be fixed throughout a co
17. otherwise tactic tactic tactic tactic tactics n tactic tactic 1 form depth first breadth first atomic atomic tactic The grammar for atomic tactic for the Top level Prover is given in Section 6 3 2 the grammar for the Interactive Prover atomic tactics is given in Section 6 3 3 The curly brackets can be omitted if the atomic tactic can be written without spaces In other casesI curly brackets have to enclose each atomic tactic 6 3 TACTICS x 73 6 3 1 Composition Options When a verification rule is applied to a goal to which it does not syntactically make sense for example B INV applied to a response formula it fazlsl otherwise it succeeds Tactics which are composed from verification rules can also fail and succeed as described below try tacl tac2 tac3 Try tactic taciTif it succeedsl apply tac2 to each subgoal generated If tac fails apply tactic tac to the original goal The entire tactic fails if tac2 fails on one of the generated subgoals of tacil or tac3 fails Figure 6 2 gives an idea of how the proof search looks like after tac and tac2 have been applied successfullyl or tac failed and tac has been applied The lower most dot represents the original goalIl the first left most layer of dots represent the subgoals generated from taciI the second left most layerl the subgoals generated from tac2 To the right is a schematic representation of the subgoals generated by tac3
18. 18 release r Figure 2 5 Program DINE dining philosophers Program variables As in most imperative languages program variables must be declared prior to their usel in the appropriate scope SPL provides an additional mode associated with the declaration of program variables A variable declared as in is an input to the program it may not be modified by any of the program statementsl and is assumed to have a fixed value throughout the program execution Variables declared as 1ocal or out may be changed by the program Variables may be initialized or constrained with an optional where clause The given condition is assumed to hold only at the start of the programI not each time the program enters the block where the variable is declared Parameterized programs SPL allows you to write parameterized N process programslin which an arbitrary number of identical processes are declared Both parameterized composition and parameterized selection are supported Example Figure 2 5 shows a deadlock free solution to the N process Dining Philosophers prob lem The program contains N instances of the infinite loop 10 18l each with its unique value of i Grouped statements A grouped statement is a set of statements enclosed by lt lt and gt gt A grouped statement is translated into a single transitionI that isl one atomically executable unit Grouped 26 CHAPTER 2 SYSTEMS AND SPECIFICATIONS statements may only contain basic s
19. Converts the selected node only one node should be selected into a terminal node The borders of the node are drawn with thick lines and the node is declared as terminal Nonterminal Converts a selected terminal node into a nonterminal node The Edge Menu The Edge menu lets you change the fairness requirements associated with a selected edgel and check that all edges are properly connected to the nodes Cut Head Cuts the head hop of a selected edge The head hop is the hop with an arrow where an edge ends 5 7 HIERARCHICAL VERIFICATION DIAGRAMS x 67 Cut Tail Cuts the tail hop of a selected edge The tail hop is the hop where an edge starts Merge Merges a selected edge with the edges chained to it Two edges are considered chained if one s ending point is close to the other s starting point Unjust Converts a selected edge into an Unjust edge Unjust edges are drawn with thin black lines Just Converts a selected edge into a Just edge Just edges are drawn with double lines Compassionate Converts a selected edge into a Compassionate edge Compassionate edges are drawn with thick black lines Connectivity Highlights those edges whose ends are not connected to nodes This is a convenient way to check whether all edges are connected properly in the verification diagram Global Hookup Checks and hooks up all loose edges An edge will be hooked up to a node if its end is close enough to or inside the node Help Activa
20. In sTeP we identify the following sub systemsI each of which operates relatively indepen dently of the rest Top level Prover Chapter 3 The Top level Prover is the main interface to a sTeP sessionl from which all other activities are initiated Interactive Prover Chapter 8 The Interactive Prover is invoked from the Top level Prover to prove a particular goal or subgoal When the Interactive Prover is active the Top level Prover is suspended The Interactive Prover provides a Gentzen style proof systemI which is guided by the user While the Interactive Prover is normally used to complete the proof of a given subgoall partial results from the Interactive Prover can also be transferred back to the Top level Prover Verification Diagram Editor Chapter 5 The Verification Diagram Editor is also in voked from the Top level ProverI but can be run concurrently with it It is used to create and edit verification diagramsI which can be given to the Top level Prover to use in a proof Model Checker Section 4 5 The Model Checker can be invoked from the Top level Prover on any given temporal subgoal If the Model Checker establishes the P validity of the formulal the corresponding goal is proved Otherwisel a counterexample com putation i e one that violates the formula is returned Simplifier Section 6 1 The Simplifier is a collection of decision procedures and rewrite rules used to reduce and prove general verification conditions The Simp
21. OFFl a verification rule only generates subgoalsI but does not simplify them These then have to be manually simplified by successive clicks on Simplify Por with the Interactive Prover If you unintentionally invoke a verification rule with automatic simplification OFFl you can click on Undol turn automatic simplification ONT and apply the rule again 4 2 Verification Rules This section describes the verification rules available in sTeP In the following descriptionI O refers to the initial condition of the current program or transition systeml and 7 refers to its set of transitions see Appendix A For a formula pr po is the initial version of pr that isl the first order formula equivalent to p at the initial state of the computation As usuall the notation p r qM stands for the verification condition p p gt q The inverse verification condition p r q Tis equivalent to q r p T giving an alternate presentation of verification conditions Below we try to use the most convenient one in each case The notation pY7 q stands for the set of verification conditions p r q for each transition 7 in the system similarly p 7 q is the set p r q for each r Verification conditions of the form a gt are replaced by a D when a and D are assertions that isl state formulas with no temporal operators In this casel the P validity 4 2 VERIFICATION RULES 53 of a B implies that of a gt p If this P validity can
22. SEM proving 0 lt y using rule INY H Simplifying Monotonicity simplified to TRUE Simplifying Initial Condition simplified to TRUE Simplifying idle simplified to TRUE Simplifying 10 simplified to TRUE Simplifying I simplified to TRUE Simplifying I2 simplified to TRUE Simplifying I3 simplified to TRUE Simplifying I4 simplified to TRUE Simplifying m0 simplified to TRUE Simplifying m1 simplified to TRUE Simplifying m2 simplified to TRUE Simplifying m3 simplified to TRUE Simplifying m4 simplified to TRUE The proof is COMPLETE Figure 9 4 Verification of y gt 0 for MUX SEM roperty Checklist Figure 9 5 Background properties 96 CHAPTER 9 BASIC TUTORIAL As when loading a file you can select an existing filename or enter a new one The default extension for saved proofs is search The window also allows you to enter three lines of text that will be added to the top of the file as a comment FinallyI click on to save your proof Figure 9 6 shows the format of the saved proof 4 Proof of y gt 0 for program mux sem with decision 4 procedures for linear arithmetic turned on using rule B INV Formula abbreviations phio O lt y Reduced via INV O lt y given the strengthening formula 0 lt y 1 Established via Simplify true 2 Established via Simplify y 1 N piO O pil 0 gt 0 lt y 3 Established via Simplify phiO idle phio 4 Established via
23. Verification Rules ee 52 4 5 WPC and Strengthening 2 e 55 4 4 Logical Rules ese 55 4 5 The Model Checker 2 0 2 ss 56 ii CONTENTS 5 The Verification Diagram Editor 59 5 1 Definitions 4 22 llle le on 59 5 2 Wait for Diagrams saasaa 60 5 3 Invariance Diagrams 4 2l eee 60 5 4 Chain Diagrams 4 a 61 5 5 Compound Nodes 22222 lle ss 62 5 6 Verification Diagram Editor Interface lees 64 5 7 Hierarchical Verification Diagrams x eee 67 6 Automatic Theorem Proving 69 6 1 The Automatic Simplifier 2 0 20 0 20 02 0200 02020200 69 6 2 BDD Simplification lll ee 71 6 2 1 BDD splitx 2 20 00 0020 ss 71 6 3 Tactics x ll e e ee hh ee 72 6 3 1 Composition Options 22e 73 6 89 2 Top level Prover Tactics 2 2 15 6 8 8 Interactive Prover Tactics 2e 75 6 9 4 Interrupting Tactics lle TT 6 3 5 Commonly used Tactics 2s 77 7 Automatic Generation of Invariants 79 7 1 Local Invariants 4 2 2 2222 2l lle ee 79 7 2 Linear Invariants 2 ee 80 7 3 Polyhedral Invariants 2 len 80 8 The Interactive Prover 81 8 1 Proof Structure 22e ll ee 81 8 2 User Interface 4 2 ee 82 8 3 Interactive Prover Rules ee 84 9 Basic Tutorial 91 9 1 Preliminaries 4 ees 91 9 2 MUX SEM Mutual Exclusion 0 000002 ee ee eee 92 9 2 1 Using BINV less 93 9 2 2 Using G INV l
24. a dialog window will appear in which you can enter the variable you want to do induction on The variable has to be a universally quantified integer variable The button implements the inference rule T A p 0 D A Forallx int x gt 0 A p p x 1 T gt A Forall x int x lt 0 Np x p x 1 T A Forall x int p x where p is a formula containing x supports simple mathematical induction for free variables Suppose that the integer variable x occurs free in the sequent T AT which we recall corresponds to a formula px A v2 V da 4 z er r C A Since z is implicitly universally quantified it makes sense to formulate the induction principle p 0 Forall x int x gt 0 p x p x 1 Forall x int x lt 0 p x gt p x 1 r A Decides formulas of Presburger arithmetic Formulas belonging to Presburger arithmetic may involve integer valued variablesl additionI multiplication by constants boolean connectivesl and quantifiers over integer variables The decision problem is super exponentiall and thus only works on small examples It is seldom needed in practicel as the decision procedure cannot handle uninterpreted function symbols e g l arrays Example The following are Presburger formulas Forall x int Exists y int x y gt 0 Exists x int Forall y int Exists z int x yMx amp yMaz amp y x wN 55z x T
25. assign gcd x Figure 2 8 Transition system obtained from the Euclid SPL program Figure 2 7 2 6 2 Transition System Syntax The syntax of transition systems is given by the following grammar transition system Transition System 32 decl system var decl mode initial progress transition relation name params fairness assignment left val CHAPTER 2 SYSTEMS AND SPECIFICATIONS decl initial transition Clocked Transition System decl initial progress transition type decl datatype decl value decl macro decl system var decl mode ids type where expn clock ids where expn in out local Initially ezxpn Progress expn Transition name params fairness relation relation modvar ids enable expn modrel expn assign assignment assignment id id type id type Justice Compassionate NoFairness left val expn expn Assignable expressions are built from system variables declared as 1ocall out or clockl as well as array references to local or out arrays 2 6 3 Clocked Transition Systems x Clocked transition systems Kesten et al T1996 can be used to model discrete or continuous real time systemsl and are partially supported in the educational release of sTeP Clocked transition systems differ from fair transition systems in the following ways e There are designated clock variables T global time a
26. component circuit designs parameterized N process programsl and programs with infinite data domains Finite state systems can be automatically verified using model checking alone For large finite state or for infinite state systemslI for which model checking is not possible or feasible STeP also uses deductive methods Verification rules Manna and Pnuelil 1995 reduce temporal properties to first order verification conditions Verification diagrams Manna and Pnuelil1994 are a visual language for guidingl organizing and displaying proofs They can be used to construct proofs hierarchically starting from a high level sketch and proceeding incrementally through layers of greater detail sTeP also includes techniques for automatic invariant generation Bjorner et al D1995 Deductive verification almost always relies on findingI for a given program and specificationI suitably strong invariants and intermediate assertions The system generates bottom up invariants automatically by analyzing the program text Combining them with the property to be provedI sufficiently detailed invariants can often be obtained to carry through the verification process Finally step provides a collection of simplification and decision procedures that au tomatically check the validity of a large class of first order and temporal formulas This degree of automated deduction can handle many of the verification conditions that arise in deductive verification Figure 1 1
27. control moves from f to The enabling condition of T is at Ar which does not depend on the value of c Note that the locations and lare equivalent e When With the statement when c do we associate a transition r l with the transition relation pe A move C 0 pres Ys According to p when c evaluates to true control moves from to l e Or No special transition is associated with the statement 59 or S2 When control resides at this statementI it is interpreted to reside simultaneously at the starting points of Sy and So e Cooperation With the statement S 4 o S2 a n Sani fn we associate two transitions T and Tepa with transition relations Dig movell 4 l2 ln A pres Ys Pg move s b D hh pres Ys All they do is to move control from the guarding location into the prelocation of each parallel statementDl and from the post location of each parallel statement to the post location of the entire statement STeP makes a special case for parallel composition at the top level of the program They do not get a designated pre and post locationI but the initial state is instead what corresponds to 1 5 in the schema e Concatenation No special transition is associated with sequential composition of statements 51 S2 Since the post location of S is the pre location of 55 the transitions generated from each substat
28. diff inc dine dine contr dine excl double Figure 3 3 File Browser If a file does not parse correctlyl a Read Error window will appear with an indication f the first parsing error encountered The file can be corrected and read again by clicking Oo ry same file again Tor the operation canceled with Cancel Load program Loads an SPL program from a file The default extension for a program file is spl The program will be parsed into a fair transition system The program text is displayed in a separate window setting the STEP_SHOW_LOADED environment variable to OFF disables this see Appendix E The program text window may be deleted at any time by clicking Quit r and redisplayed with the View program text option below Figure 3 4 shows the program window for program MUX PETI The program window also displays the correspondence between the program locations and the value of the internal control location variable Control locations are explained in detail in Appendix C 2 If Load program is selected while another verification session is still in progressl a confirmation window will first appear The entire verification session environment is reset when a new program is loadedI i e l all background properties and unproven goals are deleted Load transitions The Load transitions option works like Load programI but expects a tran sition system file The default extension for transition system files is trans Th
29. do mo loop forever do fi noncritical m noncritical fo request y zu mg request y ls critical critical f4 release y release y Figure 1 3 Program MUX SEM mutual exclusion by semaphores Consider program MUX SEMI shown in Figure 1 3 It implements mutual exclusion using the semaphore yl request decrements the semaphorel when it is positivel and release imcrements the semaphore We want to prove the following properties of this program p Oly 0 2 LI s ma The first propertyI stating that y is always greater than or equal to Ol is proved automatically using rule B INV Section 4 2 and decision procedures for linear arithmetic The property is then added to the list of background properties and may be used in subsequent proofs The second property expresses mutual exclusion and is not inductive that isl it is not preserved by all transitions In particular the verification conditions for transitions 9 and mg are not validl and indeed when we apply rule B INV the Simplifier does not reduce them to true We now have several options Since this is a finite state program with a small number of states model checking has a good chance of succeeding indeed the Model Checker can quickly verify this property Another option is to generate some auxiliary invariants One of the linear invariants automatically generated for this system is I Ollo 44 9 ms t ma y Unfo
30. integer variables in the induction duplicates formulas at indicated positions duplicates formulas at indicated positions hides formulas at indicated positions unhides formulas located at their hidden positions Instantiate existential force quantifiers at indicated positions by the listed expressions Replace at i val left by right Replace at i val right by left Skolemize Skolemize Skolemize position ezpn position i val i val i val 1 In both cases 7 val must be lt 0 expn at position 6 3 TACTICS x TT expn poss n f expn at position If a p rule is given without argumentslI it is applied exhaustively in a breadth first manner 6 3 4 Interrupting Tactics Tactics are not guaranteed to terminatel or can otherwise run for a very long time the interrupt button the sTeP logo is useful to stop the execution of a batchmode tactic Two things can actually happen if the interrupt button is pressed during the execution of a tactic if the interrupt button is activated during a simplification stepI the simplification will be canceled and the system will continue with the next one if the system is interrupted when no simplification is going onI the entire tactic will be interrupted 6 3 5 Commonly used Tactics B INV Simplify Applies the rule B INV followed by simplification of each subgoal This differs from the effect of setting Automatic Simplification ON by not b
31. lt gt for some k gt jl o k Ep and 0 7 E p for every i such that j lt i lt k e 0 EpWq ej EpUqor o j Op e o5jFOp a j 1 Fp For past operatorsI we have e 0o j F p lt gt forall KT0 k jT o k e p e 0 j F Op lt gt for some KTO k jI o k E p e 0 j Ep q lt gt for some KTO k jT o k E p and for every i such that k lt i lt jT o i E p a j EpBq ej F pS qor 0 j EEP e 0 FOp 4 j gt 0and o j 1 Ep Another useful derived operator is the entailment operatorI defined by p gt q O p gt q For a state formula p and a state s such that p holds on sT we say that s is a p state A state formula that holds on all states is called state valid For a temporal formula p and a position j gt 0 such that co j E pl we say that j is a p position in a If c 0 EF pl we say that p holds on oland write it as o F p A formula pis called satisfiable if it holds on some model A formula is called temporally valid if it holds on all models Two formulas p and q are defined to be equivalent written as p gl if the formula po qis validl i e l o F p iff o EF gEfor all models o We adopt the convention by which a formula p that is claimed to be valid is state valid if p is an assertionl and is temporally valid if p contains at least one temporal operator The formulas p and q are defined to be congruentU written as p ql if the formula p q is valid i e l o j F p i
32. marked with ax are intended for advanced users and may be safely omitted by the beginning student Chapters 2 8 are the main reference for using the system For those readers unfamiliar with Manna and Pnueli1995 l Appendixes A and B summarize STeP s program and prop erty specification languages Appendix C presents the most important differences between step and Manna and Pnuelil 1995 1 2 Starting sTeP The following are the steps for starting STeP 1 Set your STEP_DIR environment variable to the full directory path where STeP is installed If this variable is not setl you will not be able to run sTeP If you are installing the system you can edit the bin STeP file to correctly set this value for all users The DISPLAY environment variable is used by X windows to identify the screen where programs should runl and is usually of the form machine name 0 0 Due to the inner workings of eXene the SML X windows library Pthis should be changed to the form ip address 0 0Dwhere ip address is the corresponding numerical IP address AlternativelyI the display can be specified with the display command line option when running STePl as in STeP display ip address 0 0 Make sure that the machine where you plan to run sTeP has permission to open windows on your display To make sure this is the casel executel in your X windows consolel the command xhost Add STEP DIR to your path In this wayl when executi
33. on hold Check runtime system Generates a set of goals thatl if proved validl ensure that the transition system will not generate any runtime errors such as division by 0 or array references out of range Weakest precondition This option allows you to calculate weakest precondition for an arbitrary formula and transition in the current system see Section 4 3 The dialog window shown in Figure 3 9 upper window will appear after entering the transition name and formulal clicking on the button will display the weakest precondition in a separate window shown in Figure 3 9 s lower window The formula may be saved to a file with the button This function has no effect on the proof tree or on the background properties it serves a purely informative role Weakest precondition is also provided as an inference rule useful for strengthening invariantsl and is described in Section 4 3 The Tactics Menu The Tactics pull down menu is used to run tactics loaded from a file or entered directly Tactics can be run in two modes batchmode and interactive Batchmode tactics are applied without any user interaction they may not always terminatel but can be interrupted by clicking on the sTeP icon the interrupt button For interactive tacticsl a window appears with the first atomic step of the tactic The button applies the displayed step and the next one will appear In this waylI you can apply tactic steps until the proof is finishedl or at
34. operator 14 Awaits syntax r 16 axioml8P18 entryl45 in interactive proverI 90 B BACKTO tlp button 54 B CAUS tlp button 54 B INV tlp button 53 tutoriall93 B WAIT tlp button 53 back to rule basic B BACKTOT 54 general B BACKTOT 54 background propertiesD 51 activatingl 41 deactivatingD 41 deselectingI 41 selectingI 41 background propertyI 8 Backto operator l14 Backto syntax P 16 basic back to ruler 54 basic causality ruler 54 basic invariance rulel 53 basic nodel 62164 basic type 13 basic wait for ruler 53 132 BDD environment variablesl 128 simplification settingI 70 BDD splitI 71 BDD split ip button 90 binding operatorsD 17 Bool simplify top level button 71 bound variables 15 bound variables syntax l 16 branch otherwise tactic L 75 causality rule basic B CAUSI 54 general G CAUSI 54 chain diagramI 61 channel type declaration l 13 channel initialization difference with bookI 122 channel operationsI 24 check runtime system menu option I 45 clear text window menu option P48 clock syntax 31 clock variabler 32 clocked transition systemI 32 syntaxI31 commentsI 13 COMMUTATIVEL21 commutative functions simplification settingI 70 comparison operators syntax 16 Compassionate syntax 31 compassionate edgel 65 compassionate transitionI 105 Compound menu option 66 compound nodeT 62 computationI 106 computational modelI 105 conditional rewrite rules simplificati
35. p x gt q is parsed as Forall x int p x gt q and not as Forall x int p x gt q although x is not free in q e When in doubtl add parentheses Chapter 3 The Top Level Interface Starting sTeP brings up the Top level Prover window Figure 3 1 l a point and click X windows interface The Top level Prover window has the following main components 1 At the top of the main sTeP window is the main menul used to load systems and specificationsl save proof searchesI view systemsI select properties to be used in proofsI online helpl and exit sTeP Under the main menu is the status line It displays the name of the current sys tem file loadedl if any the number of unfinished proof treesl the number of open goals in the current proof treel the current simplifier settingsl and whether automatic simplification is ON or OFF Below the status line is the current goal windowl where the current unproven goal or subgoal is displayed This window has a scroll bar at the left Verification rules are applied to the formula that appears in this window Below the current goal window is the output windowl which displays the results of applying rules and generating invariants It will also state when a proof is completel and generally leave a record of the system s activities This window can be reset with the Clear text window item under the Settings pull down menu Under the output window at
36. possibility that the user will include a conjunct of the form x x 1 in the modrel fieldl or will mention a primed variable that is also assigned to The parser will automatically discover these cases and normalize the transition relation while printing a warning to the console A transition consists of one or more transition relations This partition allows a more convenient representation of certain transition relationsl e g l those for the while and if then else SPL constructs A transition is considered enabled if at least one of its constituent transition relations is enabled It is considered taken when one of its transition relations is taken A transition can be taken only if it is enabled Transitions that only differ with respect to some parameters can be collected in one parameterized transition The optional parameters are listed after the transition s name and declare one transition for each value assignment to the parameters A transition contains an optional fairness requirementlI which can be Just Compassionate or NoFairness The default fairness requirement is NoFairness Example The transition system in Figure 2 6 implements Euclid s algorithm for com puting the greatest common divisor of two positive integers x and y Transition System 4 Euclid s algorithm in a b int where a O NVb 0 local x y int out gcd int Initially x a ye b Transition ti Just enable x gt y assign X X y Transition t2 Just e
37. programs and specifications 125 126 APPENDIX D DISTRIBUTION AND INSTALLATION o directory program file specification files other files mE sa mpesm mpesmap 7 MU mux bak a mux bak a spl mux spec MU mux bak c spl MU mux bak d spl MU MU MU MU mux bak c mux bak d mux dek mux dek spl mux dek a mux dek a spl mux dek b mux dek b spl mux spec mux spec mux vd spec simple prec spec 1bo spec 1bo vd spec mux spec mux spec X FISHER o _ mux spec mux vd spec 1bo back spec 1bo spec 1bo vd spec mux spec accessibility spec 1bo spec MUX PET3 mux pet3 spl o MUX VAL3 mux val3 mux val3 spl mux spec yge0 spec mux spec PROD CONS prod cons prod cons spl no overflow spec PROD CONS C prod cons prod cons c spl no overflow c spec PRES ALLOG meal frescs C SQRT sqrt sqrt spl phi hat spec SQRT C sqrt sqrt c spl str part corr spec Table D 3 More example programs and specifications phi3 search phi4 search phi5 search mux tactic mux diagram 1bo diagram mux tactic mux diagram 1bo diagram mux tactic accessibility diagram mux search state partition diagram mux diagram mux compound diagram Appendix E STeP Environment Variables A number of UNIX environment variables can be set before running sTeP The only manda tory variables are STEP DIRI which indicates the directory where sTeP residesl and the DISPLAY environment variable which should be set
38. recently established goal View transitions Displays a separate window containing the current transition system It can also be selected when the system description is loaded as an SPL program The transition window can be deleted at any time by clicking on the Quit button of this window View program text Displays a separate window with the text of the current SPL pro gramTsimilar to View transitions above Quit Terminates the sTeP sessionl after confirmation from the user 3 1 MENU OPTIONS 41 The Properties Menu The Properties pull down menu Figure 3 5 is used to manage the background properties move between different proof treesl generate invariantsl and enter new goals and axioms directly mux Activate Deactivate pArith Auto ON Select goal Next search Select search Abandon search Get local invariants Get global linear invariants Get global polyhedral invariants Enter axiom Enter new goal Check runtime system Weakest Precondition Figure 3 5 Properties menu Activate Deactivate This option displays a window with all the background properties i e l all axioms enteredIinvariants generatedl and properties proven during the current system verification session See for example Figure 3 6I which displays the axiomsP some invariants and a proven property auxi of the program GCD By default all properties are activel which means that they are used by the Simplifier This window allows you to deactivate prop
39. results may also be returned to the Top level Prover and incorporated in the current proof tree as a new subgoal Another way to verify a program property is to use a verification diagram A verification diagram represents a set of verification conditions sufficient to establish a given property Diagrams are created by the Verification Diagram Editor Chapter 5 and subsequently transferred to the Top level Prover Finally any property or subgoal may be established by the Model CheckerI through the exploration of the state space of the system Section 4 5 Although model checking is only guaranteed to succeed for finite state programs whose state space is not too largel it is also generally useful to identify erroneous propertiesl since it provides a counterexample computation if the property is not valid for the given system STeP can also be used as a theorem proverl independently of any particular system verification task In this case you only need to load a specificationl and only the Simplifier and the Interactive Prover are used Restrictions may be placed on the system to make model checking more feasible see Section 4 5 6 CHAPTER 1 INTRODUCTION Verification Session A Quick Tour To make things more concrete we will give an example of an actual STeP session For a step by step description of the commands needed to run this examplel see the basic sTeP tutorial in Chapter 9 local y integer where y 1 lo loop forever
40. tac tac If this failsTit applies tac to the subgoal 6 3 2 Top level Prover Tactics atomic tactic n basic rule Basic rule not requiring arguments arg rule expns Rule requiring argument expressions basic rule B INV B WAIT B BACKTO B CAUS Simplify Interactive Undo Redo Postpone BDD arg rule z G INV G WAIT G BACKTO G CAUS Modelcheck esp 4 ezxpns 6 3 3 Interactive Prover Tactics To appreciate this section it is helpful to have read Chapter 8 atomic ltactic basic rule Basic rule not requiring arguments e rule expns Rule taking expression argument p rule positions Rule taking position arguments pe rule expn poss Rule taking position and expression arguments p rule Position rule without position arguments replace Replacement of equals for equals skolemize Skolemization 76 basic rule e rule p rule pe rule replace skolemize expns positions position CHAPTER 6 AUTOMATIC THEOREM PROVING Undo Redo Postpone Flatten Simplify Make first order Next Presburger All Propositional BDD split PTL expansion Cut Add Axiom Rewrite Free Induction Duplicate Delete Hide Unhide 1 Step Propositional Induction Instantiate Basic rules behave the same as their pushbutton counterparts adds argument expressions as cuts adds argument expressions as axioms arguments is a tuple of pairs each pair represents a rewrite rule arguments are the
41. the above has to be entered as in X y Z2 integer in a b c bool local d e f integer local g h i bool C 4 Initialization Array Initialization In several programs MP95 uses the following construct to initialize an array in M integer where M gt 1 y array 1l M of integer where y T In STeP this causes an error due to the incompatible types of y and T In sTeP this has to be written as in M int where M gt 1 in x array 1 M of int where Forall i 1 M y i true 122 APPENDIX C DIFFERENCES WITH THE BOOK Channel Initialization In MP95 a channel may be initialized as the empty channel with send A In sTeP this is accomplished with length send 0 In MP95 a channel may be initialized with values as follows ack 1 1 N STeP does not provide a construct to initialize a channel in the where clause If the initial values matterl the channel has to be initialized explicitly within the program withI for examplel a while statement If the initial values do not matterl which is the case for program PROD CONS C of Figure 1 18 in MP95I the channel may be initialized with the following where clause in N int where N gt O local send ack channel 1 of int where length ack N length send 0 C 5 Parameterized Programs In MP95 page 174 l terms such as Nz are often used to denote the number of processes residing at a particular location This abbreviation is not available in sTePI so th
42. the transition relation c move L t pe V pres Ys ac move l l According to p when c evaluates to true control moves from to Cand when c evaluates to false control moves from to Two way With the statement if c then E S else lo 5 f Twe associate a transition r I with the transition relation c move l h pe V pres Ys ac move t 5 According to pel when c evaluates to true control moves from to land when c evaluates to false control moves from to 5 e While With the statement while c do we associate a transition r with the transition relation c move L t pe V pres Ys ac move l l According to pe when c evaluates to true control moves from to Cand when c evaluates to false control moves from to l Note thatlin this context the post location of is Note also that the enabling condition of Te is at I which does not depend on the value of c e Loop forever 7 With the statement loop forever do we do not associate any transi tions However the locations I and post location of S are equivalent e Hepeat until With the statement repeat S 41 until c 2 we associate a transition rV with the transition relation c move ly ly p vo pres Ys ac move 6 t A 3 SPL SEMANTICS 111 According to Pe when c evaluates to true control moves from to 9D and when c evaluates to false
43. there are no goals leftI the current goal in the Top level Prover is closed If you choose to ignore the effect of the Interactive Prover the proof tree in the Top level Prover stays as it was before invoking the Interactive Prover The button saving verbose versions allows you to save the entire proof in the format seen during verification Each sequent is printed in its full lengthl and annotated with its position in the proof search The button saving for rerunsI saves a dense proof scriptI which can be loaded as a tactic for later automatic recreation of the proof 8 3 Interactive Prover Rules The right column of the Interactive Prover contains buttons to manipulate the proof tree and invoke the Gentzen proof rules The proof search proceeds as usuall with logical rules that reduce the current goal to a number of subgoalsland simplification steps that close or simplify the current goal A number of inference rules require the user to select subformulas in the sequent The subformulasI that may be selected are highlighted when selecting the inference rulel and the user clicks on the relevant highlighted formula to invoke the rule on that formula Makes the ancestor of the current subgoal into the current goal The former current goal is retained to enable a Redo I unless another proof rule is applied to the new current goal 8 3 INTERACTIVE PROVER RULES 85 Redoes a previous Undo Temporarily hides a formula from the current
44. variables that are changed by the transition relation are the ones primed in the modrel field and the ones to the left hand side of assignments in the assign field described below The modvar field does not need to contain those variables e The enable field the enabling conditionl a formula that may not contain any primed variables The transition can only be taken if the enabling condition is satisfied By defaultI the enabling condition is true e The modrel field contains the modifying relationl an arbitrary relation over primed and unprimed variables that is assumed to hold when the transition is taken Its default value is true e The assign field lists the assignments for those variables whose next state values can be described as a function of the current state unprimed variables An assignment x t in the assign field can be equivalently expressed as a conjunct x t in the modifying relation but assignment relations need not also appear in the modrel field In factlit is preferable to only include them in the assign field For examplel rather than having x x 1 as a conjunct in the modrel fieldl you should include x x 1 in the assign field 30 CHAPTER 2 SYSTEMS AND SPECIFICATIONS In generallI variables that appear on the left hand side of an assignment statement should not appear primed in the modifying relation there is the risk of unwillingly specifying an unsatisfiable transition relation Still there is the
45. versions of the system variables The transition relation expresses the relation holding between a state s and any of its T successors s r s The unprimed version of a variable refers to its value in sl and the primed version refers to its value in s Thus the state s is a r successor of the state s if the formula p V V evaluates to truel when we interpret each x V as s x l and its primed version z as s x If not explicitly specifiedl sTeP adds to each fair transition system the idling transition Ty also called the stuttering transition whose transition relation is pz V V 105 106 APPENDIX A COMPUTATIONAL MODEL A 2 Computations An infinite sequence of states 0 80 51 52 is defined to be a computation of a fair transition system P if it satisfies the following requirements e Initiality sg is initial that isl it satisfies the initial condition e Consecution For each j 0 1 the state s 41 is a r successor of the state s e Justice For each transition 7 JTit is not the case that 7 is continually enabled beyond some position j in c but not taken e Compassion For each transition 7 CTit is not the case that 7 is enabled at infinitely many positions in but taken at only finitely many positions A 3 SPL semantics System Variables The system variables V consist of the program variables declared in the programl and a set of control variables approximately one for each spawned
46. you intend to apply the rule Some rules require additional information to be entered through dialog windows Menu Options Refresh redraws the Interactive Prover windows Tactics is equivalent to the Tactics menu in the Top level Prover Section 3 1 except now it invokes tactics composed of Interactive Prover primitive commands see Section 6 3 Settings Simplification Flags This menu option is equivalent to the Simplification Flags option in the Top level Prover It brings up a window used to set the power of the automatic Simplifier see Section 6 1 8 2 USER INTERFACE 83 Current goal 0 y2 pid 3 gt 0 y2 yl _ Duplicate Flatten o Next Figure 8 1 Interactive Prover Window 84 CHAPTER 8 THE INTERACTIVE PROVER x Select boxes This menu option allows the user to control whether boxesI i e T the temporal operator known as henceforth Tin front of axioms added to the sequent during the proof should be kept or not By default boxes are removed from axiomsI when axioms are added to the sequent See also the explanation of Add Axiom below for an example of the usage of Select boxes Quit brings up the window shown in Figure 8 2 ETATE Exit and use the result obtained Figure 8 2 Exit Window for Interactive Prover If you choose to use the results obtainedl any unfinished goals are returned to the Top level Prover as a new goal with the name Interactive If
47. 45 clear text windowT 48 CONTI56 edit diagramD 46 enter axiomTI 45 enter batch tacticI 46 enter interactive tacticI 46 enter new goall 45 get invariantsL 44 load batch tacticl 45 load interactive tacticr45 load programI38 load specification 40 load transitions 38 MON CT56 MON II 55 MON WT56 next search 41 quitl40 reset alll 40 reset BDDsI 48 reset searchesT 40 save goall 40 save properties 40 save searchDl 40 save transitionsI 40 select boxesI 84 select goall 41 INDEX select searchD 44 simplification flagsl 47 system informationT 48 TRN CT56 verification diagram rule 46 view program text 40 view transitions 40 weakest precondition 45 mod operator P14 mod syntax 16 mode in declaration D 121 mode of variablesD 25 model of temporal formula 113 Modelcheck tl button 49 Modelcheck tlp button tutoriall 97 modifying relation 29 modrel syntax r31 field P29 modvar fieldI 29 MON C menu option 56 MON I tutorial 100 MON I menu option 55 MON W menu option I56 monotonicity rule causality 56 monotonicity rule invariance 55 monotonicity rule wait for 56 MUX PET1 mutual exclusionl 100 MUX SEM mutual exclusionI 92 Next ip button 88 next tlp button 48 next search menu option 41 NoFairness syntax 31 noncritical statement l semanticsI 109 noncritical syntax 27 Nonterminal menu option 66 nonterminal nodel 60 operator associativityl 17 operator preced
48. 9 TRN C menu option P56 try tactic 73 tuple projectionI 16 type constructorDL 13 type declaration 13119 types 13 ncompound menu option 66 ndo ip button Il 84 ndo tlp button 48 ngroup menu option P66 nhide ip button I 85 NIX environment variables 127 nprimed variabler 105 ntil operator l14 cag cdddadscdcd 138 Until syntax L 16 validity PT114 generall 8 state I 114 value declaration 21 variables auxiliaryI 22 bound 15 declaration 181 21 flexibler 9r22 quantifiedT 22 rigid 9122 verification conditionI 9 side I 60 verification diagramI 59 basic nodel 64 definitionI 59 double edgel 61 environment variablesIl 127 hierarchicall 67 import node 67 invariance 60 nonterminal nodel 60 P validr 60 response 61 solid edge 61 terminal node r65 tutorial 98 verification ruler 46 wait forl 60 verification diagram editorI59 activatingI 46 drawing toolsT 64 Edge menu 66 Edit menur 66 File menu 65 Help menuI 67 interfacer 64 menu optionsI 65 Node menul 66 verification diagram rule menu option I 46 verification rulesI 52 invokingI 48 INDEX view program text menu option l 40 view transitions menu option 40 wait for diagramI 60 wait for rule basic B WAITT53 general G WAITI 53 weakest precondition menu option I 45 weakest precondition rule 55 when syntax 27 where clausel 106 while syntax 27 WPC tlp button P55 tutorial 100 X windowsI3 xhost UNIX comman
49. BDD CACHET128 STEP_BDD_NODEST 128 STEP BDD SPLITT 128 STEP_BROWSERI 127 STEP DIAGRAM HEIGHTTI127 STEP DIAGRAM WIDTHTI 127 INDEX STEP DIRI3I127 STEPMCTIMETS58P 128 STEP MC CPUFPSSTP128 STEP MC SPACED58DI128 STEP POLY CPUL128 STEP POLY SPACET128 STEP_POLY_TIMET128 STEPSHOW_LOADEDP 127 Strengthen tlp button r55 strengthening ruler 55 stuttering transition 105 subgoall 9 Sum operator 28 Sum syntax P16 synchronous send receive statement semantics 108 system descriptionI 9 system information menu option P48 system variablesl OT 1051106 system verification sessionI 8 tactic 72 atomicI 72 branch otherwisel 75 elseI 74 entryl 46 examplesI 77 loading 45 repeat 74 sequence 74 spreadI 74 tryL 73 tactics tutoriall 102 tactics menuI 45 tail syntax 16124128 temporal operators future 113 pastIL 113 temporal operators syntax l 16 Terminal menu option 66 terminal nodel 60 theorem proving sessionI 8 terminatingDl 40 tickI 32 137 top level proverL 35 top level prover button B BACKTOP54 B CAUSI54 B INVI 53 B WAITT53 G BACKTOTD54 G CAUSI 54 G INVI53 G WAITTI53 Interactive proverI 49 ModelcheckI 49 next 48 previousD 48 redol 48 StrengthenI 55 undol 48 WPCTI55 transitionI 301105 compassionateI 105 disabled 105 enabledI 105 justI 105 Transition syntax l 31 transition relation 291105 transition systemI 29 loadingl 38 syntaxI31 transitivity ruleI 56 tree example P1
50. Chapter 7 Automatic Generation of Invariants STeP includes three different methods that automatically generate bottom up invariantsT based solely on the system to be verifiedl of increasing power and complexity Since these invariants arel by constructionl guaranteed to be true of the systemI they are automatically added to the list of active background properties Of the three methodsI the firstI local invariantsl operates on an SPL program the other two operate on the transition system directly A description of the general principles behind STeP s invariant generation algorithms is Bj rner et a D1995 To obtain invariantsI select the appropriate option under the Properties menu when the invariant generation is donel each invariant is simplified displayed in the output windowI and added to the set of background properties By default they are activel and thus used in the simplification of goals They may be deactivated with the Activate Deactivate menu option Each invariant is simplified on its own i e I no background properties are used l using the basic decision procedures for equality see Section 6 1 When the invariant generator is finished a message will appear in the message window Invariant generation and simplification can be halted by clicking on the interrupt button the sTeP logo 7 1 Local Invariants Local invariant generation produces very simple but useful invariants based on local analysis of the program text The
51. HE BOOK pi0 0 So pi0 1 91 pi0 2 P2 mO pi0 3 pil 0 S2 mi pi0 8 pil 1 5 m2 pi0 3 pil 2 pi0 3 pi2 0 S4 pi0 3 pi2 1 pi0 4 m4 pi0 4 Ss mb pi0 5 Se m6 pi0 6 S7 m7 pi0 7 Ss m8 pi0 10 or pi0 4 So kb pi0 8 10 k6 pi0 9 11 k7 pi0 10 or j4 pi0 4 S iz j5 pi0 10 l 15 pi0 10 13 16 pi0 11 Figure C 2 Program schema illustrating STeP s use of control counters C 3 TYPE DECLARATIONS 121 3 In both sTeP and MP95I the same rules govern the notion of label equivalence STeP This is achieved by assuming label equivalent locations the same control counter values MP95 This is achieved by using the notational convenience that a label really refers to its label equivalence class Consequentlyl 4 m4 k4 j4 and 5 mg ky js see page 13 14 in MP95 Location equivalences In srePl a loop forever do statement does not generate a transitionI so the pre location and post location of this statement are equivalent Howeverl both locations are entered as location variables in the symbol table and can thus be referred to in the specification C 3 Type Declarations In several programs MP95 uses multiple lines of declarations as follows in 7 y z integer a b c bool local d e f integer g h i bool In sTeP each line of declarations must be preceded by the mode of the variablel so
52. I specialized to linear time temporal logic For more backgroundTseel e g l Gallier 1987 This chapter explains the basic functionality of the various rules provided in the Interactive Prover and gives examples of their use 8 1 Proof Structure A goal or subgoal in the Interactive Prover is a sequentlof the form D A where I and A are multisets of formulas i e formulas can be repeated A sequent stands for the formula Aoi M 6 where q are the elements of Il and are the elements of A Free variables are implicitly universally quantified The Interactive Prover creates a proof tree similar to that in the Top level Prover An inference rule applies to zero or more of the formulas in a sequent T AT and produces a number of subgoalsl the branches of the treel again in the form of sequents The proof is finished when all subgoals are closed A subgoal is closed when one of the following conditions is satisfied e Thesequent contains true on the right hand side of the long doubly lined implication IT gt A true e The sequent contains false on the left hand side of the long doubly lined implication I false A e The sequent contains a formula p in both the left and right sides of the long doubly lined implication p T A P 81 82 CHAPTER 8 THE INTERACTIVE PROVER x cationl and no applications of see Section 8 3 separate the sequent from the root of the proof tree e The sequent contains a formula p o
53. OFF Conditional Rewrite Rules If ONT the Simplifier will use a number of built in conditional rewrite rules For examplelit will simplify y gt 0Az y gt 0 gt zr gt 0 to true when the switch is ONI but will not be able to simplify it when the switch is OFF Conditional rewrite rules may slow down the Simplifier considerably so they are switched OFF by default Commonly used Simplifier settings are also available as separate buttons in the action region of the Top level Prover 6 2 BDD SIMPLIFICATION 71 Fast simplify Applies only the most basic simplification proceduresl disregarding the background properties This is useful to rewrite formulas into a more standard form after which they can be compared more easily with each other Bool simplify Applies a propositional satisfiability checkT using the active background properties If the given formula is a propositional tautology with respect to the active background propertiesl it will be simplified to true This procedure is complete for propositional logic The basic simplification procedures see Fast simplify above are called before the propositional test This procedure uses sreP s BDD package see Section 6 2 Simplify Invokes the simplifier and decision procedures as given by the current simplifica tion settings For material related to the decision procedures and indexing used in sTePI see Bledsoel 1975 l ShostakT1979 P Nelson and Oppent 1980 Boyer and Moorel1988
54. PTER 6 AUTOMATIC THEOREM PROVING e Equality and Inequality If ONTthe Simplifier will use properties of equalities and inequalities For example it will simplify y gt l gt y gt 0 to true when this switch is ONTbut not when it is OFF These decision procedures are quite efficient and useful in generall so they are ON by default Linear Arithmetic If ONT the Simplifier will use decision procedures for linear arithmetic which use properties of gt Tand For example it will simplify y gt 0 Ay y 1 5 7 gt 0 to true when the switch is ONI but will not be able to simplify it when the switch is OFF The default is OFF The performance of these procedures can vary widely from one formula to the next the interrupt button can be used to halt the computation Associative and Commutative functions If ONI sTeP will take into account the associativity and commutativity of addition multiplication and boolean connectivesl as well as those user defined binary function symbols that have been declared as ACT ASSOCIATIVE or COMMUTATIVE see Section 2 3 Note that since STeP rewrites all formulas into a normal form it implicitly uses many instances of the associative and commutative laws even when this flag is OFF The default is OFF BDD simplification If ONIthe propositionally complete BDD simplification method will be used as part of the simplifierl before other decision procedures are used see Section 6 2 The default is
55. Simplify phiO 10 phio 5 Established via Simplify phiO 11 phio 6 Established via Simplify phiO 12 phio 7 Established via Simplify phi0 13 phio 8 Established via Simplify phiO 14 phio 9 Established via Simplify phiO mO phi0O 10 Established via Simplify phiO m1 phi0O 11 Established via Simplify phiO m2 phi0O 12 Established via Simplify phiO m3 phi0O 13 Established via Simplify phiO m4 phi0 Figure 9 6 Transcript for proof of Cy gt 0 over MUX SEM 9 2 2 Using G INV The next property we will provel yI expresses mutual exclusion This property is not inductivel even relative to the simple property y proved before Howeverl we can prove it by strengthening the invariant being provedl as follows 1 Load the specification file mux sem mux spec The property 2 will appear in the current goal window 2 Click on G INV This will bring up a window with the title Input auxiliary assertions By defaultI the auxiliary assertion is the goal to be provenI so when the default is used G INV behaves exactly as B INV Now enter the following formula after deleting the default one 134144m34m4 4y 1 9 2 MUX SEM MUTUAL EXCLUSION 97 and click on OK If there is a syntax error in the entered formulal a message will be displayed at the bottom of the entry windowl and you will be asked to try again Using boolean terms such as 13 and m3 as integers is a convenient feature for writing
56. ThusP mutual exclusion for mux pet1 can be proved automatically by this tactic Note that the batchmode application of a tactic such as this one is riskyl since it may not ter minate Howeverltactics can be interrupted by clicking on the interrupt button the sTeP logo in the bottom right corner of the main interface When applying a tactic for the first timel it is recommended to apply it in interactive mode In this wayI the behavior of the tactic can be followed at each stepl and the tactic can be easily interrupted at any time 9 3 3 Using verification diagrams The chain diagram given in Figure 5 1 is a high level proof outline for process P s acces sibility to its critical section It establishes that whenever P requests access to its critical section it will eventually get there When specified in sTeP this reads 12 gt 2514 To use the chain diagram in proving this response propertyl assume we have already loaded the programI selected automatic simplicationl and generated local invariants as described in Section 9 3 1 We now apply the following steps 1 Select Enter new goal under the Properties menu Enter the goal 12 gt 514 2 Invoke the diagram editor by selecting Edit verification diagram in the Diagrams menu 3 From the verification diagram editor select Load in the File menu to load the verifica tion diagram mux peti response diagram The diagram in Figure 5 1 should now appear in the verification diagram wi
57. You can edit the STeP script to set the STEP DIR environment variable once and for all Note These scripts use the bin sh shell if this shell is not foundI you should edit them and change the first line to indicate the appropriate location actuallyl ksh is preferred sTeP Distribution When the distribution has been untarred it will have created three directories e The bin directory containing binaries stepI model checkerland polyserv for execut ing STePl and from within it the model checker and utilities for generating polyhedral invariants e The doc directory It contains 1 The sTeP manual postscript 123 124 APPENDIX D DISTRIBUTION AND INSTALLATION 2 The step Technical Report postscript STA N CS TR 94 15180 Stanford Com puter Science Department June 1994 This report complements the sTeP man ual by giving a high level description of the system and its goals and some extra technical details The list of known problems and bugs known bugs txt 3 4 A quick installation guide installation txt 5 The text of the licence agreement license agreement txt 6 The WWW subdirectory which contains the help pages e The examples directory containing a selection of simple example programs and spec ifications that can be verified using STeP New releases will include updated help pages please let us know how those pagesl and this manualIl can be improved D 1 Example Programs The examples directory
58. accomplished by the preprocessor are e simplification of data types e elimination of unnecessary variables e instantiation of parameters and other variables e introduction of additional transitions corresponding to possible run time errors e general simplification of the transition system and of the propertyl using the Simplifier Note that the additional assumption can be used to restrict the range of a variable on which array or parameter bounds depend The Core Model Checker For each problem instancel an external core model checker is invoked It searches the state space and stops when 1 a run time error is foundI 2 a counterexample computation is foundl or 3 the entire state space has been explored The main algorithm used by the core model checker is adapted from Hojati et al L1993 Restrictions Not all programs and properties accepted by sTeP can be model checked The datatypes handled by the core model checker are booleanl integerl and channelsl and arrays over booleans and integers The preprocessor can reduce some other datatypes to these The model checker can only handle basic logicl arithmeticl and channel operations applied to these variables Formulas given to the Model Checker cannot have temporal operators in the scope of binding operators 58 CHAPTER 4 VERIFICATION AND LOGICAL RULES Log file The model checking results are reported in a log file selected by the user before model checking begins
59. acktracking to the unsim plified verification condition when simplification fails B INV Simplify Undo If simplification does not establish the given subgoal of B INV the current leaf in the proof search tree is undonel getting back to the unsimplified subgoal repeat B INV Simplify Undo WPC Repeats application of B INV to each unsimplified subgoal that has been strength ened by the rule G INV 15 N m5 14 m5 gt s 2 y1 h Simplify Applies rule G INV with a strengthening formulal and each subgoal is then simplified G INV only requires one strengthening formula rules such as G WAIT require more so a list of expressions must be entered following the keyword G WAIT Skolemize Simplify BDD split Simplify Called from the Interactive Proverl this tactic attempts to establish a subgoal by first skolemizing quantifiers of universal forcel and then simplifying in the hope that simplification will reduce the boolean complexity of the verification condition BDD split is then invoked to split the goal into subgoals of atomic formulas the simplifier is finally invoked to establish each of these subgoals 1 Step Propositional Simplify 78 CHAPTER 6 AUTOMATIC THEOREM PROVING The Interactive Prover 1 Step Propositional rule is used without a position It is therefore used exhaustively until it cannot be applied Then each generated subgoal is simplified by Simplify
60. adheres to the default filename extensions used by the File Browser These conventions are shown in Table D 1 contents of fl Spl SPL program trans transition system cts clocked transition system Spec specification Search proof search diagram verification diagram tactic tactic mclog modelchecker logfile Table D 1 Filename conventions The example programs and specification files listed in Tables D 2 and D 3 are included in the distribution They correspond to simple examples and exercises from Manna and Pnuelil 1995 In most cases the user will have to complete the specifications for exercises in order to succeed deductive verification Thus possible answers to the exercises are not included in the distribution The directory mux fisher contains a simple real time protocol implemented with Clocked Transition Systems D 1 EXAMPLE PROGRAMS directory program file specification files other files ADD TWO add two add two spl ygel spec l1x 2 spec aca sp BINOM binom binom spl part corr spec str part corr spec BINOM C binom binom c spl part corr spec str part corr spec part corrspec difEine spl__ psispec DINE dine dine spl DINE CONTR dine contr dine contr spl DINE EXCL dine excl dine excl spl double spl factspl Parkcorrspec GCD gcd gcd spl part corr spec psispee LOOP loop loop trans phi3 spec psi3 spec LOOP loop loop trans phi3 spec psi3 spec Table D 2 Example
61. al assumptionsI it is not added to the set of background properties The Model Checker results are reported in a logfile See Section 4 5 for a more detailed description of the modelchecker BDD split Fast simplify Boolean Simplify These buttons invoke various versions of the automatic Simplifier while BDD split can generate a set of subgoalsI the others can only reduce the formula to a simpler one See Section 6 1 for details STeP logo The sTeP logo serves as the interrupt buttonl and can be used to exit from each of the following time consuming operations e Simplification of verification conditions e Generation and simplification of invariants e Model checking 50 CHAPTER 3 THE TOP LEVEL INTERFACE Chapter 4 Verification and Logical Rules The main function of the Top level Prover is to apply verification rules to temporal proper ties reducing them to simpler verification conditions These verification conditions become subgoals in the top level proof tree The verification rules depend on the system being verified In contrastl a set of logical rules reduces temporal properties independent of the system being verified This chapter describes the general structure of the proof search and the rules used to construct it in the Top level Prover 4 1 The Proof Search The structure of the proof search is similar in the Top level Prover and the Interactive Prover the proof is a tree with the original g
62. any point interrupt the tactic by clicking on the button Tactics and their syntax are presented in Section 6 3 Load batch tactic Reads a tactic from a file using the File Browser and applies it in batch mode Load interactive tactic Reads a tactic from a file and runs it in interactive mode 46 CHAPTER 3 THE TOP LEVEL INTERFACE ion viewer 4 Transition name Formula IA im4 y2 V s 2 A pi Figure 3 9 Weakest Precondition entry and output window Enter batch tactic Prompts the user to enter a tacticl which is then parsed and run in batch mode Error messages from parsing the tactic are displayed in the bottom of the input window Enter interactive tactic Prompts the user to enter a tacticl which is then parsed and run in interactive mode The Diagrams Menu The Diagrams pull down menu is used to start up the Verification Diagram Editor and use verification diagrams in the current verification session The Verification Diagram Ed itor may be used in parallel with the Top level Proverl and is described in more detail in Chapter 5 Edit diagram Starts the Verification Diagram Editor in a separate window Verification Diagram rule Uses the current verification diagram as a verification rule for the current goal or subgoal It generates subgoals corresponding to all the verification conditions implicit in the diagramTif the diagram is applicable ThusI the verification diagram can be seen as a specialized v
63. ariables under consideration which can be controlled by the user The more variables that are includedI the more powerful the invariants that can be generatedI but the time spent generating invariants will also increase possibly in an exponential manner When the polyhedral invariant generation is selectedI a dialog window appears where the user can enter the following 1 Variables to be ignored you may enter a list of program and auxiliary variablesl sepa rated by spaces or commas These variables will be ignored by the invariant generator that isl the invariant generation will not try to deduce polyhedral relationships which include them 2 Location variables to be considered By defaultl location variables are not considered by the polyhedral invariant generator Here you may enter a list of location variables to be added to the vocabulary of the invariant generator The generator uses an external packagel whose time and space limitations can be controlled by setting the following environment variables STEP POLY SPACE Megabytes STEP POLY TIME minutes STEP POLY CPU minutes The invariant generation can be interrupted by clicking on the interrupt button the sTeP logo this may leave a separate UNIX process runningl which users may have to terminate independently from a UNIX prompt see the UNIX kill command man pages Chapter 8 The Interactive Prover x The Interactive Prover is based on a Gentzen style proof system
64. as It usually generates simpler verification conditions than its counterpart G INVT which is also applicable to goals of this formT by taking into account the special form of the formula to be proved After clicking on this button a dialog window will appear which allows you to enter an intermediate formula q default q After vy is enteredI the following subgoals are generated p cpVvq Monotonicity O gt q o V q o Initial condition JT ev g e B BACKTO The basic back to rule establishes properties of the form p quB Bqo for past formulas p q4 qo It generates the following subgoals p Vizo di Premise N1 qi di Monotonicity for each in 1 n dT H V lt iq foreach iin 1 n e G BACKTO The general back to rule generalizes the above by allowing strengthen ing of the q s and weakening of p To prove P qn B B qo given formulas qo nl the following subgoals are generated p gt Vico Yi Premise N1 Pi di Monotonicity for each 2 in 1 n eT MVis Qi for each in 1 n 4 3 WPC AND STRENGTHENING 55 4 3 WPC and Strengthening A basic and often successful heuristic for constructing inductive invariance properties is based on weakest preconditions e The weakest precondition verification rule can be used to prove a verification condition that does not itself simplify to true The rule is applicable to subgoals of the form teirtys and when applied it generates the subgoal
65. ative COMMUTATIVE and ASSOCIATIVE state that the function is only commutative or associativel respectively For examplel in Figure 2 1 the gcd function was defined to be commutative Thus the simplifier assumes that Forall a b int gcd a b gcd b a besides the other axioms MacrosI which may take optional argumentslare declared with the keyword macro A where clause defines the expression corresponding to the macro Each macro takes a fixed number of arguments and is expanded by the parser through purely syntactic substitution A macro definition can use other previously defined macrosI which will be expanded in turn Example Figure 2 2 shows an example of value and macro declarations as they may appear in a program or a specification file The value declarations define the integer constant c and function symbol fl which takes a pair of arguments of boolean type and returns an integer The macro declarations indicate that the symbol m should be expanded to the expression c lt c Il and the symbol g with integer arguments i j should be expanded into i i j 4 5 value c int value f bool bool gt int macro m bool where m c lt c 1 macro g int int gt int where g i j i i j 5 Figure 2 2 Value and macro definitions Example Figure 2 3 shows a specification file to prove 1 bounded overtaking for program mux peti Figure 3 4 The proof by rule G WAIT requires the input of four auxiliary assertions Having define
66. cation conditions that were not valid Applying weakest precondition to invalid verification condition is a common technique that often succeedsI so we may want the application to be automatic This can be done with the help of tactics STeP provides a simple tactic language in which sequences of rules can be specified The tactic language is described in detail in Chapter 6 3l and more examples of tactics are presented in Section 6 3 5 To prove mutual exclusion for MUX PETI using tactics we do the following 1 2 Load program mux peti spl and the specification file mux spec Select Get local invariants from the Properties menu Select Enter batchmode tactic from the Tactics menu This will bring up a data entry window with the title Enter tactic Enter the following in this window repeat B INV Simplify Undo WPC and click on OK This will apply B INV to the goal All resulting subgoals will be simplified For those subgoals that do not simplify to truel the simplification will be undonel going back to the unsimplified verification conditionl to which WPC is then applied Then the process is repeated for all open subgoals In this casel they are 9 3 MUX PET1 INVARIANCE STRENGTHENING 103 invariance formulasI since WPC always generates an invariance formula Application of the tactic is repeated in this way until there are no open subgoals left This involves two iterations in this casel and the proof is complete
67. cation of propositional inference rules is controlled uniformly with this button After clicking this button formulas which contain propositional connectives that can be analyzed are highlighted Clicking on one of the highlighted formulas applies the appropriate propositional inference rule to the selected formula The boolean connectives analyzed are A APvIoPor Dfthen else which are entered as N M gt lt gt if then else The temporal connectives analyzed are TOrUPWTAPSrsrls 86 CHAPTER 8 THE INTERACTIVE PROVER x which are entered as lt gt Until Awaits lt gt Since Backto Notice that and are not in this group Figure 8 3 shows all the rules that can be applied by 1 Step Propositional Quantifiers of universal force can be eliminated by skolemizationl which re places the bound variable by a new variable If there are multiple instances of universally quantified variables all of the correspond ing formulas are highlighted upon clicking on this buttonl and you can select the one you want to skolemize by clicking on it implements the inference rule T f b A T Exists x f x A where b is a fresh variable not occurring free in TTA or Exists x f x D A f b T gt A Forall x f x where again b is not free in either ITTA or Forall x f x Besides these casesI the Interactive Prover supports skolemization of quantifiers un
68. ch possible value of z e Consume With the statement consume y LT we associate a transition Tel with transition relation pe move l l y 0 pres Ys 1y The observable action of the consume statement is to set variable y to zero e Guarded Assignment Statement l guard c do e Transition relation pe N moves l 0 uw pres Ys u The assignment is enabled if control is at the assignment statement and c evaluates to true Run time type errors are not considered in the enabling condition of the transition As with standard assignmentI the possibility of run time errors can be checked with the Check Runtime System option under the Properties menu Composite Statements Standard control constructs and primitives for concurrency compose simpler program state ments into more elaborate statements A composite statement is in general of the form C 1 5 l where S1 Sn are the immediate substatements The transitions associ ated with a composite statement comprise of the union of the transitions associated with 110 APPENDIX A COMPUTATIONAL MODEL S1 5 and the transitions associated with the construct C Below we describe the tran sitions associated with each construct Here Ys refers to all system variables except the control and location variables changed by each construct e Conditional One way With the statement if c then l S f Twe associate a transition TI with
69. claration type id id idn Example A tree datatype can be defined recursively with a forest datatype as follows type ident type tree Node id ident children forest and forest Nil Cons first tree next forest The type ident is defined as a new underspecified type A forest is a set of trees represented as a list either Nil or the Cons of a tree and a forest A tree itself is a Node containing an id and a set of childrenl represented as a forest The above datatype definition implicitly declares the following function symbols 20 CHAPTER 2 SYSTEMS AND SPECIFICATIONS value Node ident forest gt tree value id tree gt ident value children tree gt forest value Nil forest value Cons tree forest gt forest value first forest gt tree value next forest gt forest The constructors Nodel NillCons are used to create new elements of the correspond ing typeI while the deconstructors idI childrenl firstI next are used to access the different components of the datatypes For the deconstructorsI the following simplification rulesl explained in Section 2 4 41 are automatically inferredl and do not have to be declared variable i ident variable ch n forest variable t tree SIMPLIFY id Node i ch 5 i SIMPLIFY children Node i ch gt ch SIMPLIFY first Cons t n t SIMPLIFY next Cons t n n These rules are used automatically by the simpli
70. d I3
71. d these assertions in the specification file allows the user to enter them by namel phiOl phill phi2 or phi3l in the dialog windowI reducing the chance of typing errors and saving time if the proof needs to be repeated multiple times 2 4 3 Variable Declarations aux var decl variable ids type kind auxiliary variable declaration kind Rigid Flexible system var decl mode ids type where expn system variable declaration clock ids where expn system clock mode z in out local ids n dd id list of identifiers 22 CHAPTER 2 SYSTEMS AND SPECIFICATIONS i bounded overtaking for mux peti for proof by rule G WAIT use the following intermediate assertions phio 14 phil 13 mO m1 m2 m5 M m3 s 1 phi2 13 m4 phi3 13 m3 s 1 SPEC macro phiO bool where phiO 14 macro phil bool where phili 13 m 0 2 5 M m3 N s 1 macro phi2 bool where phi2 13 m4 macro phi3 bool where phi3 13 m3 s 1 PROPERTY 1 bounded overtaking 13 gt m4 Awaits m4 Awaits m4 Awaits 14 Figure 2 3 Specification file for proving mux pet1 1 bounded overtaking Auxiliary variables are declared with the keyword variable Auxiliary variables can only be declared in the specification filel or in a directly entered goall and are not part of the system being verified Each auxiliary variable can be optionally declared to be Rigid its value does not change over time or Flexibl
72. der any nesting of the boolean connectives M gt T and the then and else branches in if then else The type of the new variable b is that of xI where range types have been replaced by int Range constraints are reconstructed in a type condition that is added to the formula f Example For formulas e f g Forall x 1 N h x l and y of type integer not free in theseI Skolemize eliminates the universal force quantifier by f e sA 0 lt y y lt N bly f e gt g Forall x 1 N h x Instantiate Quantifiers of existential force can be instantiated by terms After clicking on this buttonI a data entry window appears for entering the term you want to instantiate the bound variable with implements the inference rules D A p t T A Exists x p x T p t T Forall x p x 8 3 INTERACTIVE PROVER RULES Propositional Rules 87 Sequents and formulas in square brackets are only generated when the sequent below the line is above an application of the rule Next This guarantees that statements such as first are not derivablel as opposed to first first is shorthand for 5 truel which only holds at position 0 gt V gt gt e B s T p gt A TSA y C Le Ole Waz A Pes ws Le OH TAS LiSA y Ste
73. designed and implemented by Nikolaj Bj rner r Anca Browne Eddie Chang and Tomas Uribe Henny Sipma and Arjun Kapur have collaborated with the development and documentation of STeP The Verification Diagram editor was developed by Michael Col n The interface tools were developed by Michael Col n and Hsiao Lan Liaol and the SPL compiler was imple mented by Jaejin Lee Mark Stickel provided the AC matching and unification facilities For example it is in general not possible to instantiate an existentially bound rigid variable by a term containing flexible variables 1 6 ACKNOWLEDGEMENTS 11 Harish Devarajan implemented the decision procedure for full Presburger arithmetic As sistance and feedback has been provided by Anuchit Anuchitanukull Luca de Alfarol Jeff Kamererl and Yoshihiro Yamada We would also like to thank Paul Neves and the students of CS256L at Stanford The sTeP logo was designed by Anuchit Anuchitanukul STeP has mainly been implemented in Standard ML of New JerseyI using its X windows utilities eXene for the user interface David McQueen and John Reppy have been helpful assisting us in using SML NJ and eXene Xavier Leroy introduced us to ML The polyhedral invariant generation uses the polyhedral manipulation package developed at VERIMAG CNRS Grenoble by Nicolas Halbwachsl Yann Eric Proy and Herve Leverge The model checker uses the PTL satisfiability tester by Hugh McGuire at Stanford The sTeP project has been sup
74. e format for transition systems was given in Section 2 6 As with programsT the transition system is displayed in a separate window unless the STEP SHOW LOADED environment variable is OFF Loading a new transition system 3 1 MENU OPTIONS 39 Program mux pet1 spl local y1 y2 bool where y1 false y2 false local s 1 2 P1 10 while true do I1 noncritical I2 yl s true 1 I3 await y2 V s 2 I4 critical l5 y1 false P2 m0 while true do m1 noncritical m2 y2 s true 2 m3 await yl V s 1 m4 critical m5 y2 false Control correspondence 7 pid 6 pil 6 Figure 3 4 Program Window for program MUX PET1 40 CHAPTER 3 THE TOP LEVEL INTERFACE terminates the current verification session Load specification Loads a specification a list of axioms and properties to be proved from a file The default extension of a specification file is spec The input format of specification files was given in Section 2 3 Each property becomes the root of a separate proof treel and the first one appears in the current goal window If a specification file is loaded during another goal session the current proof search is suspended and the first property in the specification file will become the new current goall as the root of a new proof search The old proof searchl howeverl remains in the systeml and may be returned to later e g with the select search op
75. e integer integer integer value u variable uLe array access e parenthesized expression e tuple of expressions equal not equal less than greater than less than or equal to greater than or equal to unary minus 1 mod z modulo 1 div amp integer division 1 9 addition 1 3 subtraction 1 9 multiplication ey 3 rational division Prod i 6e1 6 5 6 product Sum 2 61 9 summation negation le negation ey 3 conjunction ey M e disjunction 1 gt 2 implication e1 lt gt ez equivalence Forall u e universal quantification Exists u e existential quantification Exists u e unique existential quant Table C 2 SPL expressions APPENDIX C DIFFERENCES WITH THE BOOK In STeP Description Base type integer i integer boolean boolean rational rational Simple type range range range type ty X X tk ox k tk tuple type values values enumeration type Complex type array ranges of T array ranges of T array type channel of 6 channel of b synchronous channel 1 of b channel 1 of b unbounded asynch channel range of b channel range of b bounded asynch T T parenthesized type SPL types in STeP or schematic statement i e any statement that has no substatements The sTeP version of the same program schema is presented in Figure C 2I which lists all the control counters used in italics and their
76. e its value may change from one point in time to another By defaultT auxiliary variables are rigid Auxiliary variables are often used as part of macros and rewrite rules For conveniencel a specification may also include declarations for system variables these are further described in Section 2 5 Example The declarations variable x y z int variable a b c bool Flexible variable i 1 N declare the rigid integer type variables zy and zI the flexible boolean variables alb and cl and the rigid variable i of type range 1 N Previously declared auxiliary variables can be used in quantificationIl so the type of the quantified variable type does not have to be declared within the quantifier see Section 2 2 2 4 4 Rewrite and Simplification Rules Specifications can also include simplification and rewrite rules to efficiently build in equa tional axiomsl as well as ordering relations to control automatic rewriting 2 4 DECLARATIONS 23 User defined rewrite rules can be specified in one of two ways rewrite rules declared with the REWRITE keyword are applied under the user s controlUstep by stepl in the Interactive Prover Simplification rulesI declared with the SIMPLIFY keywordl are applied automatically and exhaustively whenever the Simplifier is invoked from either the Top level Prover or the Interactive Prover ThusT the set of user defined simplification rules is expected to terminate while the set of rewrite rulesl unde
77. e File menu option Both will bring up a confirmation window asking if you really want to exit STeP 9 2 MUX SEM Mutual Exclusion We now assume that you have started sTeP and are able to load program and specification files The program and specifications mentioned in this section are available in the directory examples mux sem local y integer where y 1 lo loop forever do mo loop forever do fi noncritical noncritical fo request y zu request y ls critical critical f4 release y release y Figure 9 1 Program MUX SEM mutual exclusion by semaphores We begin with the proof of two simple safety properties for the program MUX SEMI shown in Figure 9 1 the firstly states that y is always greater than 0l and the second y2T expresses mutual exclusion These properties are expressed by the formulas p Oly 0 p2 O s ma or in sTeP s input formatI gi Oy gt 0 Q3 11 3 N m3 9 2 MUX SEM MUTUAL EXCLUSION 93 To illustrate the various methods available for verification we will prove these properties in a number of different ways In this example we will load each property from a separate file Subsequent examples will illustrate specification files with multiple propertiesl as well as entering goals directly 9 2 1 Using B INV The first property O y gt 0 l is inductivel so we should in principle be able to be verify it using rule B INV We can do this in
78. e formulal or simply as an assertion A temporal formula is constructed out of state formulas by applying the boolean operators 5 and V the other boolean operators can be defined from these l and temporal operators There are two classes of temporal operatorsI future and past The future and past temporal operators used in STeP are presented in Tables B 1 and B 2l respectively Operator Name STeP representation Henceforth p Eventually p lt gt p Until Until p Waiting for Unless q Awaits Next p O Table B 1 Future Temporal Operators Operator Name STeP representation So far p Once p lt gt p Since q Since p Back to q Backto Previously p Table B 2 Past Temporal Operators A model for a temporal formula p is an infinite sequence of states o so 5 where each state s provides an interpretation for the vocabulary of pl i e the variables occurring in p For a given state s and state formula gl we write s F q when q is true when evaluated over sj Given a model o we now present an inductive definition for the notion of a temporal formula p holding at a position j gt 0 in eI written as c 7 E p 113 114 APPENDIX B LINEAR TIME TEMPORAL LOGIC e For astate formula pI o j Ep 4 gt 5 Ep That isl we evaluate p locallyl using the interpretation provided by s Sj Fop 0 j p Ep V q lt gt 0 7 Epor 0 7 Eq Op lt gt forall k gt jl o k Ep Ep
79. em proving session environment does not include a system ThuslI properties are proved to be generally valid in this casel and only the Simplifier and the Interactive Prover can be used to prove formulas Goal session A system verification or theorem proving session may contain multiple goal sessions Each unfinished proof of a goal is represented by a tree with the goal as its root At any given timel only one tree is being worked on The user can move from one tree to the next in the middle of a proofl and later return to the unfinished proofI e g l when some auxiliary properties have been established A goal session ends when the goal is proved valid or is abandoned by the user Properties We use different terms for properties depending on their status in a verification or theorem proving session We list the terms here in alphabetical order Axiom An aziom is provided by the user and is assumed to be valid throughout a system verification or theorem proving session An axiom is considered to be a background property Background property background property is assumed or proven to be valid for the program in a system verification sessionl and assumed or proven to be generally valid in a theorem proving session The user controls their use in simplification by activating and de activating them Background properties may also be deleted altogether from a verification session If activel background properties are used by the Simplifier i
80. ement S and 55 will move control appropriately from 5 to S2 e Parameterized Cooperation n n With the statement i 1 N 2 SE i we associate two transitions P Tl entry and Tepa l with transition relations Dig Move l 4i i 1 NJ A pres Ys Pg move lji i2 1 N A pres Ys They are the parameterized versions of the transitions associated with non parameterized cooperation 112 APPENDIX A COMPUTATIONAL MODEL e Parameterized Or No special transition is associated with parameterized selection This reflects that the construct is the parameterized version of standard or e Blocks Blocks are used to encapsulate variable declarations and don t generate transitions on their own Grouped Statements To compose several simple statements into one atomic entityl SPL provides the grouping construct lt lt gt gt For instance the transition associated with a grouped statement of the form lt lt S1 S2 gt gt is the relational composition of their transition relations Appendix B Linear Time Temporal Logic As a requirement specification language for reactive systemsI we take linear time temporal logic There is an underlying first order assertion language over interpreted symbols for expressing functions and relations over concrete domains such as the integers arraysl and lists of integers see Section 2 1 We refer to a formula in the assertion language as a stat
81. encel 17 ORDER syntax 23 135 ordering relationl 221 23 out mode I25 out syntax L 27131 output window top level proverL 35 P valid formulal 114 verification diagramI 60 parameter in hierarchical verification diagramI 68 parameterized programsI 25 parser helpI 33 past formula 10 past operators 10 Past temporal operatorsT 113 polyhedral invariants environment variablesIl 128 polyhedral invariants menu option P45 Postpone ip button I 85 precedenceD 17 Presburger ip button I 89 Presburger decision procedurel 89 previous tlp button P48 primed variabler 105 primingDl 17 Prod operator 28 produce statement semantics 109 produce syntax 27 Product syntax l 16 program loadingDl 91 program variablesD25 program verification session terminatingDl 40 Progress syntax 31 progress condition 32 proof search 51 proof tree in Interactive ProverI 81 navigatingI 52 tutoriall101 properties menuI 41 P TL expansion ip button 90 quantifiers 17 136 quit menu option l40 quitting sTePI 92 range type declaration Ll 13 real time systemsI 32 receive statement syntax 27 Redo ip button P85 redo tlp button P48 release statement semanticsT 108 release syntax 27 repeat SPL construct syntax 27 repeat tactic 74 Replace ip button 88 request statement semanticsT 108 request syntax 27 reset all menu option P40 reset BDDs menu option l48 reset searches menu option P40 Rewrite ip but
82. ere are two ways to express such formulas In a formula of the form Na lt 1 i e the number of processes at location 3 is less than 1 Il the recommended sTeP represen tation is the following Forall i 1 N Forall j 1 N 3 i 13Lj gt i j This may be generalized to small numbers greater than 1 using disjunction in the consequent When this representation is not possiblel e g l in a formula of the form N3 y 2 you can use Sum as follows Sum i 1 N 13 y z We discourage the use of Sum for the simpler cases because reasoning with Sum is more difficult than reasoning with quantifiers only Appendix D Distribution and Installation Installation STeP is available for platforms that are supported by Standard ML of New Jersey ver sion 1 08T including e Sun SPARC workstations SunOS and Solaris e DEC Alpha workstations OSF1 You should have copied the distribution file specific to your machine The only difference is in the binaries included with each Files associated with running STeP are located in the bin directory The executable files are found in the bin and heap directoriesl and accessed through the STePIpolyservl and model checker scripts These scripts determine the machine type and operating systemI using the arch n opsys command l and then invoke the appropriate binary file from the run or bin directory on the given arguments ThusFPnone of these files should be moved or renamed
83. erification rule A verification diagram is chosen to be the current one by the Current to verify menu option in the Verification Diagram Editor 3 1 MENU OPTIONS 4T The Logical rules Menu The Logical rules pull down menu Figure 3 10 provides inference rules that simplify tem poral properties ThusI they can be used to derive new properties from previously proven ones Unlike verification rules these rules are independent of the system being verified Section 4 4 presents a full description of these rules FPF ae in File Properties Tactics Diagrams RENT Figure 3 10 Logical Rules menu The Settings Menu The Settings pull down menu Figure 3 11 controls some of the global sTeP environment variablesl such as automatic simplification of subgoals and the strength of the Simplifier File Properties Tactics Diagrams Logical rules Ani E No searches Equality Auto OFF No current goal Figure 3 11 Settings menu Automatic Simplification ON OFF Sets and resets automatic simplification see Sec tion 4 1 Simplification Flags Brings up a window used toset the default strength of the Simplifier See Section 6 1 for more details 48 CHAPTER 3 THE TOP LEVEL INTERFACE Reset BDDs Resets the internal BDD package if the package is used oftenI this option can be used sporadically to save memoryl at some usually small short term efficiency loss see Section 6 2 This option should also be used if the number o
84. erification rules B BACKTO G BACKTO See Section 4 2 for a description of the main verification rules in their basic and general versions Section 4 2 also describes the and proof rules The remaining buttons in the action region invoke the Interactive Prover and the Sim plifier as proof rulesl applied to the current goal 3 2 ACTION BUTTONS 49 Invokes the Interactive Prover on the current goal The Interactive Prover window will appear with the current goal as the single consequent in the sequent Once the Interactive Prover is activel the Top level Prover is suspendedI to be reactivated when the Interactive Prover session is finished Upon exiting the Interactive Prover you have the option to return the result to the Top level Prover If the goal was provedI then the current goal is closedl and the next goal in the proof treel if anyl becomes the current goal If the goal was not provedl a formula equivalent to the remaining subgoals is returned to the Top level Prover as a new subgoal The Interactive Prover is described in Chapter 8 Modelcheck Invokes the Model Checker on the current goal Before the Model Checker starts you can enter additional assumptions to limit the search space If the goal is proved without any additional assumptionsI the current goal is closed and the next goal in the proof tree if anyl becomes the current goal If the goal is not provedl it remains unchanged If the goal is proved under addition
85. ertiesl or delete them altogether A property is deac tivated by clicking on the switchl and removed by clicking on the skull icon The buttons Select All and Deselect All select or deselect all the listed properties No window will appear when there are no background properties Select goal This menu option allows you to move to another open goal in the current proof tree When selectedI it displays a window listing all open goals in the current proof tree seel for examplel Figure 3 7 Each goal has a select button By clicking on the corresponding goal is made the current one The button returns to the current goal Next search Moves to the next proof tree with open subgoals The previous proof tree is kept in its current statel and may be returned to later This option is useful if you reach a dead end in a proof and realize you need to prove another property first 42 CHAPTER 3 THE TOP LEVEL INTERFACE Property Checklist tint Forall n int m n g d m n ged m n n invariant Active ID MN l4 gt 2 lt a invariant Active UD ee ee UD ee ee lt yl ited ade gt yl Deselect all Figure 3 6 Activate Deactivate Window 3 1 MENU OPTIONS 43 2 Initial Condition length ack N A length send 0 A10 A m0 gt length send length ack I3 m2 N 3 idle flength send length ack I3 m2 Nj Transition idle NoFaimess flength send length ack I3 m2
86. es are enclosed in the region indicated by the dashed rectangle An inquisitive user may wonder why the Verification Diagram Editor does not check for parsing errors The reason is that to check parsing errors one requires knowing the system for which a diagram is being applied to However sTeP allows the Verification Diagram Editor to run independent to any system This feature is useful when the same or similar diagrams uare being applied to different systems 5 6 VERIFICATION DIAGRAM EDITOR INTERFACE 65 This tool is used to draw non terminal nodes After selecting it move the mouse to the location where you want the upper left corner of the new node and click on the left button while keeping it pressed move the mouse down and to the right until the displayed shape has the proper dimensions Releasing the button will then create the node The node will be initially selectedl and the two editable fields above the diagram will contain the default name and label for this node You can edit the name field and enter a state assertion for this node To resize an existing nodelI select it with the left button after first selecting the pointer tool move the mouse to one of its cornersl and resize the node while keeping the button pressed on the black square in the chosen corner Works exactly as the tool for non terminal nodesl but the generated node is a terminal node This tool draws an edge without an associated fairness requireme
87. ess 96 9 2 3 Using the Model Checker lens 97 9 2 4 Using Verification Diagrams een 98 9 2 5 Using MON I and Linear Invariants lens 100 9 3 MUX PETI Invariance Strengthening eee 100 9 3 1 Using WPC lle Rss 100 9 3 2 Using Tactics 4 lee 102 9 3 3 Using verification diagrams es 103 Appendix CONTENTS iii A Computational Model 105 A l Fair Transition Systems lees 105 A 2 Computations 2 2 ll l4 4 ehh n 106 A 3 SPL semantics 2 2424222 ee 106 B Linear Time Temporal Logic 113 C Differences with the Book 115 C SPL Programs hs 115 C 2 Control Locations in STeP 22 2 115 C 3 Type Declarations llle 121 C 4 Initialization 4 2 e 121 C 5 Parameterized Programs ees 122 D Distribution and Installation 123 D 1 Example Programs 2 ll less 124 E STeP Environment Variables 127 CONTENTS Chapter 1 Introduction The Stanford Temporal Proverl srePl supports the computer aided formal verification of concurrent and reactive systems based on temporal specifications Reactive systems main tain an ongoing interaction with their environmentl and their specifications are typically expressed as constraints on their behavior over time STeP is not restricted to finite state systemsI but combines model checking with deductive methods to allow for the verifica tion of a broad class of systemsT including parameterized N
88. f BDD nodes reaches the maximum given by the STEP_BDD_NODES environment variable see Section E Clear text window Clears the output windowT but has no other effect on the system System information Prints out miscellaneous statistics in the output window for the current verification session mostly related to the BDD package see Section 6 2 The Help menu On line help is available via your favorite WWW browser when clicking on the Help menu near the right corner of the top level interface T he hyper text help pages give an alternative and often quicker introduction to sTeP s facilities 3 2 Action Buttons The right hand column of the Top level Prover contains rules to manipulate and construct the main proof search The first four buttons manipulate the structure of the proof tree This button makes the parent of the current subgoal into the current goal The previous goal is rememberedI to enable a Redo until another verification rule is applied to the new goal Redoes a previous UndoT that isl restores the part of the proof tree eliminated by Unde Postpones the current goall and turns the previous subgoal in the subgoal queue into the current subgoal Postpones the current subgoal and moves to the next subgoal in the subgoal queue The next set of buttons invoke verification rules as described in Manna and Pnuelil 1995 These rules are not applicable if there is no current program or transition system V
89. ff c j F qVfor all models o and all positions j gt 0 If p q then p can be replaced by q in any context i e o p q for any formula y p containing occurrences of p The notion of temporal validity requires that the formula holds over all models Given a program PI we can restrict our attention to the set of models which correspond to com putations of Pl i e Comp P This leads to the notion of P validityl by which a temporal formula p is P valid valid over program P if it holds over all the computations of P ObviouslyI any formula that is temporally valid is also P valid for any program P In a similar wayl we obtain the notions of P satisfiability and P equivalence A state s that appears in some computation of P is called a P accessible state A state formula is called P state valid if it holds over all P accessible states Obviouslyl any state formula that is state valid is also P state valid for any program P AgainI we refer to a P state valid formula simply as P valid Appendix C Differences with the Book STeP was implemented based on Manna and Pnuelil 1995 HoweverIdue to implementation considerations and limitationsl there are some differences between sTeP and Manna and Pnuelil 1995 P hereafter referred to as MP95 For the convenience of those using STeP together with MP95I this appendix highlights most of the differences These are deviations from the syn
90. fication procedures Note that no simplification rules are given for first Nil and next Nil although these expressions are well typed Their interpretation is left underspecifiedT but they are not erroneous For the constructorsl axioms asserting injectivity are also asserted automatically and used by the simplifier so they don t have to be declared Forall t tree Forall f forest Nil Cons t f Forall i j ident Forall ci c2 forest Node i ci1 Node j c2 gt i j cl c2 Forall ti t2 tree Forall sibi sib2 forest Cons ti sibi Cons t2 sib2 gt ti t2 sibi sib2 The complete axiomatization of datatypes also includes well founded induction schemas see Manna and Waldingerl 1993 These are not automatically provided in the current release of srePI so the user may have to provide suitable instances 2 4 2 Value and Macro Declarations Program and specification files may contain value and macro declarations Their syntax is given by the following grammar value decl value ac ids type gt type value declaration macro decl macro id type gt type macro declaration where id ids expn 2 4 DECLARATIONS 21 ac AC COMMUTATIVE ASSOCIATIVE ids n dd id identifier list Uninterpreted function symbols are declared as values Binary function symbols can have additional attributes used by the Simplifier the keyword AC states that the function is both associative and commut
91. for SPL program files The right column shows the directory hierarchyl and the left column shows the files in the current directory Clicking on a directory in the right column makes it the current directory You can load a file by clicking on its filename in the left column Alternativelyl you may enter the full filename directly in the entry line under File name After entryl click the buttonl and the selected file will be loaded Loading the specification To load a specificationl select the Load specification option from the File menu Againl this activates the File Browser which brings up a Load specification window The default extension for specification files is spec If the specification file contains a single formulal this formula is understood to be the top level goall and is displayed in the top window as the new current goal If the file contains multiple formulas to be provedI the first one 91 92 CHAPTER 9 BASIC TUTORIAL is displayed as the current top level goal The other top level goals can be accessed by selecting the Next search or Select search option under the Properties menu Specification files can also contain declarationsl axioms and definitions see Chapter 2 Help At any timel you can get online help by selecting the Help option from the menu This will bring up a WWW browser with sTeP s help pages Quitting STeP To leave sTePl select the Quit option from the top level menu or select the Quit option from th
92. g method for indexing terms Technical Note 473 SRI International Menlo Park CAT October 1989 ZhangL1993 H Zhang Contextual rewriting in automated reasoning Technical Report Technical Report 93 07I Department of Computer Sciencel University of Iowal August 1993 Index O initial condition 53 T successorl105 move C P107 pres U V107 T set of transitions L 53 type constructor L 13 Model CheckerP56 environment variablesT 128 1 Step Propositional ip button I 85 abandon search menu option 44 AC associative and commutativel 21 accessible stateL 114 action region top level prover I 35 activate deactivate menu option 41 Add axiom ip button Dl 90 All Propositional ip button 90 append syntax 16124128 arithmetical operators syntax r 16 arithmetizationl 14134 array type declaration 13 array initialization difference with bookTI121 array reference syntax 16 arriving edge 62 assign example r16 assign syntax l 16L 28131 assign fieldT 29 assignable expressionI27 assignment statement semantics 107 assignment relationI 29 ASSOCIATIVELD 21 associative functions simplification settingI 70 asynchronous receive statement seman tics 108 131 asynchronous send statement I semantics 107 atomic tacticI 72 automatic simplification 52 automatic simplification menu option r47 auxiliary variabler 9 auxiliary variables 9r 22 await statement semanticsr 107 await syntax r27 Awaits
93. generated p false Contradiction 4 5 The Model Checker Model checking determines if a given temporal formula holds for a given system by a sys tematic exploration of the state space of the system sTeP includes a model checker for transition systems and formulas of linear time temporal logic which can be used to close subgoals or produce counterexamples to particular properties The sreP model checker checks the current goal under an optional additional first order assumption If the goal is found to be falsel a counterexample is reported 4 5 THE MODEL CHECKER 57 When the proof rule is invokedl a dialog window appears requesting the input of an auxiliary first order assumption by default true You may enter restrictions on parameters or system variables with infinite domainsl in order to make the program finite state For exampleI for the program MPX SEM you may enter M 2l indicating that the number of processes you want to consider is two The goal is closed only if the Model Checker proves it with assumption true The Model Checker Preprocessor The Model Checker first applies a preprocessor to the given system and the goal If possi blel a finite number of problem instances with constant size arrays and constant bounded parameters equivalent to the original goal is produced If this is not possiblel the Model Checker terminates control returns to the Top level Prover and a message is displayed Some of the tasks
94. generated invariants can be classified in the following three groups 1 Finite domain invariants Invariants of the form terra Vr aV Vr c where is a program locationI c c are constants and x is a program variable 2 Conditional invariants Invariants of the form J 2 condI where l is a program loca tion and cond is a formula arising from the initial condition or a branch statementI 79 80 CHAPTER 7 AUTOMATIC GENERATION OF INVARIANTS e g gt the program fragment if cond then 11 S1 else 12 S2 generates the condi tional invariants 11 condl and 12 gt condI if no variables in cond are modified by parallel statements 3 Range invariants Invariants of the form l gt lb z z ubl where b and ub are integer or rational constants or infinity 7 2 Linear Invariants Linear invariant generation arises from analyzing the linear relationships between system variables in the course of a program The invariants generated are usually linear equalities of the form 414 aozo antn b where a1 an bare constants Each x can be a a variabler b the sum Sum i m M A i T of the values of an arrayl or c a sum Sum i m M x i where x is a local variable of a parameterized process P i m M 7 3 Polyhedral Invariants x The polyhedral invariant generator is the most powerful of the methods provided currently in experimental state The invariants generated depend on the set of v
95. has at least one helpful transition associated with it Chain diagrams allow proving progress properties that do not require an infinite size well founded domain Later releases of sTeP will allow the user to enter well founded domains as part of the chain diagram Verification Conditions Let y be a nonterminal node and q qi Uk gt 0l be the r successors of q e If 7 labels a single edgel we associate with y and 7 the usual verification condition teiriev ei v V pr e If 7 labels a double or solid edgel we associate with y and 7 the verification condition ieri v v ge 62 CHAPTER 5 THE VERIFICATION DIAGRAM EDITOR e If 7 labels a double edge departing from ylwe associate with v and 7 the implication o gt En r i e when holdsI 7 is enabled e If 7 labels a solid edge departing from yl we associate with y and 7 the compassion requirement in the form of the response formula p Oly V En r Valid Chain Diagrams A CHAIN diagram is P valid if the first three types of verification conditions are P state valid and the compassion requirements associated with solid edgesl are P valid A P valid CHAIN diagram establishes that the response formula V Qj gt vo j 0 is P valid To establish the P validity of prod the following two additional side verification conditions have to be established p V Vj FC1 po gt 4g FC2 5 5 Compound Nodes To make verification diagrams more readablel STeP supports enca
96. he following are not Presburger formulas 90 CHAPTER 8 THE INTERACTIVE PROVER x Forall x int Exists y int f x y gt 0 Exists x int Forall y rat x gt y since the first contains an uninterpreted function symbol fI while the second includes the unsupported type rat All Propositional Applies 1 Step Propositional recursively until there are no new formulas to which it is applicable BDD split Simplifies the purely propositional structure of the formulas in the sequent T us a formula whose main connective is a temporal operator lt gt Awaits Until Since Backto lt gt Tis treated as an atomic formula as opposed to All Propositional See Section 6 2 for further explanations Add Axiom A list of previously established properties or asserted axioms is displayed in a separate window The user selects the previously proved property or asserted axiom to be inserted in the antecedent of the sequent The Select boxes menu option under Settings allows the user to automatically remove or retain preceding boxes from the axioms added by Add Axiom By default boxes are removed from axioms added to the sequent Example By defaultl adding the axiom p x q y to the sequent T gt A generates p x A a y P A Selecting Select boxes keeps the boxes Hence adding the same axiom generates the sequent p x A q y P A PTL expansion The structure of the Gen
97. he following two side verification conditions have to be established O gt Vijay I Viziv 2 5 4 Chain Diagrams x Verification diagrams can also represent fairness requirements The main extension over the previous types of diagrams is the introduction of two additional types of edges double and solid A double edge corresponds to a helpful transition that is justl and a solid edge corresponds to a helpful transition that is compassionate Thusl edges connecting nodes in a diagram can be singlel double or solid A verification diagram is said to be a CHAIN diagram if its nodes are labeled by assertions 0 Pml with Yo being the terminal nodel and if it satisfies the following requirements e If a single edge connects node y to node o I then i gt 7 e If a double or solid edge connects y to y Tthen gt J e Every node li gt 0DPhas at least one departing edge which is either double or solid The transition labeling this edge is identified as helpful for assertion q e Every transition can label at most one type of edge singlel doublelor solid departing from the same node The first two requirements ensure that the diagram is weakly acyclic in the same sense as defined for the WAIT FoR diagram The stronger second requirement ensures that the subgraph based on the double and solid edges is acyclicI forbidding self connections by double or solid edges The third requirement demands that every nonterminal node
98. he invariant generation is finished a message will appear in the message window Newly generated invariants are simplified using the basic simplification and decision proceduresl independently of previous background properties Invariant generation and simplification can be halted by clicking on the interrupt button the sTeP logo Get local invariants Activates the local invariant generator requires an SPL program Get global linear invariants Activates the linear invariant generator requires an SPL program or fair transition system 3 1 MENU OPTIONS 45 Get global polyhedral invariants Activates the polyhedral invariant generator after prompting the user for a number of parameters that control the generation method See Chapter 7 for details Polyhedral invariants are generated for SPL programs and fair transition systems Enter axiom Used to enter a property that the system may assume to be true during the current program verification sessionl i e l it is added to the list of background properties By defaultI the new axiom is activel and will thus be used by the Simplifier Note STeP does not guarantee the consistency of the set of background axiomsI nor does it require you to prove any of themI so this feature should be used with caution Enter new goal Used to enter a new goal to be proven If the formula parses correctly it will become the root of a new proof treel which is made the current proof tree while the previous one is put
99. he negation of the propositional models that can falsify the formula If all the subgoals are valid the original goal is valid as well 72 CHAPTER 6 AUTOMATIC THEOREM PROVING In the worst casel exponentially many children are produced using this expansionI but in most applications there is a good chance that it will work well The acceptable maximum number of subgoals is given by the STEP BDD SPLIT environment variable In the Top level ProverIthe active background formulas are automatically used to reduce the number of subgoals generated in the Interactive ProverI the background formulas must be added to the sequent before invoking BDD split This is analogous to the behavior of the Simplifier in the two provers 6 3 Tactics x Tactics are a method to automate parts of the high level proof search by encoding long or repetitive sequences of proof commands An individual proof command is an atomic tactic The Top level Prover and the Interactive Prover share the same tactic languagel param eterized by their atomic tactics since each has a different set of proof commands The general syntax of a tactic is as follows tactic predefined Predefined tactic composite Composite tactic atomic Atomic tactic predefined skip Identity tactic fail Failure tactic composite try tactic tactic tactic then form tactics sequence tactics else tactics repeat form tactic spread tactic tactics branch tactic tactics
100. her causal ity properties If the current goal has the form p gt rIthis option displays a dialog window for entering an auxiliary assertion After a new assertion q is entered default is r the following two subgoals are generated p QOq Left Transitivity q Qr Right Transitivity MON C The monotonicity rule for causality can prove a causality property from a stronger causality property If the current goal has the form p gt ul for past formulas p and ul this option generates a dialog window for entering two auxiliary assertions After entering the two assertions q and r defaults are p and u the following three subgoals are generated p Monotonicity 1 q gt Qr Causality r u Monotonicity 2 MON W The monotonicity rule for wait for formulas can be used to prove a wait for formula from a stronger wait for formula If the current goal has the form p nW Waol a dialog window will appear for entering n 2 auxiliary assertions The default assertions are pl q I qo After entering these assertions Prew n news GO new and clicking the buttonI the following n 3 subgoals are generated P pae Monotonicity dn new n Monotonicity n qo new do Monotonicity 0 and Pnew gt Yn new W tt W do new CONT The contradiction rule can be used to prove a general safety property by converting it into a causality formula If the current goal is of the form pl for past formula pl the following subgoal will be
101. his button all terms that are candidates to be replaced are high lightedl and you can select the term that you want to replace with Example Starting with the sequent x 3 y 4 X X yey 25 clicking on highlights xPyP3l and 4 Clicking on 3 replaces x with 3 in the consequent resulting in x 3 y 4 3x3 yey 25 Brings up the Select rewrite windowl which displays all rewrite rules that were declared in the specification during the current verification session via REWRITE desc expn gt expn Rules can be selected and de selected by clicking on the buttons When clicking on the buttonIthe current goal is simplified according to the selected rewrite rules Make first order Upon clicking on this button with current goal sequent GTa first order subgoal G is generatedI such that the first order validity of G implies the first order temporal validity of G Upon clicking on this button a new subgoal is created in which the operator is deleted from sub formulas preceded by itl and in which is appended to sub formulas not preceded by 8 3 INTERACTIVE PROVER RULES 89 Cut With the Cut rule you can perform a case split analysis on the current goal Upon clicking on this buttonl a dialog window will appearI where you can enter the formula to split on Thus upon having entered the cut formula pH Cut implements the inference rule T p A T gt A p LU A Upon clicking on this button
102. implification rule is called Navigating the Proof Tree The options in the Interactive Prover I Previous T Next in the Top level Prover land Select goal in both provers can be used to jump from one open node to another The and buttons alternate between a given node and its children In the Top level Proverl any number of proof searches can be conducted simultaneouslyI sharing the same set of background properties The button can be used to jump from one proof search to the next Automatic Simplification A verification rule can generate a large number of verification conditionsl depending on the size of the underlying transition system After having applied a verification rule a message in the message window will display how many subgoals were generated If automatic simplification is OFFthe first subgoal will be displayed in the specification window All the generated subgoals can be viewed by selecting the Select goal option of the Properties pull down menu If automatic simplification is ONT the Simplifier will be applied to each subgoal Only those subgoals that fail to simplify to true will remain Simplifications steps which fail to simplify to true will be undone to enable subsequent application of rules such as and WPC these are only applicable to unsimplified verification conditionsl since they require knowing the particular transition that generates the verification condition When automatic simplification is
103. in Manna and Pnueli1994 and Manna and Pnuelil 1995 STeP currently supports three types of verification diagrams e Invariance diagramslto represent proofs of invariance formulas p e Wait for diagramslto represent proofs of nested wait for formulas P gt daYY qui Vqo e Chain diagramslI to represent proofs of response formulas p gt q that do not require induction Herel pl qT qo qn are state assertions Hierarchical verification diagrams Section 5 7 support distributing a large verification diagram over several files 5 1 Definitions A verification diagram is a directed labeled graph constructed as follows e Nodes in the graph are labeled by assertions e Edges in the graph represent transitions between nodes Each edge connects one node to another and is labeled by the name of a transition in the program We refer to an edge labeled by 7 as a r edge e One of the nodes may be designated as a terminal node This node is distinguished by having a boldface boundary No edges may depart from a terminal node 59 60 CHAPTER 5 THE VERIFICATION DIAGRAM EDITOR Verification diagrams represent sets of verification conditions as follows For every non terminal node labeled by y and transition 7T let yi be the nodes to which is connected by r edges The verification condition associated with and T is given by fe T eV el V V yr Note that if k OVi e no 7 edges depart from
104. ion conditions are simplified to truel the proof is completel as indicated The single original goal has now been provedI so there is no current unproven goall as indicated in the current goal window The proved property is saved as a background property and can be used in the proof of subsequent properties The background properties can be viewed by selecting the Activate Deactivate option under the Properties menu This brings up a Property Checklist windowl shown in Figure 9 5 By defaultl properties are active and will be used in the proof of subsequent properties Howeverl you may deactivate a property by clicking on the switch next to it Inactive properties can be reactivated later on howeverl you may also entirely delete a property by clicking on the skull To save the proof to a file in ASCH format Pselect the Save last proof option of the File menu The File Browser brings up a window with the title Save completed proof 94 CHAPTER 9 BASIC TUTORIAL Program mux sem j local y int where y 1 FII 10 while true do I1 noncritical I2 request y I3 critical I4 release y P2 m0 while true do m1 noncritical m2 request y m3 critical m4 release y Control correspondence pid 5 pil 25 pid 0 pid 1 Figure 9 2 MUX SEM program text window 9 2 MUX SEM MUTUAL EXCLUSION 95 File Properties Tactics mux sem spl 1 goal Eq Y Figure 9 3 Loaded specification for MUX
105. ion under the Settings menu 3 Generate local invariants by selecting the Get local invariants from the Properties menu 4 Invoke rule B INV As may be expectedI the verification conditions for 4 and m3 do not simplify to truel since they are not valid The first unproven verification condition is now displayed in the current goal window in unsimplified form The other open subgoallIthe verification condition for 3I can be viewed by selecting the button Again selecting goes back to the previous goal The Proof Tree We interrupt our proof for a moment to look at the construction of the proof tree We started with the property we wanted to prove as the single top level goal This goal is the root of the proof tree When rule B INV was appliedI 15 subgoals were generated in this case these are the verification conditions for monotonicity always trivial for B INV Tl initial conditionl the idle transitionI and the 12 program transitions Since automatic simplification was onl all but two of these subgoals were immediately simplified to true and closedI which left us with two open goals The buttons and allow you to cycle through the entire list of open goals in the tree Two other buttons that manipulate the proof tree are and Redo Applying to a subgoal returns to its parent in the proof treel and the subgoal and all its siblings are removed from the tree Howeverl they may be recovered by clicking on Redo which restores the pr
106. kets or percent signs is ignored 68 CHAPTER 5 THE VERIFICATION DIAGRAM EDITOR Parameter Passing Hierarchical verification diagrams allow macro like text replacement when importing a ver ification diagram Parameters in the node to be imported are of the form 1 2 T 3 Tetc Tand 01 is replaced by the first argument passed by the importing noder 2 is replaced by the second argumentI etc When the top level diagram is processed i e I when it is used as a verification rule by the Top level Prover l sTeP checks whether the number of parameters each imported diagram requires is equal to the number of arguments passed The arguments passed by the import node are included in the assertion field each argument is enclosed within percent signs 4967 An example of the assertion field of an import node that passes parameters is lt mux pet2 mux hi diagram gt 4m3 413 4s 17 The arguments do not have to be on the same linel and white space is ignored Edges The connection of edges between the import node and the imported diagram is done by matching unconnected outgoing edges in the imported diagram also called dangling edges with outgoing edges of the import nodes that have the same labell and similarly for incoming edges If multiple edges of the imported diagram match multiple edges of the import nodel then edges are created for all possible combinations taking the product over all edges Thusl one incomi
107. l 1995 Like the bookl it concentrates on safety propertiesl and is intended for use by studentsl instructors and researchers of formal methods 1 1 Reading this Manual This manual is a complete reference guide for using STeP For more background on STeP s framework for temporal specification and program verificationIl see Manna and PnueliL1991 and Manna and Pnuelir 1995 Following are some suggestions on reading this manual e Getting started Section 1 2 describes how to get sTeP up and running Section 1 3 gives an overview of STeP and a flavor of how a typical session proceeds Section 1 4 defines the main terms used throughout this manual 1 2 STARTING STEP 3 e The Tutorial This manual includes a basic tutorial on srePI in Chapter 9 This Some sections are marked with a tutorial is the recommended method for readers to familiarize themselves with the STeP interface and the different styles of verification in sTeP After the tutoriall you should be able to verify some of the other programs included in the examples directory as well as your own simple programsl using the rest of this manual as a reference e x to indicate that they should be read only after the unmarked sections are understood For instancel first time users can postpone studying features such as tactics Section 6 3 and user defined rewrite and simplification rules Sec tion 2 4 4 l until they feel comfortable with the rest of the system Sections
108. lifier may be invoked by the userl both from the Top level Prover and the Interactive Proverl to simplify single goals or subgoals In the Top level Proverl the Simplifier uses all axiomsl invariantsl and previously proven properties that are currently active The power of the Simplifierl i e L the trade off between power and speedl is controlled by a number of global settings 8 CHAPTER 1 INTRODUCTION STeP Activities We identify a few nested levels of activitiesl each with its own environment STeP session At the top level is the sTeP sessionI which lasts for the entire period STeP is running Simplification settings are part of the STeP session environment They can be changed at any timeIbut are not affected by loading new systems or moving on to new goals System verification session The next level down is the system verification sessionl which lasts from the time a program or system is loaded until a new one is loaded Proven properties are accumulated as long as the session lasts Thus both the system and all the properties proven about itIl as well as the axioms loaded for itl are part of the system verification session environment All properties proven are valid relative to the current system A system verification session may be terminated explicitly by loading a new system or resetting STeP Theorem proving session At the same level as the system verification session is the theorem proving session The difference is that a theor
109. ll PropositionalI 90 BDD splitI 90 CutI 89 Deleter 85 Duplicater 85 FlattenI 85 Free InductionI 89 Hider 85 Induction 89 Instantiatel 86 134 Make first orderI 88 NextI 88 Postponel 85 Presburgerl 89 PTL expansionI 90 RedoI 85 Replacer 88 RewriteI 88 SimplifyI 85 SkolemizeI 86 Undo 84 Unhidel 85 internal noder 62 interrupt buttonl 37I 77D128 Model Checker 58 invariant generation 79 simplification 70 tacticsI 45 invariance diagramD 60 invariance rule basic B INVI 53 general G INVI53 invariantsI 9 obtaining linearT 44 obtaining locall 44 polyhedralI 45 IP addressI3 just edgel 65 just transitionI 105 Justice syntax P31 length syntax l 1612428 linear arithmetic simplification settingI 70 linear invariants menu option L 44 load batch tactic menu option 45 load interactive tactic menu option 45 load program menu option I38 load specification menu option I 40 load transitions menu option P38 loading batch tacticL 45 interactive tacticI 45 specification 40191 SPL programsI38I91 INDEX tactic 45 transition systemI 38 local mode Il25 local syntax F 27131 local invariants menu option I 44 location disjunction syntax 16 location equivalencel 121 logical rules menu 47 loop forever syntax 27 macro declarationI 21 mailing listI 10 Make first order ip button l 88 menu option abandon searchI 44 activate deactivateT41 automatic simplificationI 47 check runtime systemI
110. lt 1001000 e STEP BDD SPLIT Maximum number of subgoals that are generated by the BDD split rule in the Top level Prover and Interactive Prover If this maximum is reachedI the BDD split rule fails BDD split can generate exponentially many subgoals in the worst case Default 11000 e STEP BDD CACHE Size of the BDD result cachel used for efficient BDD operations Default 321000 Modelchecker and polyhedral invariant resources The following variables limit the space and time used by the external Model Checker and polyhedral invariant packages The _MC_ variables control the Model CheckerI and the POLY variables control the polyhedral invariant generator Both of them will fail if any of the limits is exceeded e STEP MC SPACEI STEP POLY SPACE Maximum amount of memoryl in Megabytes Default unlimited e STEP MC TIME L STEP POLY TIME Maximum amount of user timel in minutes Default unlimited e STEP MC CPUI STEP POLY CPU Maximum amount of CPU timeDl in minutes Default unlimited Finally remember that the interrupt button can be used to interrupt lengthy computations in STeP Bibliography Bj rner et al D1995 N Bj rner I A Browne and Z Manna Automatic generation of invariants and intermediate assertions In First Intl Conference on Principles and Prac tice of Constraint Programmingl volume 976 of LNCST pages 589 6230 Cassisl France September 1995 Springer Verlag BledsoeL 1975 W W Bled
111. m pound node are interpretedl as usuall to represent edges entering or leaving each enclosed node Therefore these edges are considered to be connected to the import nodes and interpreted as usual Chapter 6 Automatic Theorem Proving A computer aided verification system should try to make the task of proving verification conditions as easy as possible while still ensuring soundness To this effectI STeP provides powerfull usually fastl automatic simplification procedures These are supplemented by the interactive Gentzen style theorem proverI discussed in Chap ter Sl used to establish properties that the automatic simplifier cannot 6 1 The Automatic Simplifier There is a basic trade off between the strength and the speed of the automatic Simplifier The more powerful the settings arel the slower the Simplifier is The default settings are a good compromise they are able to simplify most commonly occurring verification conditions in a reasonable time The impatient user may want to use the interrupt button to halt lengthy simplification operations and try alternative proof techniques Selecting the Simplification Flags menu option brings up the window shown in Figure 6 1 It contains the following settings Simplifier Settings Use decision procedures for equality j No decision procedures for linear arithmetic E No special treatment of AC functions j No BDD simplification c Figure 6 1 Simplifier settings 69 70 CHA
112. ments of type integer and result in a value of type integer Users should note that this arithmetization is very convenient but at times confusing see Section 2 7 2 2 EXPRESSIONS e Variables bound by quantifiers may not be array types 15 The full grammar for expressions that can be used in specifications is as follows ezpn ezxpns bv index prefix bind kind bool const int const bool const int const id id index index idCexpns exprLexpns Cexpn Cexpn expns int const expn expn infix expn prefix expn if exrpn then expn else expn bind bv expn expr expn expn expns id id type kind int const int const int const V gt lt gt Until Awaits Since Backto lt gt mod div 2 lt gt gt lt 7 O O lt lt gt append head tail length assign Forall Exists Exists Sum Prod Rigid Flexible true false digit digit boolean value true or false integer value identifier disjunction of locations id can be an array identifier function application array reference parenthesized expression a tuple of expressions int const th projection of tuple infix operator unary prefix operator if then else binding primed expression globally or locally declared bound variable indexing locations binary boolean operators binary te
113. mporal operators entailment and congruence arithmetical operators predicate operators negation minus future operators past operators channel operations array update binding operators flexibility of variable 16 CHAPTER 2 SYSTEMS AND SPECIFICATIONS id x alpha alpha digit _ alpha upper or lower case letter digit number between 0 and 9 location disjunction As an abbreviated notation for the disjunction of consecutive loca tionsI the specification may contain expressions of the form 1 1 5 7 9 11 i which is shorthand for 11f4 V 120i M 1304 V 1404 V i5 i V 170i V 19 i M 110 i V 11103 channel operations are described separately in Section 2 4 5 array assignment Arrays are multidimensional tables Individual table entries can be updated by the built in function assign Example The expression entered below in N M int where N gt 0O M gt O local A array 1 N 1 M of int assign A 5 1 1 is identical to the array Al except for position 1 1 I where it has been updated to the value 5 The simplifier uses the following simplification rule automatically so it really does not have to be declared variable a x 1 N variable b y 1 M variable e int SIMPLIFY assign A e a b x y gt if a 7 x b y then e else Alx y See section 2 4 4 for how to declare your own simplification rules tuple projection The th element of a tuple t can be accessed as it
114. mputation Auxiliary variables in STeP can be declared to be flexible or rigid System variables declared as in are rigid while those declared as out and local are flexible Note that the flexible or rigid status of variables has a significant effect on whether terms under the scope of temporal operators can be replaced by others during inter active and automatic theorem proving Future operators Future temporal operators are Henceforth Eventually 4 Until W Waiting for also called Unless and Next In sreP s ASCII representationl these are 1L P UntillAwaitsland see Ap pendix B lrespectively Past operators Past operators are 7 So far Once PS Since B Back to l and Previously In sTeP s ASCII representationl these are I l Sincel Backtol and see Appendix B lrespectively Past formula past formula is a temporal logic formula that does not contain any future operators that isl it only contains state formulas and past operators 1 5 Feedback If you have problems running STeP or find bugs in the systemI please send mail to step bugs cs stanford edu If you have questions or feedback send mail to step comments cs stanford edu There is a mailing list for sTeP users which will be used to distribute updated information about the system To be added or removed from the listl send mail to step request cs stanford edu 1 6 Acknowledgements STeP has been
115. n left to right order breadth first until the first tactic fails The constructor sequence can be defined in terms of tryl namely sequence tac taco tacs has the same effect as try tac try taco tacsltail fail tactic tactic tac taco is shorthand for then tac tacg The semicolon associates to the left and has the highest precedence else factics Applies the first tactic that succeeds from the list of tactics supplied Figure 6 5 illustrates the result of else tac tac2 tac tac l where tac is the first tactic that succeeds tac XL original goal Figure 6 5 else tac tac2 tac tac repeat form tactic repeat breadth first tac applies tac repeatedly until failure appears on one of the generated subgoals in a layer repeat depth first tac applies tac repeatedly on the left most subgoal generated spread actic tactics 6 3 TACTICS x 15 spread tac tac taco tac applies first tacl and then applies tac to the th subgoal generated The tactic fails if the number of subgoals generated from tac is different from n Also if any of the tactics tac or tac faill the entire tactic fails branch tactic tactics otherwise tactic branch tac tac tac works like spreadl except that if the number of subgoals is m gt nl then it applies tactic tac to the subgoals indexed n n 4 1 m branch tac tac tac otherwise tac first applies the tactic branch tac
116. n the discussion of MUX sEMT Manna and Pnuelil 1995 presents a state space partition graph This graph can easily be converted into the invariance verification diagram shown in Figure 9 8 This diagram may be used to prove mutual exclusion for MUX SEM as follows 1 Reset the background properties and current searches with the Reset searches option under the File menu Load again the mutual exclusion property from the mux sem mux spec file Select the Edit diagram option under the Diagrams menu This brings up the Verifi cation Diagram Editor Select the Load option under the File menu in the Verification Diagram Editor window This brings up the File Browser Select the file mux sem state partition diagram This loads the verification dia graml which is displayed in the editor windowl as shown in Figure 9 8 Select the Current to Verify option of the File menu of the Verification Diagram Editor This will make the verification diagram accessible to the Top level Prover Select the Verification diagram rule option of the Diagrams option This generates all the verification conditions corresponding to the given verification diagram as subgoals If automatic simplification is enabledl the simplifier will proceed to simplify each subgoal 9 2 MUX SEM MUTUAL EXCLUSION 6 Diagram Editor File Edit Node Edge phi IOVITVIZ A mOVm1Vm2 A y 1 m2 l4 phil I3vI4 A mOVm1Vm2 A y 0
117. n the left side of the long doubly lined impli Next jp T A This axiom reflects the well foundedness of time In the first time instancel the truth value of p is false for any formula pl because there is no past at this instance e The sequent T gt A is duplicated along a branch in the proof treeli e the following conditions are satisfied 1 There is a sequent I A between the root and AT such that I C T and A C A 2 The two sequents are separated by at least one application of the Next rule 3 There is an unfulfilled formulalin the sense of the temporal tableau construction Manna and Pnuelil 1995 I for the sequents below applications of Next and above I gt A It helps to think of duplication in the presence of unfulfilled formulas as correspond ing to an induction step The requirement also replaces inference rules formalizing induction on temporal operators Fortunately all these conditions are kept track of automatically and you do not have to worry about the detailed conditionsI so that you can focus on the outline of the proof 8 2 User Interface Figure 8 1 shows the interface of the Interactive Prover It has a menu bar on top and action buttons to the right Most interaction in the Interactive Prover is accomplished by button clicks If a rule is applicable to multiple formulas in the sequentI the candidates are highlighted shown in reverse video and you can select the one to which
118. n the simplification process of goals and subgoals at the Top level Proverl and can be added to the current sequent in the Interactive Prover Background properties include axioms entered by the userl properties already proved in the same verification sessionl and automatically generated invariants 1 4 TERMS AND DEFINITIONS 9 Note that the set of background properties is lost upon termination of a system verification or theorem proving session Goal A goal is a formula that we want to prove generally valid or valid over a given programl and becomes the root of a proof tree Invariant An invariant is a formula of the form pl stating that p is true at every state of a program or system computation Invariants can be independently provedl or automatically generated by one of three methods localllinearl or polyhedral invariant generation Proven invariants are added to the set of background propertiesl and will be used by the simplifier when simplifying new formulas They can also be used as axioms in the interactive prover Subgoal A subgoal is a formula that results from the application of a verification rule to a goal or another subgoal It is a node of the proof tree n open subgoal is a leaf of the proof tree that has not been reduced to true Verification condition verification condition is a formula that results from the appli cation of a verification rule to a goal or a subgoal Verification conditions are a subset
119. nable x lt y assign y y x Transition t3 Just enable x y assign gcd x Figure 2 6 Euclid s algorithm for greatest common divisor The system illustrates that no control locations need to be associated with the transi tions when it is entered directly as a transition system This contrasts with the tran sitions generated from SPL programs An SPL program corresponding to the above The verification rules generate one verification condition for each transition relation which may be simpler to manipulate than the verification condition for the entire transition See Appendix A for the semantics of while and conditional statements See Manna and Pnueli 1995 for an example where transition relations are used to simplify verification conditions 2 6 TRANSITION SYSTEMS 31 transition system is shown in Figure 2 7 It generates the transition system shown in Figure 2 8 in a b int where a gt 0O b O local x y int where x a y out gcd int 10 loop forever do ti guard x gt y do X or t2 guard x lt y do y or guard x y do gcd Figure 2 7 SPL program for Euclid s algorithm Transition System in a b int local x y int out gcd int control pio 0 0 Initially a gt O b gt O x a y b pid 0 Transition ti Just enable pio 0 x y assign X X y Transition t2 Just enable pi0 0 A x y assign y y x Transition t3 Just enable pio O A x y
120. nabledl the Monotonicity premise will still fail to be simplified to true 9 2 3 Using the Model Checker Since program MUX SEM is a finite state program we may use the Model Checker to prove mutual exclusionI as follows 98 1 CHAPTER 9 BASIC TUTORIAL Load again the mutual exclusion property from the mux sem mux spec file The model checker does not use background propertiesl so you don t have to reset the current background properties at this point Click on the Modelcheck button This will bring up a window titled Input auxiliary assertions This window allows the user to enter additional assumptions under which model checking is to be done Since we don t need anyl we can just click the button A File Browser window titled Modelcheck log file will appear Herel you have to specify a file in which you want to have model checker results recorded The default extension of the model checker log file is mclog After the log file is specified the model checker will run We will then see in the output window Modelcheck succeeded The proof is COMPLETE The model checker log file provides more detailed informationI such as the number of states explored In generall howeverl the log file is interesting only when the model checker fails In this casel the file will include a counterexample computationI that isT a computation of the system which violates the original property 9 2 4 Using Verification Diagrams I
121. nd tick time progress measure which may not be changed by the standard transitions Only T may be used in the standard transitions Initially Tis set to 0 These variables are declared automatically when a clocked transition system is specified e Fairness conditions on transitions are irrelevantl and therefore only the condition NoFairness is allowed e The user can specify a special progress condition It restricts the amount that time is allowed to progress between the standard transitions The progress condition is written as 2 7 WHEN PARSING FAILS 33 Progress expn where ezpn is assumed to be a first order formula F clocki clock T with the auxiliary clocks clock clock and the global clock T as free variables The progress condition corresponds to a transition of the form Transition tick modvar tick enable tick gt 0 N Forall t rat 0 lt t N t lt tick gt F clocky t clock t T t assign clock clock T Celocky tick clock tick T tick which is generated automatically by the parser It is helpful to think about this transition as one that allows time to progress from T to T tickl whenever the progress condition F is satisfied for all intermediary values between T and T tick Clock variables are always of type rat 2 7 When Parsing Fails It is common for programs and specifications to fail to parse on the first try The error messages generated by the parser typicall
122. ndow 4 Enable sTeP s top level interface to use the verification diagram by selecting Current to verify under the File menu in the verification diagram editor 5 Back in sTeP s top level interface use the verification diagram as a rule by select ing Verification diagram rule from the Diagrams menu The 88 verification conditions generated from the verification diagram will now all simplify to true automatically 104 CHAPTER 9 BASIC TUTORIAL Appendix A Computational Model A 1 Fair Transition Systems An SPL program is compiled into a fair transition system A fair transition system V O T 7 is given by the following components e V system variablesl including both data variables and control variables e O initial conditionl which is a satisfiable assertion characterizing all the initial states of a computation e 7 set of transitions Each transition r 7 is a function T X22 where X is the set of all statesl and a state is a type consistent interpretation of V Each state in r s is called a r successor of s A transition T is said to be enabled on S if r s Z 0 Otherwise it is said to be disabled e J CT the set of just transitions also called weakly fair transitions e CCT the set of compassionate transitions also called strongly fair transitions Each transition T 7 is represented by a first order formula p V V T called the transi tion relationl which may refer to both unprimed and primed
123. ng STeP you don t have to type STEP DIR STeP but just STeP Execute sTePI by running STeP If your DISPLAY variable and xhost permissions are set correctlyl the sTeP main window will appear on your screen Environment variables are set with setenv variable value Unix commands which you can add to your cshrc file for convenience On UNIX systems you can usually obtain this address with the commands nslookup machine name or ping 1 machine name 4 CHAPTER 1 INTRODUCTION A number of other environment variables can be optionally set according to each user s preferences these are described in Appendix E Appendix D gives details on the installation of sTeP If you have problems installing or running sTePI please send mail to step bugs cs stanford edu 1 3 Interacting with sTeP STeP has three main interface components the Top level Prover from which verification sessions are managed and verification rules invoked the Interactive Prover used to prove the validity of first order and temporal logic formulas and the Verification Diagram Editor for the creation of Verification Diagrams Figure 1 2 shows all sTeP s interfaces with the program MUX SEM loaded
124. ng edge in an imported diagram may translate into multiple edges with the same label entering that same node in the imported diagram If multiple edges with the same label entering or leaving an import node need to be distinguished e g l because they enter different nodes in the imported diagram I the labels may be provided with a secondary label The secondary label follows the regular transition namel separated by a colon Thusl if 11 is the regular transition namel then 11 1 labels an edge for transition 11I with secondary label 1 Edges connected to the import node and dangling edges in the imported diagram only match when both the primary and the secondary label are identical White space is ignored in secondary labels Secondary labels default to O zero if left blankD but this value is not displayed in the diagram Edges can also be connected to import nodes as if the import node was a compound node i e an incoming edge in the import node is connected to all nodes of the imported diagramT and similarly for an outgoing edge I by adding the secondary label All to the label of the edge entering the import node Thusl an edge labeled with All in the importing diagram is connected to all nodes of the imported diagram without any name matching lt is not meaningful to add the secondary label All to dangling edges in an imported diagramI and this is therefore ignored If import nodes are within a compound node then edges entering or leaving the co
125. ngth ch 0 then 0 else length ch 1 Hence the operation head extracts the first element from the buffer tail returns the buffer excluding its first elementI append inserts a new element to the end of the buffer and length measures the number of elements residing in the buffer The auxiliary function pickl axiomatized in the specificationl provides us with a formal definition of the head tailland append operations We notice that taking head of an empty buffer only simplifies to some expression involving pick and its value is therefore underspecified 2 5 SPL Programs The syntax of SPL programs follows that of traditional imperative languages such as Pascal In addition to the basic constructs found in these languagesl SPL supports nondeterminism by means of the selection statement or and parallel composition by means of the cooperation statement Parallel processes can interact through shared variables such as semaphoresT as well as by synchronous and asynchronous channels Execution of parallel processes is assumed to proceed by interleaving see Appendix A for a complete account of SPL semantics 2 5 SPL PROGRAMS 25 in N int where N gt 2 local f array 1 N of int where Forall i 1 N fli 1 local r int wherer N 1 I PCi 4 N 10 loop forever do 11 noncritical 12 request r 13 request f i 14 request f i mod N 1 15 critical 16 release fli 17 release f i mod N 1
126. not be establishedI the invariant a gt B may be proved separatelyI for an incremental proof e B INV Applies the basic invariance rule to the current subgoall which has to be of the form O pl for a past formula p This rule generates the following subgoals p p Monotonicity O po Initial condition p r p foreachr e T The monotonicity subgoal is generated because this rule is based on rule G INVI below this goal always trivially simplifies to true e Applies the general invariance rule to the current subgoal The current goal has to be of the form O gI with q a past formula After clickingI a dialog window will appear that allows you to enter a strengthened version p of q The default is q After entering the auxiliary assertion pl the following subgoals are generated p q Monotonicity O po Initial condition p r p foreachr 7T e B WAIT Applies the basic nested wait for rule This rule is applicable only if the current goal is a nested wait for formulalI that isl it is of the form p qn W qu 1 W qu 2 d1 W qo where p q4 qo are past formulas Informallyl the nested wait for formula asserts that whenever p becomes truel when there is al possibly emptyl interval where qn holdsI followed by a g _1 intervall up to go becomes truel unless one of the previous q s remains true infinitely after After clicking on this button the following subgoals are generated p gt Vi o di Premi
127. nt An edge is drawn using the left mouse button press the button at the location where you want the edge to startl keep the button pressed while moving the pointer and release the button at the desired endpoint To draw an edge with cornersI release the button momentarily at the location of the turnI press againl and move the mouse in the new direction Several consecutive turns can be made in this way The label of the edge will appear in the top panel and can be edited there The label can correspond to any transition of the system being analyzed Works exactly as the tool for drawing a single lined edgeI but draws a double lined edge that has an associated Justice requirement The label of such a Just edge must be the name of a transition declared as Just or Compassion ate Works exactly as the tool for drawing a single lined edgel but draws a solid lined edge that has an associated Compassion requirement The label of a Compassionate edge must be the name of a transition declared as Compas sionate Menu Options The File Menu The File menu is used to load and save verification diagramsl as well as to make verification diagrams accessible to the Top level Prover New Resets the verification diagram editorI deleting the currently edited diagram Load Loads a verification diagram from a file Save Saves the verification diagram currently being edited to a file 66 CHAPTER 5 THE VERIFICATION DIAGRAM EDITOR Current to ve
128. nt in transitionI 30 Fast simplify top level button 71 feedback on STePI 10 file menu top level prover I 37 filebrowserI 37 filename conventionsI 124 first temporal logic abbreviation 87 Flatten ip button P85 flexible variabler 9122 Forall syntax 16128 forest example l 19 formulas P state valid 114 congruent 114 state validI 114 Free Induction ip button P89 Future temporal operatorsL 113 G BACKTO tlp button 54 G CAUS tlp button 54 G INV tlp button 53 tutoriall 96 G WAIT tlp button 53 general back to ruler 54 general causality ruleI 54 general invariance ruleI53 general wait for ruler 53 get invariants menu option 44 global timeI 32 goall 9 entryl45 133 goal sessionI 8 Group menu option l 66 grouped statementsI25 guard statement l semanticsD109 guard syntax I 27 guarded assignmentI109 head syntax 16P24D28 helpT 92 top level proverL 35 help menu top level menu T48 helpful transitionl 61 Hide ip button I 85 hierarchical verification diagramsI 67 edgesI 68 parameter passingI 68 idling transitionl 105 if then syntax 27 if then else syntax 27 import node 67 in mode r25 in syntax r27Tr31 Induction ip button I 89 inequality simplification settinglI 69 initial condition 1051106 Initially syntax P31 installation 123 Instantiate ip button P86 Interactive Prover rulesT 84 tlp buttonT49 Interactive Prover button 1 Step Propositionalr 85 Add axiomI 90 A
129. oal as its root node Nodes are labeled with subgoalsI called verification conditions in the Top level Prover and sequents in the Interactive Proverl and the application of different rules generates new subgoals or children nodes for the current node Since more than one proof rule can be applied at each nodel the process is a search The proof is finished when there are no subgoals left the number of subgoals is reduced whenever a simplification step reduces a subgoal to true which is the only formula that requires no proof In the Top level ProverI the rules applied are temporal verification rulesl logical rules or simplification steps In additionl rules that can strengthen a verification condition are availablel such as weakest precondition Finally goals in the Top level Prover can also be closed by sessions of the Interactive Prover The Background Properties Background properties include axiomsl automatically generated invariantsl and previously established properties When a top level proof is completedI the property is added to the list of background properties In the Top level ProverlI simplification is carried out relative to the properties and axioms that are active at the time except for the Fast simplify optionI discussed in Section 6 1 51 52 CHAPTER 4 VERIFICATION AND LOGICAL RULES In the Interactive Proverl these background properties have to be explicitly added by the user to the current sequent before the s
130. omposite assignment swaps the values of x and y as follows x y y x 28 CHAPTER 2 SYSTEMS AND SPECIFICATIONS Expressions The expressions allowed in SPL programs are a subset of the expressions allowed in speci fications In particular the following are not allowed in SPL programs e primed variables e Prod and Sum e temporal operators e location expressions Furthermorel when binding variables by quantifiers inside an SPL programItheir types must always be declared locallyl and the optional kind is not allowed they are always Rigid The syntax of SPL expressions is then as follows p expn bool const boolean valuel true or false int const integer value id identifier id p_expns function application exprLp_expns array reference Cp ezpn parenthesized expression p_expn p_expns a tuple of expressions int const p_expn int const th projection of tuple p_expn infix pexpn infix operator prefix p_expn unary prefix operator if p_expn then p_expn else p_expn if then else bind id type p_expn binding p ezpns p expn p_expn p_expns infix V gt lt gt binary boolean operators mod div arithmetical operators s lt gt gt lt lt gt predicate operators prefix 7 negation and minus append head tail length channel operations assign array update bind Forall Exists Exists binding operators bool const true false int const digit digit id al
131. on In this wayl a verification diagram can be applied as a verification rule to generate verification conditions that establish a given property The Verification Diagram Editor does not parse the expressions labeling the nodesl or check the existence of the transitions labeling the edges These checks are performed when the verification diagram rule is invoked If an assertion does not parsel or there is any other problem with the diagramlI a message indicating the error will appear in the message window of the Top level Prover The verification diagram can then be corrected within the Verification Diagram EditorI made current againl and the verification diagram rule applied again Drawing Tools The leftmost column contains the tools for drawing basic and compound nodesl and edges corresponding to the different justice requirements This tool sets the pointer to selection mode It enables you to select nodes and edges by clicking on them When an edge is selectedI all the nodes to which it is attached are selected too To select a single edge e g to convert it into a different type of edge you first have to move the edge away from the nodes You can do this by pressing the left mouse button while pointing at the edge and then moving it quickly while keeping the button pressed To select multiple edges and nodesI click on some location outside these nodesl and while keeping the left mouse button pressed drag the mouse until the nodes and edg
132. on settingI 70 congruent formulasT 114 constructor 19 consume statement semanticsT 109 consume syntax r27 CONT menu option r56 contradiction ruler 56 INDEX control locations 115 critical statement semanticsT 109 critical syntax r27 current goal window top level proverL 35 Cut ip button r89 datatype declaration 19 declarations 18 datatypel 19 in specification filer 18 macro 21 type 19 valuel 21 variableI 21 deconstructorl 19 Delete ip button I 85 departing edgeDl 62 diagrams menulD46 dining philosophersI 25 disabled transitionI 105 DISPLAY environment variabler 3 DistributionIl 123 div operator T14 div syntax F16 documentation 124 double edge 61 Duplicate ip button 85 edit diagram menu option 46 else tactic 74 enable syntax 31 enable fieldT 29 enabled transition 105 entailment temporal operator 114 enter axiom menu option 45 enter batch tactic menu option 46 enter interactive tactic menu option 46 enter new goal menu option I 45 enumeration typeI 19 environment variables 127 Model Checker 128 BDD settingsI 128 DISPLAYT3 polyhedral invariantsT 128 verification diagramI127 INDEX equalityl 70 simplification settingl69 equational axiomI22 equivalent formulasLl 114 Euclid s algorithmI 30 example Euclid s algorithmI30 Exists syntax 16D28 expressions 14 in SPL programs 28 syntax in specificationsI 15 fair transition systemI 9 definitionI 105 fairness requireme
133. oof tree in the reverse order that steps were undone When multiple properties are being proved at the same timel multiple proof trees are maintainedI each with its own set of open subgoals The Next search and Select search options under the Properties menu are used to move from one proof search to another 102 CHAPTER 9 BASIC TUTORIAL Finishing the Proof We now continue with the proof 5 Click on the buttonI which stands for Weakest Pre Condition This generates the subgoal O wpe l4 ma ma lin this case u V s 1 A pi 3 pio 4 where pi 3 stands for at m3 and pio 4 stands for at 4 you may check this by looking at the control correspondence information provided in the Program Text window The subgoal generated by WPC is Ac an invariance property ThusI we can try to prove it using B INV again Click on B INV to prove this subgoal all the verification conditions generated by B INV are simplified to true closing this branch of the proof tree We can do the same for the unproved verification condition for 43l which is now the only open goal left Click again on the buttonl and then on the B INV Againl all verification conditions are simplified to trueI thus closing this second branch This leaves us without any open goals in the treeI so the proof of our original top level goal is complete 9 3 2 Using Tactics x In the previous section we manually applied to the two verifi
134. oon STeP S TeP The Stanford Temporal Prover Educational Release Version 1 0 USER S MANUAL Nikolaj Bjorner Anca Browne Eddie Chang Michael Col n Arjun Kapur Zohar Manna Henny B Sipma and Tom s E Uribe November 1995 Computer Science Department Stanford University Stanford California 94305 Contents 1 Introduction 1 1 4 Reading this Manual 2 e 2 1 8 Starting STeP 4 lens 3 1 8 Interacting with STeP 4 leere 4 1 4 Terms and Definitions les 7 1 5 Feedback 2 0 a 10 1 6 Acknowledgements se 10 2 Systems and Specifications 13 2 1 Types le hh m s 13 2 2 Expressions 2 2 2 2 4 4s hh s ss 14 2 39 Specification Files ss 17 2 4 Declarations o oo oaa ee 18 2 4 1 Type Declarations a 19 2 4 2 Value and Macro Declarations oaoa a 20 2 4 3 Variable Declarations 0 0 0 s 21 2 4 4 Rewrite and Simplification Rules x o aoaaa a 22 2 4 5 Channel Operations 2 0 2 es 24 2 5 SPL Programs 2 0 0 a 24 2 6 Transition Systems aoaaa sss 29 2 6 1 Fair Transition Systems eee 29 2 6 2 Transition System Syntax ees 31 2 6 3 Clocked Transition Systems xx lens 32 2 7 When Parsing Fails 2 2 33 3 The Top Level Interface 35 3 1 Menu Options 4 2 22 2l e e les ons 37 3 2 Action Buttons 2 2 ee 48 4 Verification and Logical Rules 51 4 1 The Proof Search 2 ee 51 4 2
135. p te T gt Agop 62 LlLD A Oov D As eb AQO gBU hv gy l gt AA g C Agy PSALO esv v S 5 l gt AA g DA T y gt A r y gt Aa Tesla Tjevysad r y gt A UA T p gt y gt aA T y p gt A DIEA e Tepowsa Do Y gt A T gt A pay T 2 O pod r O gt A TesA OSyr A p T Sy gt 44 UA vv QUIA 4Q egWwv v ls A pW r PS A Olu v y gt A pv T T el O LE A pv y A p T p gt A gt A O Spr 9 A rT Spy gt 44 Tr yLOvbwJsA Tr y gt I5v gt Ip O gS v A v Tosa l o gt 88 CHAPTER 8 THE INTERACTIVE PROVER x where t is a term andI p x is a formula containing x Complementing skolemizationI instantiation applies to any existential force quantifiers under MI M Tif then else If the user supplied term t is not obviously of the same type as xI Instantiate generates additional type constraint conditions along with the instantiated formula Example For formulas N gt O IExists O N 1 h x and term t x with t eliminates the existential quantifier in the following way N gt 0 0 lt t t lt N 1 N h t N gt 0 gt Exists x 0 N 1 h x This button allows you to replace equals by equalsl that isl any term that is asserted to be equal to another term in the antecedent may be replaced with that other term throughout the sequent Upon clicking on t
136. pha alpha digit 2 6 TRANSITION SYSTEMS 29 2 6 Transition Systems Transition systems are the basic system representation in STeP SPL programs are parsed into fair transition systems an alternative to SPL is to describe transition systems di rectly Appendix A includes the basic definitions of transition systems For a more leisurely introductionl see Manna and Pnuelil 1991 2 6 1 Fair Transition Systems A transition system specification contains e Declarations of types and free variables e An optional initial conditionl which is assumed to hold at the initial state of every computation e A set of transitions Transitions are expressed in terms ofl and are usually equivalent to see below tran sition relations A transition relation describes how the system can change from one state to the next Strictly speakingl a transition relation can be expressed by a formula over the set of primed and unprimed system variables however for added conveniencel transition relations in STeP can be specified by a combination of four different fields Each field is optionall and sTeP inserts default values for absent ones The four fields are the following e The modvar field contains a set of variables that are changed when the transition is taken To indicate that the transition relation allows a variable to change value non deterministicallyl one can include it in the modvar field and not mention it elsewhere By default the only
137. poral logic In C Courcoubetisl editorD Proc 5 Intl Conference on Computer Aided Verification volume 697 of LNCSI pages 97 109 Springer VerlagI 1993 129 130 BIBLIOGRAPHY Kesten et al D1996 Y Kesten Z Mannal and A Pnueli Verifying clocked transition systems In Hybrid Systems HITLNCS Springer Verlagl1996 To appear Manna and Pnuelil 1991 Z Manna and A Pnueli The Temporal Logic of Reactive and Concurrent Systems Specification Springer Verlagl New YorkDl1991 Manna and Pnuelil1994 Z Manna and A Pnueli Temporal verification diagrams In Proc Int Symp on Theoretical Aspects of Computer Software volume 789 of LNCST pages 726 165 Springer VerlagI 1994 Manna and Pnuelil 1995 Z Manna and A Pnueli Temporal Verification of Reactive Sys tems Safety Springer Verlagl New YorkI 1995 Manna and Waldingerl 1993 Z Manna and R Waldinger The Deductive Foundations of Computer Programming Addison Wesleyl Readingl MAT 1993 McCuneL 1992 W W McCune Experiments with discrimination tree indexing and path indexing for term retrieval J Automated Reasoning 9 2 147 671 October 1992 Nelson and OppenTL 1980 G Nelson and D C Oppen Fast decision procedures based on congruence closure J ACMI27 2 356 364L April 1980 Shostakr1979 R E Shostak A practical decision procedure for arithmetic with function symbols J ACMI26 2 351 360L April 1979 Stickell1989 M E Stickel The path indexin
138. ported in part by the National Science Foundation un der grant CCR 92 23226TI by the Defense Advanced Research Projects Agency under grant NAG2 892l and by the United States Air Force Office of Scientific Research under grant F49620 93 1 0139 The sTeP project is supervised by Professor Zohar Manna 12 CHAPTER 1 INTRODUCTION Chapter 2 Systems and Specifications A system can be input to STeP as an SPL program or directly as a transition system SPL programs are parsed into transition systems The computational model associated with transition systems and SPL programs is presented in Appendix A The specification language is linear time temporal logic Its semantics is presented in Appendix B An SPL program or transition system is always loaded from a file The properties to be proven may be entered directly or loaded from a file This chapter presents the sTeP format for describing systems and their specifications Since systems and specifications share the same syntax for variable and type declarations and logical expressionsI we first describe the general syntax for types Section 2 1 and expressions Section 2 2 We then describe the overall style of specifications Section 2 3 and the syntax for declarations Section 2 4 Finally we present the syntax for describing systems either as SPL programs Section 2 5 or as transition systems Section 2 6 We use extended Backus Naur form EBNF to describe the syntax of sTeP s inp
139. psulation conventions sim ilar to those of Statecharts Harell 1987 The basic encapsulation construct is the compound node containing internal nodes We refer to the contained nodes as the descendants of the compound node Nodes that are not compound are called basic nodes Departing edges An edge departing from a compound node is interpreted as though it departed from each of its descendants Arriving edges An edge arriving at a compound node is interpreted as though it arrived at each of its descendants An assertion y labeling a compound node is interpreted as though it were a conjunct added to each of its descendants 5 5 COMPOUND NODES 63 File Edit Node Edge Figure 5 1 The Verification Diagram Editor 64 CHAPTER 5 THE VERIFICATION DIAGRAM EDITOR 5 6 Verification Diagram Editor Interface The Verification Diagram Editor allows you to load and manipulate verification diagrams The interface is shown in Figure 5 1 The two top panels are used to edit the label and the assertions on nodes and edges The diagram itself is drawn in the large panell using the drawing tools displayed in the column to its left The verification diagram does not have to be related to the current system descriptionI and you can use the Verification Diagram Editor independently of the sTeP verification session in progress By selecting the Current to Verify option under the File menul you make the current diagram the one used by the verification sessi
140. r user controlI does not have to be terminating An ordering relationl given by the ORDER keywordlI specifies a linear order over uninter preted function symbolsI as a list This order is used when converting equalities into rewrite rules during simplification roughly speakingl if t t2 or tg t is an equality encountered in contextual simplificationl t4 will be rewritten to tg if t is built from a function symbol that appears earlier in the order The syntax for simplification and rewrite rules is given by the following grammar rewrite REWRITE desc expn gt expn rewrite rule simplify SIMPLIFY desc expn gt expn simplification rule order ORDER ids The nonterminal desc can be any sequence of characters except colon l and is used as an informal description of the simplification or rewrite rule The auxiliary variables free in the expression to the left of gt should be a superset of the free variables of the right hand side expression In connection with rewrite and simplifcation rules system variables are treated as constants constructors Example Figure 2 4 shows an example of two rewrite rules The rule Peano 1l rewrites 6 0 to 6l and the rule ad hoc rewritesl f 4 2 to if y then 4 2 else 442 variable x int local y bool value f int gt int REWRITE Peano 1 x 0 gt x REWRITE ad hoc f x gt if y then x else x Figure 2 4 Rewrite rules in a specification file As wi
141. rences between MP95 and sTeP with an example Consider the program schema presented in Figure C 1I which lists the value of the control variable m in italics as it is used in MP95 In the figurel S refers to any simple 115 116 os Compound In MP95 skip u e u await e z amp e z gt u request r release r noncritical critical produce u consume u choose u if e then S if e then 5 else Sz 1 53 when e do S Sy or So while e do S repeat S until e loop forever do S 51 S2 local decl S In STeP skip u e u e await e z lt Z gt request r release r noncritical critical produce u consume u choose u if e then S if e then S else S 1 Se when e do S Sy or So while e do S repeat S until e loop forever do S 1 l Se local decl S or P j 1 M S j or j 1 M S I Ply 1 M S j I i MJ SU Table C 1 The statements of SPL APPENDIX C DIFFERENCES WITH THE BOOK Description skip single assignment multiple assignment await send receive request release noncritical critical produce consume choose 1 branch cond 2 branch cond concatenation when selection while loop repeat loop forever cooperation block param selection param selection param cooperation param cooperation C 2 CONTROL LOCATIONS IN STEP 117 In MP95 In STeP Description T true true F false fals
142. rification session Each axiom becomes a background propertyl and may be activated or deactivated from the Top level Prover 3 The properties are those formulas you want to prove true for a program or systemTor are state valid in general These become top level goals in the Top level Prover The format of the specification file is described by the following grammar specification declaration expn SPEC declaration axiom property axiom AXIOM desc expn named axiom property PROPERTY desc expn named property specification The nonterminal desc is an informal description of the corresponding axiom or property and can be any sequence of characters except colon Note that sTeP does not guarantee the consistency of the given set of axiomsI so the specification of axioms should be done with caution A specification file may contain a single formulal which by default becomes the property to be provenl or may contain multiple axioms and properties In additionI the specification file may contain declarations of macrosI valuesl and auxiliary variables An example of a file with multiple axioms and properties is shown in Figure 2 1 SPEC Greatest common divisor spec file value COMMUTATIVE gcd int int gt int AXIOM gcdi Forall m n int m n gt gcd m n gcd m n n AXIOM gcd2 Forall m int m gt O gcd m m m AXIOM gcd3 Forall m int m lt 0 gcd m m m PROPERTY auxi
143. rify Selects the currently edited verification diagram as the one used by the Top Level Prover Exit Quits the Verification Diagram Editor after confirmation by the user The Edit Menu The Edit menu is used to cut and paste parts of the diagram Cut Deletes one or more selected items from the editing window The deleted item s node or edge are put on a scratchpad and can later be recovered by Paste Copy Copies the selected item from the editing window to the scratchpad Paste Takes the item most recently put on the scratchpad either by Cut or Copy and puts it in the editing window in the same location it was before Duplicate Duplicates one or more selected items This is equivalent to doing Copy followed by Paste The Node Menu The Node menu is used to group nodes into compound nodesIchange terminal into nonter minal nodesl and vice versa Group Compound By selecting a large node and the nodes enclosed by the large node Group turns the large node into a compound nodel containing the enclosed and selected sub nodes see Figure 5 1 Subnodes of a compound node cannot be edited They have to be released with Ungroup before you can change their labels or move them The label and assertion of the compound enclosing node is displayed in the upper left corner of the node Ungroup Uncompound Converts a selected compound node into a regular nodel and releases the subnodes such that they can be edited and moved Terminal
144. rtunatelyI property yz is not inductive relative to this invariantI so the Simplifier is still unable to prove the verification conditions for 9 and mg Repeating the application of B INV with all linear invariants active for simplification you will notice that simplification is significantly slower since the background properties are being used in simplification Howeverl property gt is directly implied by the invariant and the property 4 we proved earlier Thereforel we can apply rule MON I Section 4 4 directly to the top level goall and finish the proof after one simplification step 1 4 TERMS AND DEFINITIONS 7 Another option is to use rule G INV Section 4 2 l supplementing the verification with a strengthened assertionl e g I fg fl44 m3 my4 y 1 This assertion implies mutual exclusion and is inductive the locations have been arethme tized e g the value of ls is 1 if control resides at 310 otherwise All verification conditions are reduced to true by the Simplifier thus completing the proof Yet another option is a proof by verification diagram The lower left corner of Figure 1 2 shows a state partition diagram for program MUX SEM that implies mutual exclusion the property J 3 ma is proved automatically by invoking the Verification Diagram Rule on this diagram This produces 35 different verification conditionsl all of which are reduced to true 1 4 Terms and Definitions STeP Sub systems
145. s Diagrams Logical rules Settings Load program Parches Equality Lin Arith Auto ON Load transitions Load specification Reset Searches Reset All Save search Save goal Save properties Save transitions Save last proof View transitions View program text Figure 3 2 Top Level Prover File Menu Several options in this menu activate the File Browserl a utility that allows you to move around in the directory hierarchy and select files Activating the File Browser brings up a window with several panels as shown in Fig ure 3 3 The name of the window reflects the function that called it in the figurer Load program The window under File name shows the current file selected and you can enter the filename here directly The two buttons below allow you to display all files r or only those with the default extension for the current function spl rin this casel since the default extension for programs is spl The left panel below these buttons shows the files in the selected directoryl and the right panel shows the directory hierarchy To move to another directoryI click on the directory name in the right panel To select a filel click on the filename in the left panel To load or save a filel click after selecting the file or entering its name 38 CHAPTER 3 THE TOP LEVEL INTERFACE Load program seran File name escape step dist step examples 1 Es 4f README add two any nat binom cube demo
146. s that all variables in U preserve their value at the current step In the following we represent a statement S with label and post label f in the form 6 S For a statement S f we denote by YsTV 5 loc loc Unless otherwise specifiedl all transitions are Just Basic Statements e Skip Statement l skip f Transition relation pe moves l pres Ys e Assignment J Statement u L Transition relation pe moves l 0 amp pres Ys u The assignment is always enabled if control is at the assignment statement T even if is not in the range of ul which may happen with e g l range types A proof obligation to check for this type of runtime error is generated by the Check Runtime System menu option of the Top level Prover e Await Statement l await c Transition relation pe Mmoves l c pres Ys e Asynchronous Send Statement o e L l where a is an asynchronous channel Unbounded channel Transition relation pe moves l 0 o append a e pres Ys a Bounded channel For a channel o with bound KI the transition relation is pe moves l 0 length o lt k a append o e pres Ys a To ensure that a process cannot be excluded from sending to a bounded channel if it is infinitely often non full we associate the Compassionate justice requirement with this transition 108 APPENDIX A COMPUTATIONAL MODEL e A
147. s will generate a single veri fication condition as the subgoall stating that the conjunction of all the background invariants implies the original goal 6 Click on the Simplify button the verification condition will be simplified to trueland the proof is complete If automatic simplification is ONT this simplification will be done automatically after MON I is invoked 9 3 MUX PET Invariance Strengthening In this section we illustrate the construction of the proof tree with the program MUX PETIT shown in Figure 9 9 The program and specification used in this section can be found in the files mux pet1 mux pet1 spl and mux pet1i mux spec respectively 9 3 1 Using WPC Mutual exclusion for MUX PET is not an inductive property Instead of finding a strength ened assertion and using G INVI as we did for program MUX SEMI we use STeP to do the strengthening for us 9 3 MUX PET1 INVARIANCE STRENGTHENING 101 local y y2 boolean where y yo F E 1 2 lo while T do mo while T do li noncritical m noncritical la yis T 1 ma yas T 2 f3 await Ay or s 2 U ma await ay or s 1 4 critical ma critical fs i F Ms Yoi F Figure 9 9 MUX PET1 Peterson s algorithm for mutual exclusion 1 Load the program mux peti spl and the mutual exclusion property mux spec from the mux pet1 directory 2 Turn automatic simplification on by selecting the Automatic Simplification ON OFF opt
148. se N1 qi qi Monotonicity Lfor each 7 0 n iT 1V z qj foreach i l n The monotonicity conditions are generated because the implementation of B WAIT is based on that of G WAITT below They always trivially simplify to true e G WAIT This button invokes the general nested wait for rule This rule is applicable only if the current goal is a nested wait for formulal that isl it is of the form p qn W qu 1 W qu 2 d1 W qo where p q4 qo are past formulas A dialog window will appear which allows you to enter the auxiliary assertions 4 o Their defaults are g qol respectively After entering these assertions the following subgoals are generated p gt Vizo Yi Premise N1 Pi S qi Monotonicity il for each i 0 n pT V lt i p i foreach i 2 1 n CHAPTER 4 VERIFICATION AND LOGICAL RULES e B CAUS The basic causality rule is a specialization of the basic invariance rule It is applicable to goals of the form p gt Ou where p and q are past formulas It usually generates simpler verification conditions than its counterpart B INVT which is also applicable to goals of this formTby taking into account the special form of the goal This rule generates the following subgoals papyv g Monotonicity O p o V q o Initial condition T pV a e G CAUS The general causality rule specializes the general invariance rule It is applicable to goals of the form p gt q where p and q are past formul
149. sequent Hidden formulas do not par ticipate in simplification stepsIl and cannot be acted upon by inference rules Hidden formulas howeverl can be recovered with the rulel below Hiding formulas can make the sequent more readable and may speed up simplification After clicking this button all formulas are highlighted and you can select the formula to hide To hide several formulas you must use multiple times Recovers a formula hidden with Hide The next subgoal in the subgoal queue becomes the current subgoal Duplicates a formula in the sequent This is useful if you need to instantiate a quantified variable more than oncel using different values Note that duplicated formulas can be hidden with Hide U aboveruntil they are needed This button implements the weakening rule It allows you to delete formulas that are not needed to establish the goal Deletion of unnecessary or redundant formulas makes the current goal easier to read and speeds up the simplification procedures Creates a new sequent in which all conjunctions in the antecedent and all dis junctions in the consequent are split into separate formulas Example For formulas a b c d e f gl Flatten has the following effect a b b c d A e f g a Ab bM c gt d ef g Invokes the Simplifier on the current goal The strength of the Simplifier is controlled via the Simplification Flags option under the Settings menu 1 Step Propositional Appli
150. shows an overview of step The main inputs are a reactive system which can be a description of hardware or software and a property to be proven about the systemT represented by a temporal logic formula Verification can be performed by the model checker or by deductive means Model checking is automatic deductive verification is to a large extent automatic for simple safety properties while progress properties require more user guidancel usually given in the form of a verification diagram In all cases the automatic prover is responsible for generating and proving the required verification conditions An interactive Gentzen style theorem prover is used to establish those verification conditions 2 CHAPTER 1 INTRODUCTION Temporal Logic Reactive System Hardware Formula SPL Program Description S Te P Fair Transition Verification User ee SOT Diagrams Automatic Prover r E Model x Checker Verification ottom up Invariant Rules Generator p Interactive fy First order Prover Prover Strengthenin NE 7 ieu e Simplification Gentzen style N 9 Decision procedures Temporal Propagation Non clausal resolution e First order LLL Psyaid P valid Counter example Debugging Guidance Figure 1 1 An overview of the STeP system that are not proved automatically STeP The Educational Version The current release of sTeP is the educational versionl and is a companion to the textbook Manna and Pnueli
151. soe A new method for proving certain Presburger formulas In Proc of the A International Joint Conference on Artificial Intelligence pages 15 21T Tbilisi Georgia USSRI September 1975 Boyer and MooreL1988 R S Boyer and J S Moore Integrating decision procedures into heuristic theorem provers A case study with linear arithmetic Machine Intelligencer 11 83 12411988 Bryantl1986 R E Bryant Graph based algorithms for Boolean function manipulation IEEE Transactions on Computers35 8 677 691T August 1986 Bryantl 1992 R E Bryant Symbolic boolean manipulation with ordered binary decision diagrams ACM Computing SurveysU24 3 293 318I September 1992 Dershowitz and JouannaudT 1990 N Dershowitz and J P Jouannaud Rewrite systems In J van Leeuwenl editorl Handbook of Theoretical Computer Sciencel chapter 6I pages 244 320 Elsevier Science PublishersI 1990 Gallier1987 J H Gallier Logic for Computer Science Foundations for Automatic The orem Proving Wiley New YorkI 1987 Harell1987 D Harel Statecharts A visual formalism for complex systems Sci Comp Prog 18 231 214AT1987T Hojati et aL D1993 R Hojati V Singhall and R K Brayton Edge Street Edge Rabin automata environment for formal verification using language containment SRC reportT University of Californial BerkeleyI1993 Kesten et al 1993 Y KestenlZ MannalH McGuirel and A Pnueli A decision algorithm for full propositional tem
152. subprocess l and a set of location variables one for each label in the program A control variable ranges over a subset of the integersl where each value corresponds to a location in a process see Section C 2 A location variable is a boolean variable with the same name as a program label Its value is true iff control currently resides at the location of the labelI i e L iff one of the control variables equals the value of the corresponding location Initial Condition The initial condition for program PlI with n top level processeslI is defined as Q mo9 0AmQ 0 m 0 q where is the conjunction of all the assertions that appear in the where clause of the declaration of P For a parameterized programI with top level processes PH F1 lt i NT the initial condition is given by O Vi 1 N vo i 2 0 o Transitions A transition relation is defined for each of the statements in the language To make the definitions more succinct we define the abbreviation moves l l xs val x5 val 0 A loc loe A 3 SPL SEMANTICS 107 where 7s refers to the control variable of the innermost subprocess in which the statement S appearsl and val refers to the integer value associated with the location of Vand loc refers to the location variable associated with the location of Since every transition usually modifies only a few variables we define pres U N w u ucU where U C V It state
153. succinct specificationsl and is called arithmetization The boolean value true is also interpreted as 1l and false as 0 see Chapter 2 After the strengthened assertion is enteredI all verification conditions are simplified to true and the proof is complete Note The strengthened property only implies mutual exclusion based on the invariant v1 O y 2 0 that we proved before If you do not prove this property before attempting the proof of mutual exclusionl the Monotonicity verification condition will fail to simplify to true The basic but useful property y gt 0 can also be generated automatically using STeP s invariant generation tools To see how this can be usedl reset the searches with the Reset searches option under the File menul and repeat the two steps using above The Monotonicity property will not be simplified to true Now we can do the following 3 Select the Get local invariants option from the Properties menu Five invariants appear in the output window The first invariantI in Figure 9 7I is I the property we need Obtaining local invariants Figure 9 7 Local invariants for MUX SEM 4 Select the Simplify button Now the Monotonicity condition should simplify to truer and the proof is complete Note also that these simplification steps succeed only if the linear arithmetic decision procedures are enabled This is done with the Simplification Flags option under the Settings menu If they are not e
154. synchronous Receive Statement l a u f Transition relation pe move l L length a gt 0 A u head a a tail a pres Ys u a The asynchronous receive statement is enabled only if the channel is currently nonempty To ensure that a process must receive something if the channel is infinitely often non emptyl the Compassionate fairness requirement is associated with this transition Synchronous Send Receive With each pair of matching send and receive statements fra ejf m um where two parallel statements are considered matching if they form an a lt ela gt u pair for some e and u for the same synchronous channel a Transition relation PUn Bend val l Tieng val f Treceive val m mL val m loc loc loc m loc m u e pres Y send receive ThusF transition Tym is enabled if control is at and m simultaneously When executedI the transition causes joint progress in the two processes containing the send and receive statement The fairness requirement associated with the generated transitions is Compassionatel to ensure that a process cannot wait to transmit or receive a message indefinitely if infinitely many messages are sent on the channel it is waiting on Request With the statement request r we associate a transition r l with the transition relation pe move G0 r 0 r 2r 1 pres s r Thuslthis sta
155. tac2 taci tac3 el at original goal original goal Figure 6 2 try tac1 tac2 tac3 then form tactics then has the same effect as skip the original subgoal is reduced to itself For non empty lists we define inductively then breadth first tac taco tac applies tactic tac first If it succeeds it applies the tactic then breadth first taco lac to each of the generated subgoals If it fails it applies the tactic then breadth first tacg tac to the original subgoal Figure 6 3 illustrates the levels obtained from successful completion of then breadth first tac tac2 tac3 So for instancel the nodes above the original goal in the bottom represent the result of applying tact tac3 tac2 taci original goal Figure 6 3 then breadth first tac1 tac tac3 74 CHAPTER 6 AUTOMATIC THEOREM PROVING then depth first tac tacz tac applies the tactic tac first If it succeedsI it applies then depth first tacz tac to the first subgoal generated If it failsT it applies then depth first taco lac to the original goal If any left most subgoal is closed by a tactic tac where i lt nI then tacj41 tac are ignored Figure 6 4 illustrates the effect of successful completion of then depth first tac tac2 tac3 tac3 tac taci original goal Figure 6 4 then depth first tac1 tac2 tac3 If no form is given the default is breadth first sequence tactics Applies the tactics i
156. tatementsl and may only be combined into composite statements by selection and concatenation A grouped statement may contain at most one send or receive statement on the same channel Example To request resources r and s simultaneously one can enter lt lt request r request s gt gt which can also be encoded as guard r gt 0 8 gt O do r s r 1 s 1 Program statements The following grammar provides the syntax of SPL programs program composite_stmt stmt comp_group_stmt decl composite_stmt label composite_stmt composite simt composite stmt composite stmt composite stmt or composite simt label stmt basic group stmt request variable release variable noncritical critical choose variable produce variable consume variable guard p_ezpn do assignment if p_expn then composite simt if p_expn then composite simt else composite stmt when p_expn do composite simt while p_expn do composite stmt repeat composite stmt until p_expn loop forever do composite stmt id L program lt lt comp group stmt gt gt or binding composite stmt binding composite stmt basic group stmt if p_expn then comp group stmt concatenation cooperation statement selection statement request statement release statement noncritical statement critical statement choose produce statement consume statement guarded assignment l way conditional 2 way conditional
157. tax of programs as well as differences in specification style C 1 SPL Programs STeP closely follows the SPL syntax described in MP95 Howeverl some constructs had to be translated into an ASCII equivalent To ease transcribing programs from the book Table C 1 presents each statement as it appears in MP95 and its representation in STeP In the tableI u refers to an arbitrary variabler u refers to a list of variables i e Du4 wu e refers to an arbitrary expressionl e refers to a list of expressionsIl z refers to an arbitrary channell and 5 refers to an arbitrary statement Table C 2 presents the various types of expressions as they appear in MP95 and their representation in STeP Againl e is an arbitrary expressionI u is an arbitrary variablel and refers to a list of expressions The various types allowed in STeP are presented in Table C 3 In this tablel e is an arbitrary expressionlI u is an arbitrary variablel b is an arbitrary base typel t is an arbitrary base or simple typel and T is an arbitrary type i e basel simple or complex A range in STeP is written 4 5 C 2 Control Locations in STeP As in MP95I sTeP uses control variables to indicate where the current program control resides However MP95 uses a single control variable whose value is the set of locations where control currently resides sTePl on the other handI uses a set of control counters where each control counter has its own subscript We illustrate the diffe
158. tement is enabled when control is at and r is positive When executed it decrements r by 1 To model fair scheduling of semaphores in the form of for instance single or multi level feedback queues I the transition associated with request is Compassionate Release With the statement release r T we associate a transition r with the transition relation pe move l l r r 41 pres Ys ir This statement increments r by 1 A 3 SPL SEMANTICS 109 e Noncritical With the statement noncritical lT we associate a transition Tel with transition relation pe move l l A pres Ys ThusI the only observable action of this statement is to terminate The situation that execution of the noncritical section does not terminate is modeled by a computation that does not take transition re This is allowed by excluding T from the justice set e Critical With the statement critical we associate a transition r Iwith transition relation pe move U pres Ys The only observable action of the critical statement is to terminate e Produce With the statement produce z Twe associate a transition Tel with transition relation pe move l l a Z0 pres Ys z The observable action of the produce statement is to assign a nonzero value to variable x Note that this transition is nondeterministic that isl a state s may have more than one T successors In fact it may have infinitely many successorsD one for ea
159. th axiomatizationsI the user is responsible for the consistency of the set of rewrite and simplification rules The reader interested in learning more about rewrite rules and their applications should consultl for examplel Dershowitz and JouannaudT 1990 An example of simplification rules appears in Section 2 4 1 The Simplifier uses the recursive path ordering on terms to orient equalities see Dershowitz and Jouan naud 1990 24 CHAPTER 2 SYSTEMS AND SPECIFICATIONS 2 4 5 Channel Operations x Asynchronous channels are modeled as queuesl i e l new elements are appended to the tail of the queuel and elements are extracted from the head The basic operations on channelsl headl taill appendl and length are best described in the specification file that users should provide when they want to establish properties of channels That isl 8STeP does not include the partial axiomatization given below insteadI specifications should provide separate axiomatizations for each type of asynchronous channel used Sample channel specification SPEC type t type chan channel 1 of t local ch chan value pick chan int gt t variable x t AXIOM Forall i int pick append ch x i if i 1 length ch then x else pick ch i AXIOM Forall i int pick tail ch i pick ch i 1 SIMPLIFY head ch pick ch 1 SIMPLIFY length append ch x gt 1 length ch SIMPLIFY length tail ch gt if le
160. the bottom of the top level proverl is STeP s mes sage help line In this windowI sTeP indicates what action is being donel which dialog window is waiting for inputl or if an action has terminated successfully or not It will also display a brief description of any feature that is being selected For examplel if is selected this window will display Backtrack to parent At the right side of the top level window is the action regionl a double column of buttons that invoke verification rules and decision procedures and apply them to the the current goal Besides the temporal verification rules buttons in this column invoke the automatic Simplifier or start up the Interactive Prover The and buttons cycle through the open goals in the current search 35 36 CHAPTER 3 THE TOP LEVEL INTERFACE x STeP File Properties Tactics Diagrams Logicalrules Settings f a This is STeP Version 1 0 educational release Simplify j Help messages Figure 3 1 Top level Prover window 3 1 MENU OPTIONS 37 T In the lower right hand corner of the window is a button with the sTeP logo This button functions as the interrupt buttonl and can be used to halt most of the automatic operations performed by sTeP 3 1 Menu Options The File Menu The File pull down menu Figure 3 2 is used to load system description and specification filesl and to save finished and unfinished proofs git Properties Tactic
161. the following steps 1 Load the program MUX SEM by loading the file mux sem spl This will bring up the Program Text window shown in Figure 9 2 Apart from the programlit contains a list of how the program s control locations correspond to STeP s internal variables Control locations are explained in detail in Appendix C 2 When an SPL program is loadedl a fair transition system is automatically generatedI which you can view by selecting View Transitions from the File menu 2 Load the specification file nux sem ygeO spec The property appears in the current goal windowl as shown in Figure 9 3 3 Enable automatic simplification by selecting the Automatic Simplification ON OFF option under the Settings menu 4 Enable the use of decision procedures for linear arithmeticT by selecting the Simplifi cation Flags option under the Settings menu A window with the title Main Flags will appearl as shown in Figure 6 1 Click on the second switch to include decision procedures for linear arithmetic in the standard simplification and press the button Throughout this tutorial we will assume that the decision procedures for equality are also enabled this is the default for sTeP 5 Click on the button in the action region One by one the verification con ditions for all transitions are displayed in the current goal windowl and the result of their simplification is displayed in the output window see Figure 9 4 Since all verificat
162. thus generating the first level of subgoals of the proof tree These subgoals are numbered accordingly 1 1L1 2L1 3T etc If all subgoals are established automatically by the Simplifier i e the Simplifier can reduce them to true l all branches are closed and the proof is finished If the Simplifier is not able to prove one of the subgoalsIl we have one of the following possibilities 1 The subgoal is not valid for the given program In this caseIl the proof cannot succeed 2 The property is valid for the programI but not generally valid In this case you will have to a strengthen the original formulal or b first prove some auxiliary properties of the programlI relative to which the problematic verification condition becomes valid In the latter case you may start a new proof tree for the auxiliary property and return to the original property after the auxiliary proof is finished This approach reflects the incremental proof style advocated in Manna and Pnuelil 1995 Another way to establish auxiliary properties is through the automatic generation of invariants STeP includes three such methodsI which generate properties that often help in proving verification conditions Chapter 7 3 The property is generally valid but the simplifier is unable to reduce it to true In this casel the Interactive Prover Chapter 8 can be used to establish the given property with user guidance If this is successfull the given subgoal is closed Partial
163. tion Reset Searches Selecting Reset Searches deletes all pending proof trees and goalsl as well as all background properties Howeverl the current program or transition system is retained Thusl it resets a verification session Reset All Terminates a system verification or theorem proving session it removes all cur rent proof treesl background propertiesl and the current system descriptionl if any Save search Saves the current proof tree to a filelin ASCII formatITor off line inspection Note that the current proof tree is necessarily unfinishedli e It still has open subgoals Once all subgoals are closed the proof tree is removed from the listl and the next proof treel if anyl becomes the current one To save the last complete proofl use Save last proofl described below Note the current version of STeP does not support reloading this file to resume the proof We plan to add this capability in future releases Save goal Saves the current goal to a file The file will contain declarations for all free variables Save properties Saves all background properties to a file The background properties include all properties proven and all invariants generated during the current program verification sessionl as well as all axioms asserted by the user Save transitions Saves the current transition system to a file this is useful to see how SPL programs are converted to transition systems Save last proof Saves the finished proof of the most
164. tion of the on line help pagesl using Mosaic or your favorite html WWW browser The Top level Prover help pages are accessible from the Verification Diagram Editor help pages and vice versal so a single help session should generally suffice The executable used for on line help can be changed by setting the STEP BROWSER environment variable 5 7 Hierarchical Verification Diagrams x In order to allow decomposition of verification diagrams into smaller more manageable parts STeP supports hierarchical verification diagrams With hierarchical diagramslI several nodes in a large diagram can be represented by a single node making large diagrams more readable and easier to edit Import Nodes A hierarchical verification diagram has one or more import nodes An import node imports a verification diagram from a file The imported diagram may itself have import nodes that import other files The edges going out from the import node are matched up with outgoing edges from the imported diagraml and similarly for incoming edges An import node is created by giving it the label import and giving it as assertion the filename with full or relative path name within angle brackets l for example mux pet2 mux hi diagram l of the file that contains the diagram to be imported The assertion field may also contain parameters see next paragraph enclosed within 76 Any text in the assertion field of an import node that is not enclosed by angle brac
165. to the IP address of your screen If these variables are not setI you will not be able to run sTeP To set a UNIX environment variablel enter setenv variable name new value from the UNIX prompt You can also add these commands to your cshrc filel to make them the defaults when you log in General variables e STEP DIR Local sTeP installation directory Default 1ocal step e STEP BROWSER The location of the WWW http browser executable used for on line help Default usr local bin mosaic e STEP AUTO SIMPLIFY If this flag is set to anything other than OFFT this will cause STeP to start with the automatic simplification flag see Section 4 1 ON e STEP SHOW LOADED Set this to OFFI if you do not want loaded programs and tran sition systems to be automatically displayed Verification Diagram settings The following values can be increased when very large diagrams need to be drawn e STEP DIAGRAM WIDTH Maximum widthl in pixelsl of the verification diagram canvas Default 1200 e STEP DIAGRAM HEIGHT Maximum height in pixelsl of the verification diagram canvas Default 1200 127 128 APPENDIX E STEP ENVIRONMENT VARIABLES BDD package settings These variables control the amount of memory used by the BDD s e STEP BDD NODES Maximum number of BDD nodes that are kept around by the BDD package After this maximum is reachedIl the BDD packages has to be reset for BDD based operations to succeed Defau
166. ton l 88 REWRITE syntax 23 rewrite ruler 22123 rigid variabler 22 runtime errorsI 45 save goal menu option l40 save properties menu option 40 save search menu option l 40 save transitions menu option 40 saving goall 40 proofI 40193 propertiesDl 40 transitionsI 40 select boxes menu option 84 select goal menu option P41 select search menu option 44 send statement syntax l27 sequence tactic 74 settings menu top level prover l 47 side verification conditionl 60 simplification automaticI52 use of background propertiesI 51 simplification flags menu option l47 simplification ruleI 221 23 simplification settings INDEX associative functionsI 70 BDD simplification 70 commutative functionsI 70 conditional rewrite rulesL 70 equalityl 69 inequalityr 69 linear arithmeticI 70 Simplify ip button r85 SIMPLIFY syntax 23 Simplify top level button l71 Since operator 14 Since syntax r16 skip statement syntaxI27 skip statement l semanticsP 107 Skolemize ip button 86 solid edgel 61 specification 9I 17 declarations 19 loading 40191 SPL basic statementsT 107 SPL composite statements 109 SPL expressionsI 28 SPL programsI 9 loadingIl 38D1 91 syntax 24 spread tactic 74 starting STePT3 state accessible 114 state valid formulasT 114 Statechartsr62 status lineI top level proverI 35 STeP STeP sessionI 8 distribution 123 documentationI 124 mailing list 10 STEP_AUTO _SIMPLIFYT127 STEP
167. tzen sequent calculus resembles the one used in temporal tableau like decision procedures for propositional linear time temporal logic The prover therefore supports an automatic decision procedure for propositional temporal logic Disclaimer This implementation of PTL expansion only applies well to small formu lasso its use should be limited to textbook examples More efficient implementation are availablel e g l Kesten et al D1993 Chapter 9 Basic Tutorial This chapter presents detailed verification sessions that can be followed as a tutorial for STeP and used as templates for other verifications All input files mentioned in this chapter are available in the examples directory in the sTeP distribution We assume that you have successfully started sTeP see Section 1 2 9 1 Preliminaries The input to sTeP will be an SPL program P and a temporal logic formula y that expresses a property of P to be verified A verification session deals with a single program and one or more properties to be verified for that program Thusl loading a new program reinitializes the systeml and starts a new verification session Loading a program To load an SPL programTselect the File menu option in the upper left corner see Figure 3 2 and select Load program This will start up the File Browser with a Load program windowT as shown in Figure 3 3 By clicking on the buttonl you can choose to see only the files with extension splIthe standard extension
168. ut Ter minal symbols are written in typefontlnon terminals in italics Alternatives are separated by l optional parts enclosed in l zero or more occurrences of a construct are indicated by enclosing in Tand is used for one or more occurrences Comments can be included in a file using the 4 character indicating a comment until the end of the line Il or using and for multi line comments 2 1 Types The basic types in STeP are booleansl integersl rationals range typesl underspecified types and datatypes New compound types can be created using type constructors The type con structors in sTePlI listed belowI define types for arraysl channelsI and tuples of types in the usual way A type can be enclosed in parenthesis to distinguish for instance a tuple of three elementsl e g l int rat booll from a nested tuple of pairsl int rat bool type N id type identifier basety base type array range range of type array type channel of type synchronous channel channel 1 of type unbounded asynchronous channel 13 14 CHAPTER 2 SYSTEMS AND SPECIFICATIONS channel 1 int const of type bounded asynchronous channel range range type type type tuple type type parenthesized type range empn expn range basety bool boolean type int integer type rat rational type The type constructor x has higher precedence than all other type constructors ThusI the type channel
169. value The following highlights the similarities and differences between STeP s interpretation of control counters and the MP95 use of the control variable 7 1 step The ordering of the labels does not affect the value of the control counters For examplelif we renamed label 12 to be 125Il the control counters would still have the same values In generall the program counter pi j associated with the process P starts at 0 and increases by 1 as control proceeds sequentially through the process MP95 The ordering of the labels does affect the value of the control variable 7 Solin the above examplel if we rename fz to 55 then m 5 would change to r 425 STeP A cooperation statement among N processes employs N control counters If the cooperation is a top level cooperation statement i e no entry and exit transitions then the program has only N control counters This is not the case in Figure C 2P where the cooperation statement has entry and exit transitions In this casel we have two control countersl pii and pi2lIin addition to piOl whose value within the cooperation statement is constant MP95 There is always only one control variablel called 7 C 2 CONTROL LOCATIONS IN STEP ka ks ke k7 Sio S 11 5 k x ja u js T Us z 65 Sis w 46 Figure C 1 Program schema illustrating MP95 s use of the control variable 7 119 120 APPENDIX C DIFFERENCES WITH T
170. y indicate the line number and character range where the error was detectedI separated by a Tand provide some extra information about the offending part Unfortunatelyl the error messages are not always as illuminating as we would like Here are some hints for when things don t work as expected e The different kinds of arrows can be confusing lt gt is the temporal operator once lt gt is double implication lt is less than or equals gt is normal implicationI but gt is also used in function types gt js the temporal entails relation p gt q stands for p gt q Tbut gt js also used for channel operations in SPL lt gt is a built in macrol expanded to p lt gt q gt is used to specify rewrite rules e A period is expected after quantifiers e Variables declared in the specification file and quantified variables are rigid by default To specify a flexible variable in quantificationI just write Forall x int Flexible ezrpn Even after parsing a file watch out for the following CHAPTER 2 SYSTEMS AND SPECIFICATIONS e Arithmetization 1 lt i lt Nis parsed as 1 lt i lt NI hence as the truth value of 1 lt i is less than or equal to N Tand not as 1 lt i i lt N e Rigid vs flexible variables see above e Scope of quantifiers and declarations Binding operators have maximal scope Hence Forall x int

STeP The Stanford Temporal Prover Educational Release USER`S

Contents

Download Pdf Manuals

Related Search

Related Contents