A User's Guide to Zot
Contents
1. 2 is the output of the SMT solver whose syntax and structure vary with respect to the used solver 3 is the resulting trace of the system if it exists Finally output dict txt is the set of all the sub formulae which the tool handles 5 ARCHITECTURE 26 5 Architecture Zot s architecture is based on a PLTL to SAT core which interacts with the outside world through a TRIO based interface and different plug ins The core itself is structured as a plug in so that different encodings can be defined and used More recently May 2009 we added two plugins to Zot natively sup porting metric operators like lasts withinf These native metric plugins are called meezot mono infinite and mbezot Their usage is exactly the same as eezot and bezot 17 5 1 PLTL to SAT encodings As said before Zot s core is based on encoding PLTL into SAT and CLTLB IDL or CLTLB LIA into SMT At present two main propositional encodings are available in the standard distribution eezot which is a standard eventuality based encoding on a mono infinite time domain N see e g 8 and the bi infinite one bezot 18 on Z The arithmetic encoding see 6 is imple mented in ae2zot The two propositional encodings are packaged as asdf systems in the following files eezot lisp eezot asd bezot lisp bezot asd The arithmetic encoding is packaged in ae2zot lisp ae2zot asd The file kripke lisp contains the basic data structure and the2. This approach encourages experimentation as plug ins are ex pected to be quite simple compact usually around 500 lines of code easily modifiable and extendible At the moment a variant of the eventuality en coding presented in 8 is supported approximated dense time MTL 11 and a bi infinite encoding 18 19 Zot offers three basic usage modalities 1 Bounded satisfiability checking BSC given as input a specification formula the tool returns a possibly empty history i e an execution trace of the specified system which satisfies the specification An empty history means that it is impossible to satisfy the specification 2 Bounded model checking BMC given as input an operational model of the system the tool returns a possibly empty history i e an execution trace of the specified system which satisfies it 3 History checking and completion HCC The input file can also con tain a partial or complete history H In this case if H complies with the specification then a completed version of H is returned as output otherwise the output is empty The provided output histories have temporal length lt k the bound given by the user but may represent infinite behaviors thanks to the loop selector variables marking the start of the periodic sections of the history The BSC BMC modalities can be used to check if a property prop of the given specification spec holds over every periodic behavior with period
3. equal p p1 state p1 N turn p next state p C state p C next state p N else amp amp state p x 4 USAGE 17 next state p x or case x turn d schedule amp amp state 1 N state 2 T state 3 N next turn 2 amp amp state 1 T state 1 N state 3 N next turn 1 amp amp state 1 N state 1 N state 3 T next turn 3 random choice policy amp amp state 1 T state 2 T next Cturn 1 turn 2 amp amp state 1 T state 3 T next Cturn 1 turn 3 amp amp state 2 T state 3 T next Cturn 2 turn 3 else amp amp turn x next turn x As the reader may see the transitions are defined as a list of constraints which must hold on every instant of the time domain We then write a simple property we wish to check on the system defvar spec alw 88 gt turn 1 somf turn 2 turn 3 gt turn 2 somf turn 1 turn 3 gt turn 3 somf turn 1 turn 2 The main procedure is called zot and has two arguments the time bound and the formula to be satisfied plus some optional switches e g transitions declarations loop free To check if spec 0 holds for a time bound of 30 we perform eezot zot 30 time bound amp amp yesterday init initializ
4. gt P L I yesterday P on E x loop for i from 2 to delta collect i amp amp past P on x withinP_ee P off x amp amp P on P off To obtain a history compatible with the spec we perform bezot zot 10 amp amp init the lamp 4 USAGE 24 This is an example history generated by Zot where LOOP and POOL are the loop selector variables POOL towards the past LOOP towards the future time 0 Saaie tine L 2 2 23 LOOP ON SSE Sa time 2 55 ON L seqccs time 3 ON L 222 time 4 OFF L SS time 5 OFF ZAFER time 6 OFF gt time 7 OFF Tyan bime 8 3 OFF SS time 9 PDOL x OFF time 10 4 USAGE 25 4 6 Temporary data Zot uses files to save temporary data during the verification activity They differ depending on the used plug in The propositional plug in like eezot creates 1 output cnf txt 2 output sat txt 3 output hist txt 1 contains the resulting boolean formula of the system in the stan dard DIMACS CNF format 2 is the output of the SAT solver 3 is the resulting trace of the system e g a TRIO history if it exists SM T based ae2zot creates different files 1 output smt txt 2 output 1 txt 3 output hist txt 4 output dict txt 1 contains the resulting SMT LIB description of the system the stan dard is SMT LIB v 1
5. by using the two dual constructs and case and or case 20 To give the reader an idea of their semantics here is an automatic trans lation made by Zot on two simple examples and case x 1 2 y 3 4 P P x P Q x P R y P Ri y else P R2 x expands to A X 1 2 A Y 3 4 amp amp gt P R Y P R1 Y gt P P X P Q X gt amp amp P R Y P P X P R2 X and or case x 1 2 y 3 4 P P x P Q x P R y P Ri y else P R2 x expands to E X gt 1 2 E Y 3 4 11 amp amp P R Y P R1 Y amp amp P P X P Q X amp amp P R Y P P X P R2 X 3 LANGUAGES 13 3 7 MTL There is an experimental plug in called ap zot for using a variant of dense time MTL through approximation see 11 and 10 Observe that MTL is a pure propositional temporal logic so relations functions and variables over possible infinite domains are not supported Here is a list of the time operator defined in ap zot until b until b v until b since b since b v since b release b release b release b v trigger b trigger b trigger b v until b inf until b v inf until b inf since b inf since b v inf since b inf release b inf release b inf release b v inf trigger b inf trigger b inf trigger b v inf diamond diamond inf diamond p diamond inf p box box inf box p box
6. default 9 MiraXT 15 PicoSAT 7 and zChaff 16 Zot as sumes that executable files called minisat MiraXTSimp optional picosat optional zchaff optional are system wide installed A pre packaged all inclusive version for Windows WinZot based on Cygwin compiled binaries and SBCL is available from the author All Zot s components are available as open source software GPL v2 2 1 Hello world Here the user can find short examples of the functionality of Zot which can be used to test the installation and to understand the basic notion support ing the tool knowledge about verification and bounded model checking are hardly recommended Zot is tailored to solve the Bounded Model Checking problem BMC and Bounded Satisfiability Checking BSC which are both reduced to a satisfiability problem The aim of the satisfiability process is to represent SBCL and CMUCL are usually the fastest implementations for running Zot 2 INSTALLATION 3 infinite model of CLTLB LTL formulae by means of a finite representation of length k i e amp instant of time A model is an infinite word of propositional atoms and counters values when CLTLB is considered In the following sections the term model and behavior of a system in particular when the satisfiability checking is performed have the same meaning and they can be equivalently used The first example shows how to solve the BSC for a LTL formula by means of a finit
7. definition 4 of the generics defclass kripke time bound i e 0 k the k accessor kripke k number of used prop variables numvar accessor kripke numvar formula gt integer data structure hash table the list accessor kripke list integer gt formula data structure hash table the back accessor kripke back kripke does not actually contain a Kripke structure names of data structures and generics come from previous forsaken incarnations of the tool set 5 ARCHITECTURE 27 list of propositional letters sf prop accessor kripke prop list of used boolean subformulae sf bool accessor kripke bool list of used future tense subf sf futr accessor kripke futr list of used past tense subf sf past accessor kripke past n of props used in the encoding max prop accessor kripke maximum resulting SAT formula the formula accessor kripke formula There is also an old variant of eezot called ezot which supports virtual unrollings as presented in 8 usually called 6 so its data structure is extended through inheritance The user may change the default behavior ie 6 0 by setting ezot FIXED DELTA to nil which tells eezot to actually compute 6 or s he may change to set it to a fixed meaningful value The call generic translates a formula proposition and a time instant into an integer the SAT solver proposition self must be an instance of kripke o
8. is evaluated differently depending on if it is a Lisp variable or a 0 ary function e if var is a Lisp variable its value is written as a usual Lisp variable e if var is a logic variable its value is written as V var Predefined operation and relations a small number of binary opera tion relations between integers are predefined in the SMT library namely only available in the plugin ae2zot 3 LANGUAGES 8 lt lt gt gt with their usual meanings is the remainder oper ator As CLTLB operations which map to SMT LIB operations they are written lop x_1 x 2 Observe that some operations are not defined in all constraint systems in order to use and the logic QF_UFLIA has to be declared Arithmetic temporal terms if a is an arithmetic temporal term Xa and Ya are written respectively as next V alpha and yesterday V alpha Temporal operators the following temporal operators are supported until since release trigger next yesterday zeta The last one is the dual of yesterday and is used only in the mono infinite semantics For the semantics of these operators see e g 6 TRIO operator are also supported see section 3 5 3 2 Quantifiers Quantification is possible over finite and infinite domains in the second case undecidability problems can arise Finite domains can be declared as Lisp list defvar Set One Two The formula Jt Set Formula t
9. lt k In this case the input file contains spec A prop and if prop indeed holds then the output history is empty If this is not the case the output history is a counterexample explaining why prop does not hold 2 INSTALLATION 2 2 Installation Zot s core is written in Common Lisp with ASDF packaging http www cliki net asdf It can be used under Linux Windows or MacOS X but has been tested only under Linux and Windows XP using the following Common Lisps e SBCL http www sbcl org e CLISP http clisp cons org e CMUCL http www cons org cmucl e ABCL http common lisp net project armedbear e Clozure CL http www clozure com clozurecl html This approach makes Zot an open system as it uses Common Lisp also as internal scripting language of the tool both to define complex verification activities and to add new constructs and languages on top of the existing ones Typically to install Zot in a Debian system or Ubuntu the user must install a Common Lisp e g one of the packages clisp sbcl cmucl and the common lisp controller package To perform a system wide install of the Zot packages just put symbolic links to its ads files in the usr share common lisp systems directory Note that it is possible to avoid a system wide installation but in this case the user has to work inside the main Zot directory Zot works with external SAT solvers The supported SAT solvers are MiniSat
10. real time systems Journal of Systems and Software 12 2 107 123 1990 M Lewis T Schubert and B Becker Multithreaded SAT solving In 12th Asia and South Pacific Design Automation Conference 2007 REFERENCES 31 16 M W Moskewicz C F Madigan Y Zhao L Zhang and S Malik Chaff engineering an efficient SAT solver In DAC 01 Proceedings of the 38th Conf on Design automation pages 530 535 New York NY USA 2001 ACM Press 17 M Pradella A Morzenti and P S Pietro A metric encoding for bounded model checking In A Cavalcanti and D Dams editors FM 2009 Formal Methods Second World Congress Eindhoven The Netherlands November 2 6 2009 Proceedings volume 5850 of Lecture Notes in Computer Science pages 741 756 Springer 2009 18 M Pradella A Morzenti and P San Pietro The symmetry of the past and of the future Bi infinite time in the verification of temporal properties In Proc of The 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering ESEC FSE Dubrovnik Croatia September 2007 19 M Pradella A Morzenti and P San Pietro Benchmarking model and satisfiability checking on bi infinite time In 5th International Col loquium on Theoretical Aspects of Computing ICTAC 2008 Istanbul Turkey September 2008 20 M Pradella A Morzenti and P San Pietro Refining real time sys tem specifications thr
11. A User s Guide to Zot June 2013 CONTENTS Contents 1 2 Overview Installation 2 1 Hello world 000000000 000004 Languages Sul CEELB pA e aa ad aa a 3 2 QUAMbl erS 22s ea Sd adi a a a ee he 3 3 Short examples curra ad ee a iA MG TG pete ches O stele es ALG atten 30 ARO a ho aa eon eel tes Motus da te cic o 3 6 Operational constructs s osoo a a ee A Sa case ee ES a Maan Gate teen eh ad es hk a 3 8 Timed Automata 2 0 0 00000 ee ee ee Usage Ail SAT solVers ti g Ge co Stee el ade e God ey GG ed 422 SMT esolvers s 5 ao ek St aa le a A ls 4 3 Model Checking 0 2 000220004 4 4 Completeness vn o ee el ee a ed A a a 4 5 Satisfiability Checking 0 4 6 Temporary data 0 200000 0004 Architecture 5 1 PLTL to SAT encodings 0 0 2 Main Interface ocr i celp he eae dia ala a 5 3 Other modules and plug ins 15 15 15 15 21 23 25 1 OVERVIEW 1 1 Overview Zot is an agile and easily extendible bounded model checker which can be downloaded at http home dei polimi it pradella The tool supports different logic languages through a multi layered ap proach its core uses CLTLB DL 6 and on top of it a decidable predicative fragment of TRIO 14 is defined An interesting feature of Zot is its ability to support different encodings of temporal logic as SMT problems by means of plug ins
12. V x 0 P B The following function is useful to define the transition from the value 1 to 0 of an arithmetic temporal term defun g z amp amp z 0 yesterday z 1 The definition of g is realized by combining CLTLB language and Common Lisp language During the process of evaluation of the function the variable z is substituted with its evaluation The function has to be used accordingly to the syntax defined by the declared formula In this case the variable z is an arithmetic temporal term X7x a correct use is for example lt gt P A g mext V y where the variable y is a CLTLB variable defined by using the construct define tvar The following example makes use of two uninterpreted function A and B and quantification over finite domains A and E define tvar A int int int define tvar B int int defconstant f 3 LANGUAGES 10 A x 123 FAS y 10 23 alwf gt 28 x y gt V A x y 0 next V A x y V Ax y EV B x 3 4 PLTL PLTL is a subclass of CLTLB in which no relations functions and variables appear Nevertheless variables over finite domains can still be used actually this is only a useful shorthand If the problem is expressed in PLTL there is no need to declare a costraint system The following temporal operators are supported until since release trigger next yesterday zeta The la
13. added to the set of available SMT solver 4 3 Model Checking To perform Bounded Model Checking the user must provide the model as transition system through as argument transitions In this section only the next operator is admitted Important every variable used must be declared implicitly by e g an initialization formula as the second argument of Zot Here we start with a simple example mutex3 a simple mutual exclusion protocol with three processes 4 USAGE 16 As mutex3 is expressible in LTL the first part is used to load the propo sitional mono infinite plug in and defines the used variables The first line loads the propositional mono infinite plug in called eezot bezot is the bi infinite one asdf operate asdf load op eezot use package trio utils defvar state d N T C defvar turn d 1 2 3 define array state turn d state d define item turn turn d defconstant decl optional declarations just for checking usage append loop for x in state d append loop for y in turn d collect state y x loop for x in turn d collect turn x Then we define the system initialization and transitions defvar init system initialization at 0 amp amp A x turn d state x N turn 1 defvar trans list of model constraints list A p turn d or case x state d state p N next state p T amp amp state p T A pi turn d gt not
14. ation init must hold at 0 spec negated property transitions trans list of model constraints declarations decl optional declarations 4 USAGE 18 UNSAT means that the desired property holds If the output is SAT then spec does not hold and Zot returns a counter example Now we show an example that require the full expressiveness of CLTLB LIA It represents a time varying variable taking two possible values 0 and 1 in an hysteresis like way led by an independent variable x The two parameters of the hysteresis cycle are the thresholds x0 and x1 The system is defined by a set of CLTLB LIA formulae descriptive specification and therefore it is not represented by a transition system The first line loads the arithmetic mono infinite plug in called ae2zot asdf operate asdf load op ae2zot use package trio utils define tvar x int define tvar y int define tvar d int define var x0 int define var x1 int Observe that x0 and x1 are time invariant variables so they are actually undefined constant We define some high level construct following the suggested constructs explained in Section 3 1 in order to have a coincise description of formulae defining the system defun up down z amp amp 1 z 0 yesterday z 1 defun down up z amp amp z 1 yesterday z 0 defun low z z 0 defmacro high z z 1 As previously anticipate
15. d it is worth noticing that the definition of these function is realized by merging CLTLB language and Common Lisp lan guage During the process of evaluation of the function the variable z will be substituted with its evaluation Then we define the system initialization and formulae defining the be havior of the system defvar init amp amp 4 USAGE 19 V x 3 CES V y 0 defvar tr up down alwf gt amp amp yesterday amp amp lt V x V x1 high V y D V x V x1 up down V y defvar tr down up alwf gt amp amp yesterday amp amp gt V x V x0 low V y lt V x V x0 down up V y defvar s up down alwf gt up down V y amp amp yesterday lt V x V x1 C V x V x1 defvar s down up alwf gt down up V y amp amp yesterday gt V x V x0 lt V x V x0 defvar low state alwf gt low V y 4 USAGE 20 since until low V y down up V y up down V y defvar high state alwf gt high V y since until high V y up down V y down up V y defvar high low state is alwf low V y high V y defvar continuous x alwf next V x V x 1 next V x V x 1 defvar Ncontinuous x a
16. e representation of its model of length 5 asdf operate asdf load op eezot use package trio utils eezot zot 5 amp amp P Hello next P world The first two lines load the plugin eezot for LTL and the basic definitions of operators available from trio utils lisp The Common Lisp function zot of the package eezot is invoked with the length of the finite model and the LTL formula to be satisfied The output reported is the model satisfying the LTL formula hello Xworld hello holds in the origin instant and world in the next one The formula is evaluated in 1 which is the origin of the model the instant 0 is defined for technical reasons It is worth noticing that predicate hello holds in 1 and world holds in 2 If no formula defines the truth value of 2 INSTALLATION 4 generic subset of the atomic propositions or formulae for a generic time instant then in that instant it may or may not holds this is the case of world which holds in 1 and hello in 2 The resulting finite model is a prefix of all infinite models satisfying the formula since the proposition LOOP denoting the position of the periodicity does not appear This is not the case of the following example in which the LTL formula G hello A Xworld for all instant from the origin towards the future hello holds and world in the following one is considered asdf operate asdf load op eezot use package trio utils eezot zot 5 al
17. fined accordingly to Common Lisp language They are firstly interpreted by the Common Lisp interpreter and the results is used to define the CLTLB formulae Here a short list of useful constructs of the Common Lisp language is provided Constants a Lisp constant c of value v is declared in the following way defconstant c v Variables a Lisp variable v is declared in the following way defvar v 1 defvar v One Two Note that the value of a constant or a variable can be any Common Lisp ob ject including CLTLB formula since they are Common Lisp list as shown later in the section 3 3 Functions an n ary Lisp function fun of domain is defined as defun fun x_1 x_n axioms where axioms describe the properties of fun The user should consider these functions as procedure and should not confuse them with a CLTLB unin tepreted function relation defined in the following section At the end of the section after the definition of of the syntax of CLTLB a simple example is provided Valuation of a function if fun is an n ary Lisp function the value fun x1 2n is written as fun x_1 x_n Predefined operation and relations a small number of binary opera tion relations between integer are predefined in Common Lisp namely X lt lt gt gt with their usual meanings op x_1 x_2 2A basic knowledge of the language is required It is very easy to find online a lot of tutorials and s
18. hort presentations e g http gigamonkeys com book 3 LANGUAGES 7 3 1 CLTLB CLTLB Counters LTL is essentially Propositional LTL with both future and past operators PLTLB with in addition terms that are arithmetic constraints in Integer Difference Logic CLTLB DL or in Linear Integer Arithmetic CLTLB LIA Propositional operators are written as not amp amp and or gt implies and lt gt equivalent Propositional letters a proposition Q is written P Q Relations there exist two possible way to define a relation 1 Uninterpreted time variant relations an uninterpreted i e satisfying no axioms time variant relations i e varying in time rel on the set types X X type is defined as define tvar rel type_1 type_n 2 Uninterpreted time invariant relations an uninterpreted i e satisfy ing no axioms time invariant relations i e constant in time rel on the set type X X typen is defined as define var rel type_1 type_n Time variant unvariant variables are defined as 0 ary relations The do mains specified as type_i are actually the ones supported by the used SMT solver Available keywords are one to define Integers int one to define Reals real and bool to define Boolean supported in Z3 Valuation of a predicate if R is an n ary relation the boolean R 21 n is written as V R x1 xn Valuation of a variable a variable
19. inf p The plug in offers the following operations normalize basicize compute granularity over approximation under approximation nth divisor To compute over and under approximations an axiom must be prepared through the two functions basicize and normalize e g with setf ax1 normalize basicize ax1 The two functions over approzimation and under approximation are used to compute the approximated formulae while compute granularity is used to set the p parameter see 11 for details The interested reader may find a complete example in coffee lisp 3 8 Timed Automata Timed Automata TA are supported through a very experimental plug in called ta zot see 12 13 which is based on the approximations offered by ap zot As for ap zot only the pure propositional version is supported First here is a list of the added operators and approximations proce dures 3 LANGUAGES 14 white tri white tri 3 black tri black tri 3 timed automaton under formula timed automaton over formula timed automata under formula timed automata over formula Here is the main data structure used to represent TA s together with its interface defstruct timed automaton alphabet states initial states clocks defgeneric add trans autom from to lamb constr defgeneric add label autom state list of symbols defgeneric alpha autom state defgeneric get trans from states autom from to defgeneric all connected pa
20. ints system QF_UFLIA must be loaded If not the default constraint system is QF_UFIDL 4 4 Completeness A switch of the zot procedure loop free nil by default of the propositional plug in eezot beezot is used to check completeness In the first example above we can check completeness by performing eezot zot 30 time bound yesterday init initialization init must hold at 0 4 USAGE 22 transitions trans list of model constraints declarations decl optional declarations loop free t check completeness UNSAT means that the completeness bound is reached The zot procedure returns t if the spec is satisfiable nil otherwise So it is possible to write a loop to actually find the completeness bound e g 4 USAGE 23 format t Found s loop for bound from 2 unless eezot zot bound yesterday init transitions trans declarations decl loop free t return bound 4 5 Satisfiability Checking Let us now consider a simple example to show how satisfiability checking can be performed with Zot The first line loads the bi inifinite plug in asdf operate asdf load op bezot use package trio utils We then define the timed lamp spec defconstant delta 5 Alphabet on the on button is pressed off the off button is pressed an be the light is on defconstant init amp amp Cll P on P off P L defconstant the lamp alw amp amp lt
21. irs autom defgeneric all unconnected pairs autom defgeneric get all trans autom defgeneric get trans from clock reset autom clock The interested reader may find a complete example in trans_prot lisp 4 USAGE 15 4 Usage 4 1 SAT solvers The supported SAT solvers are MiniSat 9 which is used by default Mi raXT 15 and zChaff 16 To use the zChaff SAT solver the user has to set the zot solver pa rameter For example setq sat interface zot solver zchaff MiraXT is a multi threaded solver so to use it we also have to choose the maximum number of threads that it will use setf sat interface zot solver miraxt setf sat interface n threads 3 4 2 SMT solvers SMT solver are used in the decision procedure for the plug in ae2zot The supported SAT solvers are Z3 3 which is used by default Yices 5 CVC3 1 and MathSat 2 To change the SMT solver the user has to set the Lisp keyword solver when invoking the function zot For example zot 10 formula solver yices Available keyword are z3 yices and mathsat ae2zot is written to agree with the SMT LIB v 1 4 whose major goal is to establish common standards and library of benchmarks for Satisfia bility Modulo Theories that is satisfiability of formulas with respect to background theories for which specialized reasoning procedures exist Every other SMT solvers respecting the standard of the SMT LIB can be easily
22. is written E t Set Formula t The definition of the Lisp variable Set is optional and the same formula can be written as E t One Two Formula t A is the universal quantifier Infinite domains are implicitly declared by the definition of the con straint system Available domains from SMT LIB are Integers and Reals By the definition of satisfiability all logic variables as well as values of uninterpreted functions and predicates are existentially quantified The formula 3t Z Formula t requires the definition of a logic variable by define var h int or define var h real and it is written Formula V h by simply substituting the instance of t with the evaluation of V h 3 LANGUAGES 9 It is worth noticing that the Naturals can be defined by constraining the value of the existentially quantified variable The formula At N Formula t can be written amp amp gt V h 0 Formula V h and Formula should be defined by the construct defun The first form which uses the Lisp definition of sets as lists can be equivalently written by using logic variables values of a variable over a finite set are defined by an explicit list amp amp 11 V h c_0 V h c_1 Formula V h 3 3 Short examples Some simple examples of compound syntax of CLTLB and Common Lisp are here shown defconstant p lt gt until P A gt
23. lasts P A t 3 O lt tA is written withinf P A t 4 A or M_ 4 is written past P A t 5 B lt A is written lasted P A t 6 lt A is written withinp P A t with t gt 0 3 6 Operational constructs Zot offers some simple facilities to describe operational systems The fol lowing constructs are represented by means of a propositional encoding and therefore they are available both for SAT based plug in e g eezot and for SMT based plug in ae2zot define item lt varname gt lt domain gt is used to define variables la Von Neumann over finite domains e g coun ters define array lt varname gt lt index domain gt lt domain gt is used to define mono dimensional arrays Example usage 3 LANGUAGES 12 define item cont loop for i from 0 to 9 collect i define array arr loop for i from 0 to 9 collect i on off unknown In the spec the user can e g write cont 6 arr 6 off Caveat both define item and define array have side effects It is there fore wrong to define items after a zot main procedure call since successive calls may work with spurious constraints It is therefore recommended to perform clean up before defining items or arrays Typically to define an operational model means to constraint operational variables and arrays This can be done either by using simple next time formulae i e containing only the next temporal operator or
24. lwf next V x V x V d defvar safe state alwf amp amp gt V V y 1 lt V x V x1 gt V V y 0 gt V x V x0 defvar thresholds DJ V x1 V x0 defvar syst amp amp high low state is high state low state 4 USAGE 21 tr up down tr down up s up down s down up cont inuous x thresholds As already anticipated the main procedure is called zot and has two ar guments the time bound and the formula to be satisfied plus some optional switches e g transitions declarations logic To check if the system is satisfiable i e it admits at least one behavior for a time bound of 15 we perform ae2zot zot 15 amp amp init syst logic QF_UFLIA If it is the case then the tool provides two values for the two thresholds x0 and x1 The satisfiability of the formula represents an instance of synthesis problem since the two thresholds values are not previously defined Being variables of the problem they will be given a value which fulfills the axioms To check if the property safe state holds for a time bound of 15 we perform ae2zot zot 15 amp amp init syst 1 safe state logic QF_UFLIA If the safe state property holds then the tool answers UNSAT Available keyword for logic are QF_UFIDL and QF_UFLIA Observe that the formula uses explicitly sum and difference and so the constra
25. ough bounded model and satisfiability checking In 23rd IEEE ACM International Conference on Automated Software Engineering ASE 2008 L Aquila Italy September 2008
26. r of a subclass defgeneric call self obj the time amp rest other stuff The back call generic is used to translate an integer in 0 k into the cor responding subformula self must be an instance of kripke or of a subclass defgeneric back call self x defgeneric back call time self x 5 2 Main Interface There are two interfaces sat interface lisp the first one is with the SAT SMT solver and it is used to send the output of the PLTL CLTLB encoding to it then to parse its output and get a counter example if any The other one 5 ARCHITECTURE 28 trio utils lisp is the basic interface with the user and is based on TRIO see Section 3 5 augmented with the operational constructs covered in Section 3 6 5 ARCHITECTURE 29 5 3 Other modules and plug ins At present just ap zot and ta zot are available Please refer to Sections 3 7 3 8 and the related papers The two plug ins are implemented and packaged as asdf systems in ap zot lisp ap zot asd ta zot lisp ta zot asd ta zot is based on ap zot which uses TRIO as underlying language through the trio utils interface Acknowledgments I thank the following people Stefano Riboni for his work on the CNF trans lator Davide Casiraghi for the metric plugins meezot and mbezot REFERENCES 30 References 1 10 11 13 14 CVC3 http http www cs nyu edu acsys cvc3 Mathsat5 http http www cs nyu edu acsys cvc3 Mic
27. rosoft Z3 http z3 codeplex com Smt library http smt lib org Yices2 http yices csl sri com M M Bersani A Frigeri M Pradella M Rossi A Morzenti and P San Pietro Bounded Reachability for Temporal Logic over Con straint System In Proc TIME 2010 A Biere PicoSAT essentials Journal on Satisfiability Boolean Mod eling and Computation JSAT 4 75 97 2008 A Biere K Heljanko T Junttila T Latvala and V Schuppan Lin ear encodings of bounded LTL model checking Logical Methods in Computer Science 2 5 1 64 2006 N E n and N S rensson An extensible SAT solver In SAT Confer ence volume 2919 of LNCS pages 502 518 Springer Verlag 2003 C A Furia M Pradella and M Rossi Dense time MTL verifica tion through sampling Technical Report 2007 37 DEI Politecnico di Milano April 2007 C A Furia M Pradella and M Rossi Dense time MTL verification through sampling In Proceedings of FM 08 volume 5014 of LNCS 2008 C A Furia M Pradella and M Rossi Practical automated par tial verification of multi paradigm real time models Technical Report arXiv org 804 4383 April 2008 C A Furia M Pradella and M Rossi Practical automated partial verification of multi paradigm real time models In 10th International Conference on Formal Engineering Methods ICFEM October 2008 C Ghezzi D Mandrioli and A Morzenti TRIO A logic language for executable specifications of
28. st one is the dual of yesterday and is used only in the mono infinite semantics For the semantics of these operators see e g 6 or any other note about LTL 3 5 TRIO Zot was originally born as a satisfiability checker for the TRIO metric tem poral logic 14 The list of supported operators and their correct Zot spelling is the following dist futr past lasts lasts_ee lasts_ie lasts_ei lasts_ii lasted lasted_ee lasted_ie lasted_ei lasted_ii withinf withinf_ee withinf_ie withinf_ei withinf_ii withinp withinp_ee withinp_ie withinp_ei withinp_ii lasttime lasttime_ee lasttime_ie lasttime_ei lasttime_ii nexttime nexttime_ee nexttime_ie nexttime_ei nexttime_ii somf somf_e somf_i som somp somp_e somp_i alwf alwf_e alwf_i alw alwp alwp_e alwp_i until until_ie until_ee until_ii until_ei since since_ie since_ee since_ii since_ei Bounded version of since and until are written as 3 LANGUAGES 11 until_ie_ lt _ lt t1 t2 A B B will be true at t instants in the future with t1 lt t lt t2 until_ie_ gt t1 A B B will be true at t instants in the future with t gt t1 since_ie_ lt _ lt since_ie_ gt Caveat emptor The default until is PLTL s which is usually called until_ie in TRIO For example the following model satisfies until A B at 0 AAAAAAAAAAAAAAAAAAAAA B may appear at 0 For MTL users 1 9 A or D A is written futr P A t 2 O lt A is written
29. wf amp amp P hello next P world the resulting model is LOOP HELLO WORLD 2 INSTALLATION 5 The LTL operator G is written as alwf always in the future and the symbol amp amp is the usual A boolean connective The finite model represents the infinite periodic model given by the w regular expression h w th w th w h w Lh wh where h w are shorthands for hello and world respectively Let consider the following example in which it is shown an unsatisfiable LTL formula G hello A Xworld A F hello asdf operate asdf load op eezot use package trio utils eezot zot 5 amp amp alwf amp amp P hello next P world somf P hello The output is clearly The operator somf corresponds to the LTL operator F and means eventu ally in the future 3 LANGUAGES 6 3 Languages Being an open system Zot supports different languages At present the main native language is CLTLB 6 linear temporal logic with future and past operators over constraint systems and its subclasses The other main layer based on PLTL is the metric temporal logic TRIO Zot scripts are interpreted as a usual Lisp code Beside the CLTLB temporal operators and relations functions available from the constraints system used Difference Logic Linear Integer Arithmetic the user can de fine own constructs and embeds them in the CLTLB formulae These con structs are de
Download Pdf Manuals
Related Search