χChek RC2 User Manual - Department of Computer Science
Contents
1. EJ Model fairness B fairness en lt gt Algebra Preferences Output Options Compiled in 0 58s Fairness Macros loaded Use fairness Model Checking AG state Searching gt EF state Ready Fairness conditions to be used AG state Searching gt EF state Ready au Done in 0 149s O Selected Result is T Remove Produce counter example CTL state Searching gt EF state Ready v Figure 5 2 Model Checking main window after successfully checking a property 28 5 2 Vacuity Detection In the following example we show how XChek can be used for vacuity detection according to See Gurfinkel and Chechik GC04 The 3 valued Kleene logic F is used for this purpose They show that is it possible to detect the vacuity of a propositional formula y with respect to a formula w that is pure in y by a replacing all occurrences of Y by M and b interpreting the result in the 3 valued Kleene logic If the new property evaluates to then is vacuously true If it evaluates to F then is vacuously false Finally if y evaluates to M no decision can be made w r t the vacuity of the formula Model examples gclang peterson gc 1 2 Main window press Model button Pick a compiler window choose the GCLang Compiler Options2. All SMV Model Compiler Flat Selected edu toronto cs xkripke XMLXKripkeModelCompiler Propertie Property Settings xmlFile edu toronto cs xkripke XMLXKripkeModelCompiler Optid M Property Editor Cancel Produce counter example Figure 4 4 The Options window for the XML model compiler Only one option is available XML file Click on this option and use the browse button to pick an XML model Afterwards press the OK button XChek will produce the following message in the main output area if model loading was successful Compiled in xx xxx s loaded 4 2 CTL History files A CTL history file is just a simple list of properties one per line To load a CTL history file press the load CTL button The user will be prompted for a history file XChek will create a drop down menu using this history file which is accessible from the CTL input box For example given the following CTL history file AG state Searching gt EF state Ready EF state Canceled AG AF state Canceled AG AF state Canceling 20 XChek produces the drop down menu seen in Fig 4 5 File Model Fairness CTLhistory Help 1 r Y 1 fairness fairness d CTL Algebra Preferences Output Options Compiled in 0 585 Fairness Macros loaded C Use fairness Fairness conditi
3. implExpr implExpr implExpr implExpr implExpr implExpr implExpr implExpr implExpr implExpr implExpr implExpr implExpr implExpr implExpr implExpr implExpr implExpr implExpr implExpr implExpr implExpr implExpr basicExpr varname number boolConstant expr boolConstant true false rulesBlock RULES guardedCommand guardedCommand guard command guard expr command SequenceCommand SequenceCommand choiceCommand choiceCommand choiceCommand atomicCommand atomicCommand atomicCommand assign SKIP ite command assign varname expr disjunction exclusive or conjunction negation implication if and only Xf equal not equal less than greater than less or equal than greater or equal than module addition subtraction multiplication division rules that specify model behavior statement concatenation non deterministic choice assignment empty instruction do nothing if then else group of commands Rw nN ite if expr then iteBody then is optional iteBody command else command fi Note Usual precedence rules apply and comments start with EXAMPLE the Peterson mutual exclusion algorithm
4. NAME peterson VAR 5 boolean yl boolean y2 boolean pel 0 1 2 3 pe2 f 0 1 2 3H INIT 13 amp yl amp y2 amp pcl 1 amp 2 1 RULES guards for process 1 1 1 yl true s true 1 2 1 2 if y2 s pel 3 else skip fi 1 3 yl false pel 1 guards for process 2 2 1 y2 true s false 2 2 pc2 2 amp yl s 2 3 2 3 y2 false 2 1 In this example the model s name is peterson line 1 Five variables are defined s yl y2 pcl and pc2 lines 3 7 The variable s is used to keep track of which process should enter the critical section Variable y 1 y2 is used by the first second process to indicate that it is in the critical section Variable pc1 pc2 is used to store the state of the first second process These variables are defined by enumeratation 1 not in critical section 2 trying to get into critical section 3 in critical section The value 0 is included to make the booleanization of pc1 pc2 easier Line 9 initializes s y1 and y2 to false and pc1 2 to 1 Finally the mutual exclusion algorithm is described using guarded commands lines 10 28 3 1 3 XML Compiler XMLXKripkeModelCompiler edu toronto cs xkripke XMLXKripkeModelCompiler Multi valued models are specified in XML by mapping the model to a GXL graph that represents the model s behavior Nodes are labeled by va
5. pick Kleene query checking according to Gurfinkel et al GCD03 pick upset e SMV File use the browse button to pick a flat SMV model e MvSet Implementation decision diagram implementation used for this model We recommend using mdd mdd our own multi valued decision diagrams Everything should work with this jadd our own multi valued decision diagrams over Boolean variables used for debugging testing and comparisons to CUDD Som01 Counterexamples may not always work with this cudd add CUDD based implementation Supports multi valued analysis but not counterexample gener ation jcudd new CUDD based implementation developed for Yasm GCOS Once all the options have been set press the OK button XChek will produce the following message in the main output area if model loading was successful Compiled in xx xxx s loaded 19 4 1 2 XML models As XML models specify the logic used to encode the model there are fewer options when loading an XML model To load an XML model choose the XMLXKripkeModelCompile compiler in the Pick a compiler window The Options window for the XML compiler is shown in Fig 4 4 File Model Fairness CTL history Help SS amp Model fairness fairness d CTL CTL Algebra Preferences e Output Options Faimess Macros Pick a model compiler Use fairness GCLang Compiler _ Fairness conditions to be used XMLXKripkeModelCompiler ok
6. Amsterdam North Holland 1978 Somenzi CUDD CU Decision Diagram Package Release 2001 32
7. edge edge from FF type val edge edge from FT type val edge edge from lt type val lt edge gt lt graph gt gxl ION ORDER to FF lue to TT lue to TF lue to FT lue An explanation of the various items in the logic encoding file 1 2 GXL namespace declaration the graph is directed and it s id is 4 3 link to an image showing the logic s lattice In this case the image linked is the one shown in Fig 3 2 4 8 logic values TT TF FTandFF 9 21 edges of the graph describing the logic s truth ordering For example in Fig 3 2 we see that TT is above TF in the lattice ordering which is encoded in lines 10 12 22 34 negation order which describes the result of negating the different logic values For example lines 29 21 tell us that FT is the negation of TF 13 3 3 Properties Properties are specified in Computation Tree Logic CTL CGP99 The syntax of CTL formulas recognized by XChek is as follows ctlExpr basicExpr a simple boolean expression MCN ctlExpr ctlExpr disjunction alternative symbol ctlExpr amp ctlExpr conjunction alternative symbol gtlExpE negation alternative symbol ctlExpr ctlExpr implication ctlExpr ctlExpr if and only if EX ctlExpr exists next sta
8. an initial state 22 37 transition definitions For example in Fig 3 1 we see that there is a TT transition between states 50 and s1 which is encoded in lines 23 25 3 2 Algebras The class of logics XChek can use are those whose logical values form a finite distributive lattice and where there is a suitably defined negation operator that preserves De Morgan laws and involution a a Such lattices are called quasi boolean and the resulting structures are called quasi boolean algebras Ras78 3 2 1 Available algebras XChek is distributed with some of the more commonly used multi valued logics like Boolean for classic model checking CGP99 Kleene used for vacuity checking GC04 4 valued disagreements logic used for reasoning about model disagreements ECO1 upset used for query checking GCD03 etc For SMV and models Boolean Kleene and upset algebras are available For XML models the following algebras are available e 2val logic xml classic two valued logic Can be used for model checking e 3val logic xml Kleene three valuedlogic T M maybe This logic is useful for representing partial models See Gurfinkel and Chechik GC04 for an explanation of how this logic is used for vacuity detection 4val logic xml a4 valuedlogic TT TF FT FF that has been used to model disagreements that arise when composing two models drawn from different sources ECO1 e 4fto
9. and Chechik GC04 for an explanation of how Kleene logic is used for vacuity detection and Section 5 2 for an example of how vacuity checking is done in XChek EF x pcl pc2 amp EX pcl 3 amp pc2 3 Query checking This query is also w r t the Peterson mutual exclusion algorithm It has one placeholder x which is restricted to the model variables pc1 pc2 In other words XChek will look for the set of strongest propositional formulas involving pc1 pc2 that make the query true See GCD03 for details on query checking and Section 5 3 for an example of how query checking is done in XChek 15 Chapter 4 Guide to the XChek User Interface In this chapter we show how various tasks are carried out in XChek XChek is controlled through the main XChek GUI shown in Fig 4 1 There is no command line interface XChek LA ene moger Faimess CTL niston Helm B Model fairnes tairnes d ce Algebr Preference e Output Options Fairness 1 Macros2 Use fairness Fairness conditions to be used amp All Q Selected Add Edit Remove Sa 4 Run 21 Trace 3 v Produce counter example Figure 4 1 The main XChek windows Main window components A Menu 1 File access to Model options and Preferences A2 Model access to Model info and Show variables functions Not functional in th
10. be viewed using these tools by pressing the Grappa or DaVinci buttons 21 8 KEG window Proof Current State KET U I state Searching U state Ready a0 T a0 U K state Searching E T U state 11 0 F reject F CA EIT Uo state Searching U state Readyj l a1 State Initiab amp 9 state Searching U state Readyy al F cancel P search uipProcessesState Idle turn statemachine approve F cancelFinished F select F searchCanceled F searchFinished F davinci Grappa Figure 4 6 Default counterexample viewer The Grappa button generates the dot graph corresponding to the counterexample see Fig 4 7 The DaVinci button starts up uDraw Graph see Fig 4 8 uDraw Graph graphs are expandable you can click on a node to see a subgraph The Hide Proof option see KegTree preferences controls whether proof nodes of the counterexample should appear as expanded or not when the graph is initially presented reject F state Initial cancel F search F tripProcessesState Idle Draw turn statemachine approve F cancelFinished F searchCanceled F Qui searchFinished F K E T U l I state Searching V E T U state Ready D DI3CD Figure 4 7 Counterexample view using Grappa 22 u
11. compiler Thus in this section we only show the steps for loading an SMV model To load a flat SMV model choose the SMV Model Compiler Flat compiler in the Pick a compiler window An Options window will appear see Fig 4 3 For SMV models there are three options Model Checking Algebra SMV File and MvSet Implementation 18 E xchek File Model Fairness history Help ll nn P amp Model fairness fairness a CTL CTL Algebra Preferences e Output Options Faimess Macros B Picka model compiler 152 Use fairness GCLang Compiler SMV Model Compiler Flat edu toronto cs smv parser smvCompiler Fairness conditions to be used All Selected Properties Property Settings Model Checking Algebra SMV File MvSet Implementation edu toronto cs smv parser SmvCo Options Property Editor Cancel Produce counter example Figure 4 3 The Options window for the flat SMV model compiler Click on an option to set its value e Model Checking Algebra drop down list of possible logics User picks a logic for the model that is currently being loaded This choice depends on what XChek is being used for For classical 2 valued model checking pick 2 vacuity checking according to Gurfinkel and Chechik GC04
12. logic xml a4 value finite total order ME MT maybe false MT maybe true e 5fto logic xml 5 finite total order possibly false PT possibly true Each of these algebras is encoded in an XML file which maps the algebra s Hass diagram to a GXL graph edges are the truth ordering Thus users can introduce their own logics by encoding the corresponding Hass diagrams 11 3 2 2 Encoding an algebra An algebra encoding is divided into five parts e Namespace declaration optional Link to image of the corresponding Hass diagram Logic values one node tag per logic value in the algebra The node tag can have an optional lt att r gt tag where a description of the logic value can be specified Logic order specify the ordering of the lattice through the above relationship One edge tag per edge in the lattice Negation order describes the result of negating the different logic values through the neg relationship Must specify the negation of all logic values one edge tag per logic value Basic structure of an algebra file lt gxl xmlns xbel www cs toronto edu xbel xmlns xlink xlink graph ID user defined edgemode directed gt OPTIONAL Hass diagram image gt xbel img xlink type simple xlink href link to image of Hass diagram gt lt LOGIC VALUES gt node ID logic value node ID logic v
13. may take any of the truth values of a given multi valued logic Properties are expressed in XCTL a multi valued extension of the temporal logic CTL Additional information about the algorithms and the data structures used by XChek is available in Gur02 CDEGO3 CGD 06 XChek is distributed under a FreeBSD license For the terms of this license see http www freebsd org copyright freebsd license html The main features of XChek are the following e Multi valued logics 2 valued 3 valued upset 4 valued disagreements etc Users can define their own logics e Multiple model formats reads SMV and GCLang models Multi valued models are specified in XML e Proof like counterexamples proof rules are used to generate counterexamples Counterexamples can be gener ated statically or dynamically and various viewers are available This document is structured as follows e Chapter 2 Installation e Chapter 3 Input models algebras and properties e Chapter 4 Guide to the XChek User Interface loading models CTL history files counterexample viewers and preferences e Chapter 5 Tutorial model checking vacuity detection and query checking Known bugs and limitations e XChek sometimes runs out of memory when statically computing a counterexample e XChek is a best effort implementation We recommend restarting XChek before loading a new model Collaborators Marsha Chechik Benet Devereux Steve Easterbrook Arie Gurfink
14. window e Model Checking Algebra Kleene e GCLang file examples gclang peterson gc e MvSet Implementation mdd Options window press OK when options have been set CTL input box type in the following property AG 1 3 amp 2 3 gt yl Optional Check the Produce counter example box to produce a counterexample for this property Press Run The Main window should now look like the one in Fig 5 3 The property is true Notice that we can check Boolean properties when the model is loaded as Kleene since Boolean logic is subsumed by Kleene logic We will now check the vacuity of the formula by checking the following formulas M amp 2 3 gt yl AG 1 3 amp M gt yl 1 3 amp 2 3 gt CTL input box type in each of these properties press Run after each one The Main window should now look like the one in Fig 5 4 if the steps uptil now have been followed correctly Interpreting the results M amp pc2 3 gt yl result M 1 3 amp M gt yl result AG 1 3 amp 2 3 gt M result The original property AG 1 3 amp pc2 3 gt yl is vacuously true w r t the following subfor mulas pc2 3 1 29 File Model Fairness CTL history Help 9 Model i fairness 9 fairness CTL lt gt Algebra Preferences Output Optio
15. Draw Graph 3 1 1 keg9129status File Edit View Navigation Abstraction Layout Options Ed tripProcessesState Idle turn statemachine approve F cancelFinished F select searchCanceled F searchFinished F Bil s s U state Searching V EIT U state Ready P D I T Figure 4 8 Counterexample view using uDraw Graph The experimental counterexample viewer seen in Fig 4 9 is not as user friendly as the default viewer since this is a new feature This viewer s interface is very simple and basically only displays the internal data strcture as is However it is interactive the proof is generated as the user clicks on the leaves that she wants to expand E T U I state Searching E T U state Ready pplI FOO T E IIKE T U Searching E T U state Ready DII FOO T EAIMELT U Searching E T U state Ready ppII FOO D E T U I state Searching E T U state Reacly FOO Figure 4 9 New experimental counterexample viewer 4 4 Preferences To specify user preferences for XChek press the Preferences button The XChek Preferences window should appear see Fig 4 10 By default the General preference options will be displayed Grappa and KegTree preferences can also be set see Figs 4 11 and 4 12 respectively Use the Apply button to apply preference c
16. XChek RC2 User Manual Documentation maintained by Jocelyn Simmonds and Arie Gurfinkel xchek cs toronto edu Department of Computer Science 40 St George Street University of Toronto Toronto Ontario Canada MSS 2E4 This document is part of the distribution package of the XChek model checker Copyright 2002 2007 by University of Toronto Contents 1 Introduction 2 Installation 3 Input Models d Hale ele SIE XOT Ae ee EE a SMV RE Saige S ae et Ake Bee Se te ai 331 GCLang fo ied Seo Ed be bate d we eb Ph mr oe ed 3 11 35 eb ak aes ee EAS es ROGO E ge 3 2 AIBeDr2S pe Ar Cee HESS Se eee RE RP E Peer E a 52 1 Avaablealgebras eer aS eb ver REPE ge 32 2 Encodmg amalgebra 2 is PU uw SERVI Wr Bee uere 3 3 Properties oS Ae op E EU PUR S SUE S Ba der E Pa ese 4 Guide to the XChek User Interface 4 T Eo dingamodel NARI Lm RA RE Uem Bate ae AUT TR RU 4 1 1 SMVandGCLangmodels 4 1 2 XML models c 5 sr Sos Po ah 8e eite qeu Role OR e de 42 CTL History Des ios Andie Fe eos Od Set BE mede metu 4 3 Counterexamples x eae oe Sw ee ded Be eat OW OG ea eee eed 44 IPTELETENCES eos poU E ede movere Rv enm are Aye eek de s We 5 T
17. alue OPTIONAL gt attr name desc value description node LOGIC ORDER interpreted as logic valuel is above logic value2 in the lattice gt edge from logic valuel to logic value2 type value above gt lt edge gt lt NEGATION ORDER gt lt interpreted as logic valuel is the negation of logic value2 gt edge from logic valuel to logic value2 type value neg edge graph gxl EXAMPLE 4 valued disagreements logic Now we will show how to encode the logic shown in Fig 3 2 TT FF Figure 3 2 4 valued disagreements logic 12 This is the encoding for this logic lt gxl xmlns xbel www cs toronto edu xbel xmlns xlink xlink graph ID 4 val edgemode directed xbel img xlink type simple xlink href examples xml 4val gif uv e 26 27 28 29 30 31 32 33 34 35 36 lt LOGIC VALUES gt lt node ID lt node ID lt node ID node ID gt FT gt FF gt lt LOGIC ORDER gt edge from TT to TF gt lt type value above gt lt edge gt edge from TT to F type val edge edge from TF to F type val edge edge from FT to F type val edge Lue above Lue above Lue above NEGAT edge from TT type val
18. ble gt attr type prop name model variablel value logic value attr type prop name model variable2 value logic value attr type prop name model variable3 value logic value attr type prop name model variable value logic value gt node lt an initial state gt node ID node_idl xbel initial true gt lt one attr tag per model variable gt attr type prop name model variablel value logic_value gt attr type prop name model variable2 value logic value attr type prop name model variable3 value logic value attr type prop name model variable value logic value gt node lt EDGES gt lt one edge tag per model transition gt 29 30 31 32 33 34 35 lt interpreted as there is a logic value transition from node idl to node id2 gt edge from node_idl to node id2 lt indicates the logic value of the transition gt attr name weight value logic value edge graph gxl EXAMPLE Now we will show how to encode the model shown in Fig 3 1 This model has been encoded in the 4 valued disagreements logic shown in Fig 3 2 TT H 50 52 Figure 3 1 A model encoded in the 4 valued disagreements logic This is the encoding for this model lt gxl xmlns xbel www cs toronto edu xbel xmlns xlink xlink gra
19. el Kelvin Ku Shiva Nejati Viktor Petrovykh Jocelyn Simmonds Rohit Talati Anya Tafliovich Christopher Thompson Walsh Kapil Shukla and Xin John Ma Chapter 2 Installation Prerequisites e Linux based OS Fedora Core 4 7 and Ubuntu 7 are known to work e Java SE 6 e Apache ant version gt 1 6 5 only for compilation Installation 1 Download XChek distribution archive 2 Extract the XChek archive to create a directory xchek with the following structure build xml XChek ant buildfile bin scripts for running XChek doc documentation Includes JavaDoc API and this doucment jsre the source code lib bindings to C libraries ext 3rd party Java libraries examples example models and properties 3 Optional Recompile by running ant 4 Run bin xc to execute XChek Notes The amount of memory given to XChek is controlled by setting environment variables MEMORY MIN and MI For example in bash MEMORY MIN 512m MEMORY MAX 1024m bin xc will start XChek with 512MB of available RAM and will allow the process to use up to 1024MB EMORY MAX Chapter 3 Input This chapter describes the syntax of model specification languages the syntax of algebra multi valued logic specifi cations and the syntax of temporal logic properties XChek supports models specified in either a simplified version of the SMV CCGt02 modeling language or the Guarded Command Language GCLang Arbitrary multi valued models are speci
20. examples It produces a graph describing the counterex ample in the format of the uDraw Graph tool Path to UDG home directory use the Browse button to specify the path to your uDraw Graph home direc tory uDraw Graph creates flow charts diagrams hierarchies or structure visualizations using automatic layout strategies Available at http www informatik uni bremen de uDrawGraph en index html Hide proofs controls whether proof nodes of the counterexample should appear as expanded or not when the graph is presented initially File Model Fairness CTLhistory Help EJ Model fairness fairness CTL Ej cn Algebra Preferences Out XChek Preferences Choose Grappa General Path to DOT Engine Grappa usr bin dot Browse KEGTree Export Close Run Trace 71 Produce counter example Figure 4 11 Grappa preferences 25 amp taimess E d CTL CTL amp Algebra NL al KEGTree Path to UDG home directo home jsimmond utilities uDrawGraph 3 1 Hide proofs Produce counter example Figure 4 12 KegTree preferences 26 Chapter 5 Tutorial In this chapter we show how XChek can be used for various purposes 5 1 Model Checking In the following example we show how XChek can be used for clas
21. fied in XML by explicitly describing the model s Kripke structure i e states and transitions These XML files also include a reference to the algebra used to describe the model XChek is distributed with some of the more commonly used multi valued logics like Boolean the classical 2 valued logic Kleene used for vacuity checking GC04 4 valued disagreements logic used for reasoning about model disagreements ECO1 upset used for query checking GCD03 etc 3 1 Models SMV and GCLang models are easier to read and maintain since high level instructions are used to specify the model XML models are easier to generate in an automated fashion Also this is the only way to explore the full generality of multi valued model checking in XChek 3 1 1 SMV Compiler SMV Model Compiler Flat edu toronto cs smv parser SmvCompiler SMV is the specification language of NNSMV CCG 02 Use the following steps to generate an input model for XChek 1 Specify your model using SMV This language is described in the NuSMV User Manual which can be found on the NuSMV website http nusmv irst itc it 2 Once satisfied with the model flatten it using NuSMV Modules and processes are instantiated when a SMV model is flattened Command 2 NuSMV ofm flat smv file smv normal smv file smv 31 2 GCLang Compiler GCLang Compiler edu toronto cs gclang parser GCLangCompiler GCLang is a simple guarded command language In thi
22. hanges and close 23 the XChek Preferences window using the Close button The Import and Export buttons can be used to load save preferences to from an XML file We are use Java Preferences API http java sun com j2se 1 4 2 docs guide lang preferences html to deal with user preferences FA xchek File Model Fairness CTLhistory Help a Model fairness 9 fairness dcn Out CTL Algebra Preferences XChek Preferences Choose General m Global Default Directory Grappa home jsimmond xbel xchek release Browse KEGTree Model Picker default directory home jsimmond xbel xchek release p Browse CTL file Picker default directory home jsimmond xbel xchek release p Browse Default CTL file home jsimmond xbel xchek release Browse Startup with Counter Example Enable Fairness v New experimental CexViewer Enable double buffering Look and Feel Requires Restart Default v Apply Impon Export Close Il Trace Produce counter example Figure 4 10 General preferences e General Global default directory use Browse button to change the value This directory will be used as the base directory by XChek when loading files Model Picker default use Browse button to cha
23. is version A3 Fairness load save fairness constraints Not functional in this version A4 CTL History load save CTL history 16 5 Help access to Help and About B Quick access buttons 1 Model quick access to the Model options B2 load Fairness load fairness constraints Not functional in this version B3 save Fairness save fairness constraints Not functional in this version B4 load CTL load CTL history A CTL history file is just a simple list of properties one per line XChek creates a drop down menu with these properties which is accessible from the CTL input box B5 save CTL save CTL history B6 Algebra change model algebra Not functional in this version B7 Preferences quick access to Preferences B8 Quit exits XChek If there are properties in the CTL input box XChek will prompt the user asking if these properties should be saved C Main output area various system messages appear in this area e g success on model loading results of model checking etc D Options these options are not functional in this version D1 Fairness will allow the specification of fairness constraints to be applied to the currently loaded model D2 Macros will allow the specification of macros which can be used to simplify CTL properties and fairness constraints E CTL area E1 Input box properties can be typed directly into this box Can also be used to access the drop down menu created when loading a CTL hist
24. lts 30 5 3 Query Checking In the following example we show how XChek can be used for query checking see GCD03 Queries are expressed as CTL formulas with missing propositional subformulas designated by placeholders Query Checking finds the formulas that make the query true Model examples gclang trip trip planning5 gc 1 2 Main window press the Model button Pick a compiler window choose the GCLang Compiler Options window e Model Checking Algebra upset e GCLang file examples gclang trip trip planning5 gc e MvSet Implementation mdd Options window press OK when options have been set CTL input box type in the following property AG x state gt EF state Ready This query has one placeholder restricted to the st ate variable Optional Check the Produce counter example box to produce a counterexample for this property Press Run XChek will look for the set of strongest propositional formulas involving state that make the query true The Main window should now look like the one in Fig 5 5 There is one solution for this query state Initial state Ready state Searching File Model Fairness CTLhistory Help E Model fairness E rairness d E Algebra Preferences Output Options Compiled in 0 367s Fairness Macros loaded C Use fairness Model Checking AG x state gt EF state Ready Fairness conditions to be u
25. lues of the atomic propositions and the edges are labeled by logic values The algebra used to encode the model is also specified explicitly In this section we describe how a model is encoded See Section 3 2 for algebra encoding This input format has been designed for automated generation not direct user manipulation A model encoding is divided into four parts e Namespace declaration Link to logic used to encode the model e Nodes one node tag per model state Nodes must have unique identifiers within the model A node can be defined as initial by adding the following attribute to the node tag xbel initial true The node tag has nested lt att r gt tags one for each model variable These attr tags define the state e Edges one edge tag per model transition The nested attr tag defines the logic value of the transition Basic structure of a model file lt gxl xmlns xbel www cs toronto edu xbel xmlns xlink xlink graph ID user defined edgemode directed gt lt LINK TO LOGIC gt lt xbel logic xlink type simple xlink href link to logic used to encode model MODEL lt NODES gt lt 1 one node tag per model state gt lt interpreted as node id model variablel logic value amp model variable2 logic value amp amp model variable n logic value gt node ID node_idl gt lt one attr tag per model varia
26. nge the value This directory will be used as the base directory by XChek for loading model files CTL file Picker use Browse button to change the value This directory will be used as the base directory by XChek for loading CTL history files Default CTL file use Browse button to change the value This CTL history file will be loaded by default when XChek is started Startup with Counter Example checking this box will ensure that the Produce counter example box E4 in the Main window is checked when XChek is started Enable Fairness checking this box will ensure that the Use fairness box D1 in the Main window is checked when XChek is started New experimental Cex Viewer this option switches between the two available counterexample viewers If checked the new counterexample viewer will be used if the Produce counter example box E4 is checked in the Main window Enable double buffering Remote X checking this box will enable double buffering This is recommended when running XChek remotely 24 Grappa Grappa is Java front end to dot Used to show counterexamples Path to DOT engine use the Browse button to specify the path to dot executable dot is used to make hierarchical or layered drawings of directed graphs and is usually available by default in many linux distributions nowdays If dot is not installed in your system install the graphviz package e KegTree KegTree is another way of presenting counter
27. ns Compiled in 0 195s loaded Model Checking AG pcl 3 amp pc2 3 gt y1 AG 1 3 A 2 3 gt yl Done in 0 024s Result is T Fairness Macros Use fairness Fairness conditions to be used O Selected Remove Produce counter example CTLIAG 3 gt yl v Figure 5 3 Vacuity Detection main window after checking 1 File Model Fairness CTL history Help 3 Model fairness B fairness B en lt gt Algebra Preferences 3 amp pc2 3 gt yl Output Options Compiled in 0 167s loaded Model Checking AG amp pc2 3 gt y1 pc2 3 gt yl Done in 0 029s Result is M Model Checking AG 1 3 amp M gt y1 1 gt yl Done 0 0275 Result is Model Checking AG 1 3 amp pc2 3 gt M AG pcl 3 2 3 gt Done 0 00905 Result is Fairness Macros Use fairness Fairness conditions to be used Selected Produce counter example CTL AG 3 gt v Figure 5 4 Vacuity Detection main window showing vacuity detection resu
28. ok and M Chechik Framework for Multi Valued Reasoning over Inconsistent View points In Proceedings of International Conference on Software Engineering ICSE 01 pages 411 420 Toronto Canada May 2001 IEEE Computer Society Press A Gurfinkel and M Chechik Generating Counterexamples for Multi Valued Model Checking In Proceedings of Formal Methods Europe FME 03 volume 2805 of LNCS pages 503 521 Pisa Italy September 2003 Springer A Gurfinkel and M Chechik Proof like Counterexamples In Proceedings of 9th International Confer ence on Tools and Algorithms for the Construction and Analysis of Systems TACAS 03 volume 2619 of LNCS pages 160 175 Warsaw Poland April 2003 Springer A Gurfinkel and M Chechik How Vacuous Is Vacuous In Proceedings of TACAS 04 volume 2988 of LNCS pages 451 466 March 2004 A Gurfinkel and M Chechik YASM Model Checking Software with Belnap Logic Technical Report 533 University of Toronto April 2005 A Gurfinkel M Chechik and B Devereux Temporal Logic Query Checking A Tool for Model Explo ration IEEE Transactions on Software Engineering 29 10 898 914 October 2003 A Gurfinkel Multi Valued Symbolic Model Checking Fairness Counter Examples Running Time Master s thesis University of Toronto Department of Computer Science October 2002 H Rasiowa An Algebraic Approach to Non Classical Logics Studies in Logic and the Foundations of Mathematics
29. ons to be used Selected qf Add Edit Remove Trace iv Produce counter example state Searching gt EF state Ready AG state Searching gt EF state Ready EF state Canceled AG AF state Canceled AG AF state Canceling Figure 4 5 Drop down menu created by loading a CTL history file At any moment new properties can be added to the drop down menu by typing them into the CTL input box A list of properties can be saved to disk by pressing the save CTL button The user will be prompted for the location of the save file 4 3 Counterexamples If a property is checked when the Produce counter example box is ticked XChek will produce a counterexample or witness for the property This counterexample will be shown using one of the available counterexample viewers which permit the interactive exploration and visualization of counterexamples These counterexamples are generated using proof rules GC03b The default counterexample viewer seen in Fig 4 6 can show the counterexamples using different tools with or without proofs This viewer also offers a state based view of the counterexample When XChek is configured to use this counterexample viewer proofs are generated prior to viewing When a proof step is selected the equivalent model state is shown When the Grappa and KegTree preferences are set the counterexample can
30. ory file E2 Run runs XChek checking the property selected in the input box w r t the last model loaded Results will be displayed in the main output area C E3 Trace for simulation purposes Not functional in this version E4 Produce counter example when this box is ticked Run will also produce a counterexample for the property being checked The manner in which this counterexample is shown depends on the user s preferences 4 1 Loading a model To load a model press the Model button The Pick a compiler window should appear see Fig 4 2 17 xchek File Model Fairness CTL history Help Model 2 fairness E fairness d CTL B Algebra Preferences Output Options Faimess Macros C Use fairness Pick a model compiler Fairness conditions to be used GCLang Compiler All XMLXKripkeModelCompiler O Selected SMV Model Compiler Flat Cancel Add Edit Remove Import Export Edit Remove Produce counter example Figure 4 2 The Pick a compiler window As discussed in Chapter 3 XChek supports SMV GCLang and XML as input formats for models Thus the three corresponding compilers appear in this window 4 1 1 SMV and GCLang models SMV and GCLang models are loaded in the same way the only difference is the
31. ph ID 2 model example edgemode directed LINK TO LOGIC gt xbel logic xlink type simple xlink href examples xml 4val logic xml lt MODEL gt lt NODES gt node ID s0 xbel initial true gt attr type prop name p value TT gt attr type prop name q value TF attr type prop name r value FF node node ID s1 attr type prop name p value FT attr type prop name q value TT attr type prop name r value FF node node ID s2 attr type prop name p value TF attr type prop name q value FT attr type prop name r value TF gt node lt EDGES gt edge from s0 to sl attr name weight value TT gt lt edge gt edge from s0 to s2 10 attr name weight value TF edge edge from sl to s1 attr name weight value TT gt lt edge gt edge from s2 to s0 attr name weight value ITT edge edge from s2 to sl attr name weight value TF edge graph gxl An explanation of the various items in the model encoding file 1 2 GXL namespace declaration the graph is directed and its id is model example 4 location of the logic used to encode the model 6 21 state definitions For example lines 7 11 define state 50 Note that this is
32. s type of language statements have guards The guard is a proposition which must be true before the statement is executed If the guard is false the statement will not be executed GCLang models are divided into four parts e NAME model name e VAR variable declaration block e INIT variable initialization block e RULES guarded commands that specify the behavior of the model The GCLang syntax accepted by XChek is the following grouped by part NAME start main model structure NAME varname varBlock initBlock rulesBlock varname is the model s name varBlock variable declaration block VAR varDecl varDecl varname type e g p10 boolean type boolean textSet textSet textOrNumberValued textOrNumberValued J textOrNumberValued varname number varname atom atom number digit 91916 atom tess Pa oheh p AT EAE YS Gat stet tu uten comer imo RESON rer p eite digit et OF INIT initBlock variable initialization INIT expr expr implExpr initialize using an expression setExpr initialize using a set setExpr setElement setElement setElement sets contain text or numbers textOrNumber textOrNumber varname number implExpr basicExpr implExpr implExpr implExpr implExpr implExpr implExpr amp implExpr rir implExpr implExpr implExpr implExpr
33. sed AG x state gt EF state Ready All Done in 1 858s D Selected Solution 1 is x state state Initial V state Ready V state Searching v Produce counter example CTL x state gt EFGtate Ready Figure 5 5 Query Checking window showing query checking results 31 Bibliography 02 CDEG03 CDG02 CGD 06 CGP99 EC01 GC03a GC03b GC04 GCOS GCD03 Gur02 Ras78 Som01 A Cimatti E M Clarke E Giunchiglia F Giunchiglia M Pistore M Roveri R Sebastiani and A Tac chella NUSMV 2 An OpenSource Tool for Symbolic Model Checking In Proceedings of CAV 02 volume 2404 of LNCS pages 359 364 2002 M Chechik B Devereux S Easterbrook and A Gurfinkel Multi Valued Symbolic Model Checking ACM Transactions on Software Engineering and Methodology 12 4 1 38 October 2003 M Chechik B Devereux and A Gurfinkel XChek A Multi Valued Model Checker In Proceedings of 14th International Conference on Computer Aided Verification CAV 02 volume 2404 of LNCS pages 505 509 Copenhagen Denmark July 2002 Springer M Chechik A Gurfinkel B Devereux A Lai and S Easterbrook Symbolic Data Structures for Multi Valued Model Checking Formal Methods in System Design 29 3 2006 E Clarke O Grumberg and D Peled Model Checking MIT Press 1999 S Easterbro
34. sical 2 valued model checking Model examples gclang trip trip planning5 gc 1 2 Main window press the Model button Pick a compiler window choose the GCLang Compiler Options window e Model Checking Algebra 2 e GCLang file examples gclang trip trip planning5 gc e MvSet Implementation mdd Options window press OK when options have been set The Main window should look like the one in Fig 5 1 if the steps uptil now have been followed correctly CTL input box type in the following property AG state Searching gt EF state Ready Optional Check the Produce counter example box to produce a counterexample for this property Press Run The Main window should now look like the one in Fig 5 2 If the Produce counter example box is checked the result is shown in a separate window as described in Section 4 3 27 File Model Fairness CTL history Help Model fairness 9 fairness E lt gt algebra Preferences 2 Output Options Compiled in 0 58s Fairness Macros loaded Use fairness Fairness conditions to be used all Selected Remove Produce counter example v Figure 5 1 Model Checking main window after successfully loading the model File Model Fairness history Help
35. te AX ctlExpr forall next state EF ctlExpr exists finally AF ctlExpr forall finally EG ctlExpr exists globally AG ctlExpr forall globally E ctlExpr exists until A ctlExpr forall until E ctlExpr exists weak until A ctlExpr forall weak until E ctlExpr exists release A ctlExpr forall release basicExpr atomic placeholder ctlExpr atomic identifier number placeholder atomic atomicSet atomicSet atomic atomic identifier alpha _ alpha number digit digit alpha digit Note Usual precedence rules apply EXAMPLES e EF CC Cruise amp Throttle ThrottleMaintain Model checking property CC and Throttle are model variables in a flattened SMV model and Cruise and ThrottleMaintain are possible values of these variables See Section 5 1 for an example of how model checking is done in XChek e AG connected A connected U offhook AG connected 14 Model checking property connected offhook are variables of a 4 valued model logic shown in Fig 3 2 i e these varibles can take the following values TT TF FT FF See Section 5 1 for an example of how model checking is done in XChek amp 2 3 gt yl Using Kleene logic in the property for vacuity checking This is a property for the GCLang version of the Peter son mutual exclusion algorithm given in Section 3 1 2 See Gurfinkel
36. utorial 5 1 Mod l Checking RM WEE EUR Pe eee MEU OE eee 5 2 NVacunty Detectioni 8 eR Ou SERERE GR AGERETUR eS E VETUS 5 3 Query Checking cc tee 5 Ad a Ru Pr Ede ep B 16 17 18 20 20 21 23 Chapter 1 Introduction XChek is a multi valued symbolic model checker 02 It is a generalization of an existing symbolic model checking algorithm to an algorithm for a multi valued extension of CTL XCTL Given a system and a XCTL property XChek returns the degree to which the system satisfies the property By multi valued logic we mean a logic whose values form a finite quasi boolean distributive lattice The meet and join operations of the lattice are interpreted as the logical and and or respectively The negation is given by a lattice dual automorphism with period 2 ensuring the preservation of involution of negation and De Morgan laws Multi valued model checking generalizes classical model checking and is useful for analyzing models where there is uncertainty e g missing information or inconsistency e g disagreement between different views Multi valued logics support the explicit modeling of uncertainty and disagreement by providing additional truth values in the logic XChek works for any member of a large class of multi valued logics It s model of computations is based on a generalization of Kripke structures where both atomic propositions and transitions between states
Download Pdf Manuals
Related Search