Home

Quest UserGuide - Software and Systems Engineering

1. F Huber and B Schatz Rapid Prototyping with AutoFocus In A Wolisz I Schieferdecker and A Rennoch editors Formale Beschreibungstechniken fiir verteilte Systeme GI ITG Fachge spr ch 1997 pp 343 352 GMD Verlag St Augustin 1997 F Huber B Schatz and G Einert Consistent graphical specifi cation of distributed systems In FME 97 4th International Sym posium of Formal Methods Europe LNCS 1313 pages 122 141 1997 M P Jones An Introduction to Gofer August 1993 Koob Baur Reif and Stephan VSE II Development Method 1998 R P Kurshan Reducibility in analysis of coordination In Kurzhanski Varaiya editor Discrete Event Systems Models and Applications volume 103 of Lecture Notes in Control and Infor mation Science pages 19 39 Springer Verlag 1987 C Loiseaux S Graf J Sifakis A Bouajjani and S Bensalem Property preserving abstractions for the verification of concurrent systems Formal Methods in System Design 6 1 11 44 1995 Stephan Merz Rules for abstraction In R K Shyamasundar and K Ueda editors Advances in Computing Science ASIAN 97 volume 1345 of Lecture Notes in Computer Science pages 32 45 Kathmandu Nepal December 1997 Springer Verlag Olaf M ller and Tobias Nipkow Combining model checking and deduction for I O automata In Proc Ist Workshop Tools and Al gorithms for the Construction and Analysis of Systems volume 1019 of Lecture Notes in Computer S
2. Figure 21 Banking System with two components means that the compute phase is active For the communication with the sched ulers the shared inout variables sync_Connectionl and sync Central and the in variables phase Connectionl and phase Central are used The sync variables are set to BSync and ESync from the schedulers and are reset to Ok by the barrier With BSync and ESync a scheduler signals that it wants to begin a new synchronization phase or that it wants to end its current phase In the barrier this leads to the execution of the appropriate action Begin Sync and EndSync Note that the BeginSync action is guarded by phase ph which means that the global phase must be the same as the phase which the scheduled component wants to enter The Sync and the SyncAll actions are only abbreviations used to make the code more compact BASIC AF Sync tsync BSync ESync InitSync Ok BASICEND AutoFocus Barrier for BankingSystem XIT TLSPEC BankingSystem0 Barrier PURPOSE AutoFocus Barrier for 48 Component BankingSystem0 USING Boolean Natural AF_Sync DATA SHARED INOUT sync_Connectionl tsync IN phase_Connectionl bool SHARED INOUT sync_Central tsync IN phase_Central bool INTERNAL compCounter nat INTERNAL phase bool ACTIONS BeginSync ph IN bool phase ph AND UNCHANGED compCounter phase EndSync IF compCounter 1 THEN phase phase AND compCounter 2
3. SPEC AFi ControlState sWaiting AND store NoMoney AND Tin Channel Info ChannelBase NoVal AND AFi Tin Channel Info ChannelBase NoVal AND Answer Channel Message ChannelBase NoVal AND AFi Answer Channel Message ChannelBase NoVal TLSPECEND 8 2 3 DTD In this section we describe the translation of data types and functions from the Quest language see Section 3 to the VSE II specification language Furthermore we describe the translation of properties to VSE Since data types and functions are executable within Quest we translated using the executable parts of VSE II Some concepts like pattern matching or pa rameterization are different between Quest and VSE and therefore they cannot be translated directly In this section we explain the principle translation scheme and the translation the special constructs We explain the translation algorithms by means of examples The translation of identifiers is as directly as possible i e if the translated function is no VSE keyword it is used for the translation For VSE keywords similar names are generated however these generated identifiers are retranslated directly For a 66 round trip engineering the VSE keywords should therefore be avoided Translation of Simple Data Types A simple data type in Quest has no type arguments like List a An example for a simple data type is data Nat Zero Succ pred Nat Simple data types are translated into BA
4. ELSE compCounter compCounter 1 AND UNCHANGED phase EX Sync s OUT tsync ph IN bool sl OUT tsync s BSync AND BeginSync ph AND s Ok OR s ESync AND EndSync AND s Ok AND UNCHANGED s1 SyncAll Sync sync Connectionl phase Connectionl sync Central OR Sync sync Central phase Central sync Connectionl 49 SPEC INITIAL compCounter 2 AND phase T ComputePhase AND sync_Connectionl InitSync AND sync_Central InitSync TRANSITIONS SyncAll compCounter phase sync_Connectionl sync_Central FAIRNESS WF SyncAll compCounter phase sync_Connectionl sync_Central HIDE compCounter phase TLSPECEND Next the scheduler for the component Connectionl and the component it self is shown In this example there are two separate TLSPECs but these two could also be merged to one component see Section 5 2 2 and the notes on useinclude In the scheduler Connectionl_Scheduler it can be seen that the description of the component Connect ionl is included The scheduler has an out variable schedulePhase which presents the value of the current phase i e T compute or F copy Also a shared inout variable sync is used for the communication with the global barrier The scheduler has three actions WaitOk Copy and Compute The WaitOk action waits for an Ok signal on sync which can only be set from the barrier The Copy and the Compute ac tion are executed in the appro
5. gt SensorSig Signal2Signal Signal gt Signal VARS variables for function Int2SensorSig Vlint2SensorSig Int variables for function Signal2Signal ViSignal2Signal Signal EINE em Int cSignal Signal AXIOMS axiom for the function Int2SensorSig fun Int2SensorSig x S00 ky FOR Int2SensorSig DEFFUNC Int2SensorSig VlInt2SensorSig S00 axiom for the function Signal2Signal fun Signal2Signal x x nr FOR Signal2Signal DEFFUNC Signal2Signal V1Signal2Signal VlSignal2Signal THEORYEND The corectness condition of the abstraction function with respect to the selected properties the strengthening is 93 THEORY OpenBarrier_Strengthen_Property USING OpenBarrier_Strengthen_Definition VARS IntIWL Int IntOwL Int l Int AXIOMS Strengthening for Property Concrete Val Comparator Combine Concrete IntOWL lt Val Comparator Combine Concrete IntIWL gt lt gt Comparator Combine Concrete OPENDif Present Abstract Val Comparator Combine Abstract OWL lt lt Val Comparator Combine Abstract IWL gt Comparator Combine Abstract OPENOK Present ur Int2SensorSig IntOWL lt lt Int2SensorSig IntIWL gt IntOWL lt IntIWL AND Signal2Signal OPENDif Present gt OPENDif Present
6. we distinguish the following test bases e component interfaces i e specifications with SSDs and DTDs e components with behavior i e SSDs STDs and DTDs e function definitions DTDs e sequence diagrams EETs In the following sections we discuss the specific test creation methods depending on the given test basis The central component is the test automaton The test au tomaton is a temporary automaton that is used in the testing process It represents the behavior or at least a part of the behavior of the test object During the test case generation process the tester works with the test automaton Quest s testing en vironments allows you to adapt the test automaton in a systematic way to resolve the needs for the software testing process This task is supported by the classifi cation tree editor CTE from DaimlerChrysler Finally the tester can derive test sequences from the test automaton which will be displayed as sequence diagrams Depending on the test automaton the resulting sequence diagrams include the expected responses or not If they do not include results either a reference im plementation is needed to produce the results or the tester can complement them manually 9 2 1 Test Basis SSDs The System Structure Diagrams in particular include the interfaces of the compo nents described by the specification These interfaces are a good starting point for test case generation The test case generation from component int
7. 7 Then the following steps are performed 26 Figure 7 VSE Import Quest 1 If the current VSE repository is no new one i e it is already saved in a gti file then the user can choose to create a new empty project a If Yes is selected then a new project with the name noname will be created and used b If No is selected then the state of the current project will be saved to tmp quest bck and all changes will be made to the current project 2 The AUTOFOCUS Quest repository can be chosen with the file browser de fault suffix is out a Choose b Choose Ok to import the file Cancel to cancel the import operation 3 The AUTOFOCUS Quest repository will now be read All actions particu larly error messages will be stored in a log file Quest log in the start directory 4 If errors occurred during the import and the import is done in an existing VSE repository then the user can choose to restore the previous version Some notes on VSE internals 27 Import of new nodes If no node with the representation of a specification exists then a new node with the appropriate name class will be created The initial node attributes are set like in a normal ASCII import in particular Checked No Change of existing nodes If an existing specification will be imported the sta tus information of the node and dependent nodes will be
8. FOR AbsStates DEFFUNC AbsStates Conc IF Conc Concrete_States sMain THEN Abstract_States sMAIN FI THEORYEND C 2 Homomorphosm Proof Obligation To express the proof obligation that ensures that the abstraction function is an homomorphosm within VSE II we use the follwoing theory correctness of the abstraction function TLSPEC OpenBarrier_AbsState_Correctness INCLUDE Conc Concrete Abs Abstract SATISFIES OpenBarrier_AbsState_Property TLSPECEND The important proof obligation is in the follwoing theory TLSPEC OpenBarrier_AbsState_Property USING OpenBarrier_AbsState_Definition INCLUDE Conc Concrete Abs Abstract VARS Conc tConcrete_States MI oe Int SPEC ALL Conc ConcInitial Conc gt AbsInitial AbsStates Conc correctness for transition owl openDifference lt iwl IntIWL iwl IntOWL owl OPENDif Present ALL Vl lt gt Conc AFi ControlState Conc Concrete States sMain AND Vl Conc l gt Conc AFi_ControlState Conc Concrete_States sMain AND 91 Channel_Int ChannelBase is_Msg IntIWL AND Channel_Int ChannelBase is_Msg IntOWL AND Channel_Int ChannelBase Val IntOWL openDif ference lt Channel Int ChannelBase Val IntIWL AND Conc AFi ControlState Conc Concrete States sMain gt AbsStates Conc AFi ControlState AbsStates Conc Concrete_States sMain AND Channel_SensorSig Chan
9. e less lt 3 e less or equal lt 3 19 e multiplication 41 e division 41 Note that multiplication and division cannot be translated to SATO see Wim00 4 Using the Model Browser The model browser of the Quest development environment is the starting point for all verification and testing activities It enables you to e load a repository e view the repository e edit the repository in a limited way and e start the verification and testing tasks 4 1 Starting the browser The browser does automatically come up when you start the Quest development environment This is done by typing startQuest from a command shell See Section A for further details on the installation 4 2 Working with repositories With the Files menu in the menubar you can open close save and import the repository 20 Open a repository There are two ways to open a repository When opening a repository an optional type check can be performed If you want to leave out the type check use open repository fast to open the repository After the repository is loaded the repository name and all projects will be displayed in the browser If you load the repository with open repository check all terms in your model will also be type checked while the repository is loaded Use this if you want to type check the model Type checking the model especially the transitions of STDs cannot be performed in AUTOFOCUS If you are currently working
10. editing nodes 44 Creating new nodes ck o coc a X ox Ox R9 X X Ro E 25 Deleting nod s xod a ESM Rd x Ee RE ES Integration 5l Integration im AUTOFOCUS o o d 5 1 1 Exporting Projects from AUTOFOCUS 22 sss ss 5 1 2 Importing Projects in AUTOFOCUS LLI TS Loo ee X we Re eR EE Re 32 Willen VSE sese ho eee er S UR EA Sd OWERVIEW 2 2 22999594 x R4 bx be 24 5 2 2 Importing Projects in VSE S44 3 482 20 5 2 3 Exporting Projects from VSE 64 gt 28 Limitations e e hos acq ber eq RRS EE S Model Checking with AUTOFOCUS Ep TIO uc usu ouo xc XC AOR ORD OR Roe aro 64 Counter Examples o ccor ew x x RA XO RS 6 3 Connected Checkers 6542s voa o yo oO RR oor ea 03d MORON C Dou Using SATO oorge semear Rex Re 29 cR OE KS 7 Abstraction Chooser 20 20 20 21 21 22 22 22 22 22 22 23 23 24 28 31 31 31 33 33 33 35 35 TA Methodology ax scs sw saw Od HH FOE KR OM RS 7 2 Abstraction Example Comparator 7 3 Using the Abstraction Chooser 2 Connection to VSE BO Introducti n Le ace aces rda EK OR ORK HER EO ES 8 2 Translation from AUTOFOCUS to VSE Be DoD a Sh be hee heh eh ee ee ker Bs SED en ROSA HR a ER RE fd B3 DTD 52253 WR hee aaa haha 8 3 Translation from VSE to AUTOFOCUS BE 1 eRe Sw eR em Rex ROROE HSH en ite En ak ee ea ee ee d erh c DID a nee Oe ew ea The Test Env
11. name c the model with cpp macros not always generated 3 name smv the model with expanded macros 4 name counter the result of SMV with counter examples where name is the name of the model concatenated with the name of the checked component 6 3 2 Using SATO SATO works completely automatic and does not generate intermediate files 7 Abstraction Chooser Model checking is completely automatic but limited to systems of relatively small finite state space Theorem proving however is in a sense complementary it re quires user interaction but can deal with systems of arbitrary size Abstractions provide conditions that ensure the correctness of such simplifications and so ab straction techniques CGL92 LGS 95 GL93 M l98b Mer97 Kur87 DGG97 SLW95 Wol86 MN95 HS96 promise to combine the advantages of both ap proaches Within the project Quest we decided to support abstractions related to certain properties this gives us a very powerful tool for reducing complex sys tems to their critical core First we will propose a customized abstraction methodology for the context of Quest Then we describe tool support for defining abstractions see Section 7 3 In Section 7 2 we present an example and the resulting proof obligations 7 1 Methodology The general idea of abstraction is depicted in Fig 12 in a first step the original system C is reduced to a smaller model A If C is large or infinite this step will in gene
12. recomputed from the original state and the kind of the change Original state Action Unchecked the node will be changed without a request Checked the node will be changed without a re quest the node and dependent nodes become Unchecked Invalid the node will be changed without a re quest the node and dependent nodes become Unchecked Suspended Verified the node will be type checked automatically and if necessary a warning with the possibil ity to cancel the action will be shown If the warning is ignored dependent nodes become Unchecked or Invalid In Veri fication the node won t be changed This may lead to inconsistencies because then parts of a AUTOFOCUS specification are imported and other parts aren t 5 2 3 Exporting Projects from VSE If you want to export a project or parts of a project from VSE and reimport it to Quest you have to select the appropriate VSE objects and you must choose Ex port from the File menu of the VSE main window Note that the retranslation to AUTOFOCUS Quest can be started with Call Transformer from the VSE main window see 9 automatically After that the resulting specification can be read from the Quest tools or from AUTOFOCUS Selection Before the export to Quest can be started the VSE development ob jects which should be exported have to be selected To select some nodes you have to double click on a node and to choose a selection operat
13. the abstract component from an abstraction function and 2 to define the abstraction function between a concrete and an abstract model In Quest up to now only the second way is supported because designers mostly have the abstract model in mind and want to find a homomorphism between the concrete and the abstract one Defining such an abstraction function in general is more difficult due to the consistency conditions and therefore Quest supports difficult task with the abstraction chooser The feature of computing abstraction functions is future work To select the abstract component for the abstraction the abstraction chooser shows all components in the system see Figure 16 This requires that both components the concrete and the abstract are specified within one SSD Abstraction Chooser OX Choose an abstract Component press Select for Abstract Concrete B Select for Abstraction E Abstract RR a a J Figure 16 Selecting the Abstract Component 41 After the selection of the abstract component all elements Variables Ports Types that can be related are defined and the definition window of the abstraction chooser appears see Figure 17 It suggests an order for the definition of the abstraction functions but allows for arbitrary orders as well Furthermore sugges tions are made that consider the previous definitions In Figure 17 the abstraction A AbstractionChooser ri m o Define Abstr
14. 0 Changing MaxInt MaxInt is an attribute of projects a project has to be selected The default value for MaxInt is 15 See Figure 10 for a changing of MaxInt Model checking and bounded model checking can be started for components and for projects Be careful with this selection since it can influence the truth of properties Checking a component includes all subcomponents but not the surrounding components Model checking evaluates all properties of the selected components Model checking assumes an arbitrary environment that sends arbi trary inputs to the checked component Therefore there can be counter examples that are no real counter examples i e that are not possible for the complete sys tem Just think of two components one generating the constant output true the other an identity component just passes boolean values A property of the iden tity component is that it does not sent always true however this is not the case in this example where only true arrives from the other component This effect can be exploited to reduce the search space of a system by providing an environment model for a system This will lead to faster checking results even if the number of components if bigger Experiments however have shown that a too detailed environment model increases the transition relation and thus can make checking more time consuming Since model checking and bounded model checking are of exp
15. 272 275 Berlin July 13 17 1997 Springer 98
16. 5On Unix systems the installer stores some information in the directory binor usr bin e g an uninstall program 8l st Setup program Figure 27 The welcome screen of the installer 82 lt a L wore __ NewDirectory MEM o i EES 1 E e usr local DIR Quest Figure 28 Choose a destination directory 83 7 If not already done the other programs like VSE II SMV CTE needed for the Quest tools have to be installed now and should be added to your path settings 8 If another user wants to run the Quest tools she he should expand her his path settings appropirate and she he have to copy the file quest to her his home directory A 3 Configuration Normally no further configuration of the Quest tools are needed All settings are done by the Quest setup program All user configurable settings are stored in the file quest A 4 Uninstallation To uninstall the Quest tools on Unix platforms follow those steps 1 Log in as the user who installed the Quest tools 2 Start the uninstall program juninst Quest Home UnInst 3 Follow the suggested steps After this you may remove juninst from your bin directory To uninstall the Quest tools on Windows platforms go to the Add Remove Pro grams dialog in the Windows Control Panel and remove the program B Case Studies and Examples In this section we present the examples case studies that have been modelled and checked within the
17. Central is a combination of those two components as the root component BankingSystem is a combina tion of Connectionl and Central Combine In components which are decomposed the ports are inlined in the TLSPEC of the Combine component In the Combine components all external variables are connected Beside the in and out variables for component ports like inp1 and inp the communication channels between the schedulers and the barriers are connected Combine for AutoFocus Component Central The port inp1 ofthe component Central is connected to the port inp of the subcomponent Driverl through the channel inp1 The names of the ports are not shown in Fig 22 53 TA TLSPEC Central Combine PURPOSE AutoFocus Combine for Component Central USING ImportDataTheories Natural AF Sync MAINCHANNEL DATA INTERNAL sync Driverl tsync INTERNAL sync Database tsync SHARED INOUT sync tsync OUT schedulePhase bool PortDeclarations IN inpl Channel Info ChannelBase Channelm IN ClAck Channel Signal ChannelBase Channelm OUT Answerl Channel Message ChannelBase Channelm COMBINE Central Barrier Central Barrier phase Central Combine schedulePhase Central Barrier phase Driverl lt Driverl Scheduler schedulePhase Central Barrier phase Database lt Database Scheduler schedulePhase SHARED Central Barrier upsync lt Central Combine syn
18. Edit gt Create Subnode Then you get a dialog that allows you to create the new subnode 4 5 Deleting nodes Nodes can also be deleted within the model browser Currently this functional ity is restricted to the deletion of transition nodes and EET nodes To delete a node first select the desired node and then click on Edit gt Delete Node Be aware that all subnodes i e the subtree of the selected node will also be deleted instantaneously 5 Integration 5 1 Integration in AUTOFOCUS 5 1 1 Exporting Projects from AUTOFOCUS You can export an AUTOFOCUS project by simply pressing Export Project gt Quest Format from the Projects menu in AUTOFOCUS and choosing a file name The exporter creates one file for model with the given file name and for each specified DTD module a special module file Note that all generated files have to be in the same directory to read or import the repository 5 1 2 Importing Projects in AUTOFOCUS Importing projects to AUTOFOCUS is as easy as exporting them Just click on Im port Project gt Quest Format inthe Projects menu and enter the file name that contains the model Pay attention that the corresponding DTD module files are located in the same directory as the model file 5 1 3 Limitations Due to limitations of the quest data structures and the AUTOFOCUS data structures some information gets lost when converting a project from Quest to AUTOFOCUS or vice versa The Quest export can not han
19. FOCUS Due to the differences in the interaction semantics synchronous asynchronous schedulers are generated for the representation of AUTOFOCUS models in VSE II see Section 8 1 In VSE II there are intermediate states that are not reachable in AUTOFOCUS Therefore AUTOFOCUS Quest properties hold only in these states and the properties have to be expanded This allows also for a translation of the next state relation The example of Section 3 5 the following property has been given FM99 BankingSystem Connectionl Answer NoMoney gt FM99 BankingSystem Connectionl CentralMsg NoMoney It is translated into the following VSE II specification 70 TLSPEC Connectionl_Properties INCLUDE PropertyBase Connectionl_Scheduler SPEC PropertyBase schedulePhase T AND PropertyBase schedulePhase F AND Channel_Message ChannelBase is_Msg PropertyBase AF_Component Answer AND Channel Message ChannelBase Val PropertyBase AF Component Answer NoMoney gt PropertyBase AF_Component CentralMsg Channel_Message ChannelBase Msg NoMoney TLSPECEND Again the patterns are eliminated as described for function definitions 8 3 Translation from VSE to AUTOFOCUS In this section the retranslation of VSE specifications to AUTOFOCUS Quest is discussed The retranslation of specifications is only suggestive for specification or parts of specifications which are generated by Quest This is due the f
20. NoVal CAck AND AFi Tin Channel Info ChannelBase Msg Channel Info ChannelBase Val Inp AND AFi Answer Channel Message ChannelBase Msg store AND UNCHANGED store Driving2Driving 2 AFi ControlState sDriving AND AFi ControlState sDriving ND Channel Info ChannelBase is NoVal Inp Channel Message ChannelBase is NoVal Tout Channel Signal ChannelBase is NoVal CAck AFi Answer Channel Message ChannelBase Msg store AFi Tin Channel Info ChannelBase NoVal z Z E EE B B 00000 Z 64 AND UNCHANGED store Driving2Waiting AFi_ControlState sDriving AND AFi_ControlState sWaiting AND Channel_Info ChannelBase is_Msg Inp AND Channel Signal ChannelBase is Msg CAck AND is Present Channel Signal ChannelBase Val CAck AND AFi Tin Channel Info ChannelBase Msg Channel Info ChannelBase Val Inp AND AFi Answer Channel Message ChannelBase NoVal AND UNCHANGED store Driving2Waiting 1 AFi ControlState sDriving AND AFi ControlState sWaiting AND Channel Info ChannelBase is NoVal Inp AND Channel Signal ChannelBase is Msg CAck AND is Present Channel Signal ChannelBase Val CAck AND AFi Tin Channel Info ChannelBase NoVal AND AFi Answer Channel Message ChannelBase NoVal AND UNCHANGED store IdleStep
21. OD END schedulePhase sync AF Component AFi ControlState store Tin AFi Tin Answer AFi Answer HIDE AF Component AFi ControlState store AF Component AFi Tin AF Component AFi Answer TLSPECEND BASIC Driverl States tDriverl States sWaiting sDriving BASICEND AutoFocus Component Driverl EN TLSPEC Driver PURPOSE AutoFocus Component Driverl USING Natural MAINBankSystem_Module_MESSAGE Driverl_States 62 DATA PortDeclarations IN Tout Channel_Message ChannelBase Channelm IN Inp Channel_Info ChannelBase Channelm IN CAck Channel_Signal ChannelBase Channelm OUT Tin Channel_Info ChannelBase Channelm OUT Answer Channel_Message ChannelBase Channelm PortDeclarations internal ports INTERNAL AFi_Tin Channel_Info ChannelBase Channelm INTERNAL AFi_Answer Channel_Message ChannelBase Channelm LocVariables INTERNAL store Message ControlState INTERNAL AFi_ControlState tDriverl_States ACTIONS CopyPorts Tin AFi_Tin AND Answer AFi_Answer AND UNCHANGED AFi_ControlState AFi_Tin AFi_Answer store Transitions Waiting2Driving AFi_ControlState sWaiting AND AFi_ControlState sDriving AND Channel_Info ChannelBase is_Msg Inp AND Channel_Message ChannelBase is_Msg Tout AND AFi_Tin Channel Info ChannelBase Msg Channel_Info ChannelBase Val Inp ND AFi_Answer Channel_Message Cha
22. Quest Users Guide Peter Braun Heiko L tzbeyer Oscar Slotosch Version 1 0 of March 7 2000 Abstract Within the project Quest several tools have been connected The central tool is AUTOFOCUS the connected tools are VSE SMV CTE and SATO Furthermore several parts a temporal specification language a selection tool a test driver and an abstraction chooser have been added to improve the integration of the tools and to support the development of correct soft ware Furthermore we describe some examples that have been used to test the quest tools Contents 1 Introduction 1 1 Conventions used in this manual 2 Views and Models of AUTOFOCUS 8 2 1 Structure of Views in AUTOFOCUS 24 Structure of the Models 22242 ed ma Rao Rx 9 3 The Language QuestF DTDs and Properties 11 3 1 Jupe Definitions 4 44 s ok a x e we ee we E S 12 32 TEMIS oo oe he Er a reed 14 33 Punchon D finitons uu uad ee 4 ee RR 14 24 Module Definitions uo dos x ooa ie a ats GO ae a 15 20 opel 5G hes haa Ee c RN rer her eS ERE a 16 3 6 Correctness Conditions 3 7 Integration and Application 2 su o RS 3 8 Predefined Elements 2 2222222412 422 koe Eee ES eel K oe ec OR ee A HM PRD a 392 qODGHIBON lt 2 hono barche WS OS RED ES EA Using the Model Browser 4 1 Starting the browser ko we ae x RR wR iii 4 2 Working with repositories sooo 0 0 o o os 4 3 Viewing and
23. SIC specifications Since data types in Quest have canonical discriminators is_Zero is_Succ these are also gen erated The resulting VSE specification is BASIC NatBase Nat Zero WITH is_Zero Succ pred Nat WITH is Succ BASICEND For every data definition one basic specification is generated Translation of Structured Data Types Structured data types are DTDs that import other DTDs see Figure 4 or data type definition that use data type def initions of the same DTD For example the DTD TRANSACTION of Appendix B 2 contains data Action SendMail Withdraw Int ViewBallance data Info TA Action account Int The translation of this structured specification to VSE II is BASIC ActionBase USING INTEGER Action SendMail WITH is SendMail Withdraw WithdrawSell Int WITH is Withdraw ViewBallance WITH is ViewBallance BASICEND BASIC InfoBase USING 67 ActionBase INTEGER Info TA TASell Action account Int WITH is_TA BASICEND This results into a more detailed structure of data types in VSE II compared with the structures of DTDs in Quest Translation of Function Definitions Functions can be defined in Quest using pattern matching Pattern matching is expanded using explicit case distinctions with the generated discriminator and selector functions This allows us to gen erate executable algorithms for functi
24. SSDs can be refined with SSDs states in STDs can be refined by STDs and components or boxes in EETs can be refined using EETs DTDs have an inclusion structure since each DTD can import other DTDs This leads to a graph structure instead of a tree structure however this is not yet imple mented within AUTOFOCUS Copy and paste has to be used to reuse DTDs The association that relate views of different kinds cannot be visualized in the browser of AUTOFOCUS Atomic components cannot be seen in the browser since it shows only the available documents The only visible association in the browser is the substructure association between views of the same kind Further associa tions for example the assignment of a STD to a component cannot be seen in the Project Document Options Tools Windows Help Projects Pedestrian Traffic Lights System mun Mm SSD en Light System S Facility m STD FH Controller Bj Automatic S Manual S ManualSwitch E Facility behavior R EET Facility m Traffic Light System S Manual Bi Automatic A Bj Automatic B TOC Light System hubert 10 Mar 98 Bj Facility huberf 10 Mar 98 B DTD B Figg us See 99 999 90909090909090909099090909090 0 Figure 2 The Browser of AUTOFOCUS browser of AUTOFOCUS 2 2 Structure of the Models QML has a model oriented structure The main models are components The model browser shows more details and attributes of the model than AUTOFOCUS does and in ad
25. THEORYEND again the fact that this condition is true is expresed in a theory witha SATISFIES section THEORY OpenBarrier_Strengthen_Correct USING OpenBarrier_Strengthen_Definition SATISFIES OpenBarrier_Strengthen_Property THEORYEND References BLSSO00 P Braun H L tzbeyer B Sch tz and O Slotosch Consistent Integration of Formal Methods In Tools for the Analysis of Correct Systems TACAS 2000 to appear 94 BS99 CGL92 DGG97 Gie99 GL93 GWG95 Ham98 Ham99 HEea96 HMR 98 M Broy and O Slotosch Enriching the Software Development Process by Formal Methods In Current Trends in Applied Formal Methods 98 LNCS 1641 1999 Edmund M Clarke Orna Grumberg and David E Long Model checking and abstraction In Proc 19th ACM Symp Principles of Programming Languages pages 343 354 ACM Press 1992 Dennis Dams Orna Grumberg and Rob Gerth Abstract interpre tation of reactive systems ACM Transactions on Programming Languages and Systems 19 2 22 43 1997 P Gierl Casestudy The Oostershelde NSS 1999 Fortgeschritte nenpraktikum Technische Universit t M nchen Susanne Graf and Claire Loiseaux A tool for symbolic pro gram verification and abstraction In C Courcoubetis editor 3th Int Conf on Computer Aided Verification volume 697 of Lecture Notes in Computer Science pages 71 84 Springer Verlag 1993 M Grochtmann J Wegner and K Gri
26. UNCHANGED AFi ControlState Tin Answer AND NOT Channel Info ChannelBase is Msg Inp AND Channel Message ChannelBase is Msg Tout AND NOT Channel Info ChannelBase is Msg Inp AND NOT Channel Info ChannelBase is NoVal Inp AND Channel Message ChannelBase is Msg Tout AND NOT Channel Info ChannelBase is Msg Inp AND Channel Message ChannelBase is Msg Tout AND Channel Signal ChannelBase is NoVal CAck AND NOT Channel Info ChannelBase is Msg Inp AND Channel Message ChannelBase is NoVal Tout AND Channel Signal ChannelBase is NoVal CAck AND NOT Channel Info ChannelBase is NoVal Inp AND Channel Message ChannelBase is NoVal Tout AND Channel Signal ChannelBase is NoVal CAck AND NOT Channel Info ChannelBase is Msg Inp AND Channel Signal ChannelBase is Msg CAck AND is Present Channel Signal ChannelBase Val CAck AND NOT Channel Info ChannelBase is NoVal Inp AND Channel Signal ChannelBase is Msg CAck AND is Present Channel Signal ChannelBase Val CAck 65 set output ports to NoVal AND AFi_Tin Channel_Info ChannelBase NoVal AND AFi_Answer Channel_Message ChannelBase NoVal local variables stay unchanged AND UNCHANGED store NextStep Waiting2Driving OR Waiting2Waiting OR Waiting2Driving 1 OR Driving2Driving OR Driving2Driving 1 OR Driving2Driving 2 OR Driving2Waiting OR Driving2Waiting 1 OR IdleStep AND UNCHANGED Tin Answer
27. act that AUTOFOCUS Quest is based on a synchronous execution model while VSE II uses an asynchronous interleaving semantic Up to now there is no useful pre sentation of such specifications in AUTOFOCUS Quest So it is only possible to retranslate specifications which are structured like shown in Section 8 2 So usually a specification of a system is started in AUTOFOCUS Quest and trans lated to VSE II later if some properties have to be shown In VSE II the specifica tion could be modified but if it or parts of it should be retranslated the structure of the specification should follow the structure of the generated constructs Usually only the behavior of a component will be changed 8 3 1 SSD For the retranslation of SSDs only the following parts are recognized 71 Location Specification part Combine Component components and SSDs Scheduler Component local variables i e internal variables except those beginning with AFi_ Component initial values of local variables Component Combine in and out variables which are retranslated to in and out ports Combine channels The structure of the SSDs will be the same as those used by the translation All view informations e g positions of the drawn rectangles and so on are lost It is not checked if the scheduling algorithms fit to those used by the translation i e the internal specification of the barriers and the scheduler
28. actions Main MAIN Figure 17 Definition Window of Abstraction Chooser chooser suggests to map the concrete state Main to the abstract state MAIN In this example this is the only possible choice and pressing Define defines the abstraction function for states After the definition of the mapping between lo cal variables in the example there is also no choice the chooser tries to make a suggestion for the abstraction of types that matches to the abstracted types of the ports see Figure 18 If there are inconsistencies for example if the type of a A AbstractionChooser D 109 Define Abstractions Concrete Type Name Abstract Type Name Int i Figure 18 Selecting the Abstract Types function abstraction does not match the type define for local variables the error 42 is reported and the inconsistent fields are marked with red colors in the definition window see Figure 19 i AbstractionChooser sp Define Abstractions gig ve riables Concrete Variable Abstract Variable Properties SensorSig Figure 19 Inconsistencies are marked with red color The functions that map the values of the concrete type to the abstract in our case Int2SensorSig are defined in the Functions window of the chooser that allows to enter a text that defines the abstraction function Pattern matching for abstraction functions is not supported in this version An imp
29. ankingSystem0_Combine sync_Central Connectionl_Scheduler Connectionl_Scheduler AF_Component Answer lt Central_Combine Answerl SHARED Connectionl_Scheduler sync lt BankingSystem0_Combine sync_Connectionl Central_Combine Central_Combine inpl lt Connectionl_Scheduler AF_Component inp Central_Combine ClAck lt Connectionl_Scheduler AF_Component CAck SHARED Central_Combine sync lt BankingSystem0_Combine sync_Central HIDE BankingSystem0_Combine sync_Connectionl BankingSystem0_Combine sync_Central TLSPECEND As we use a hierarchic barrier synchronization algorithm the component Cen tral has its own barrier This barrier communicates with the global barrier like 56 a normal scheduler It acts to the local schedulers like the global barrier But internally it differs from the global barrier It has an additional internal variable endcomp which is T when all of its scheduled components have performed their step and the barrier itself signals the end of its step to his super barrier In contrast to the root barrier which only performs synchronize with their super barriers So schedulers AutoFocus Barrier for Centr Xf TLSPEC Central Barrier PURPOSE AutoFocus Barrier f USING Boolean Natural AF S DATA HARED INOUT sync Driverl phase Driverl bool HARED INOUT sync Database IN phase Database bool INTERNAL compCounter nat INTERNAL endcomp bool OUT phase
30. bool ARED INOUT upsync SE tsyn ACTIONS BeginSync ph phase ph AND UNCHANGED compCounte IN bool EndSync IF compCounter phase phase AND compCounter AND endcomp T AND UNCHANGED upsync ELSE 1 THEN 2 SyncAll actions sub barriers have to they have a TRANSITIONS section like al or Component Central ync tsync tsync C r phase endcomp upsync 57 compCounter compCounter 1 AND UNCHANGED phase endcomp upsync FI WaitOk upsync ok AND endcomp F AND UNCHANGED compCounter phase upsync sync_Driverl sync_Database Sync s OUT tsync ph IN bool sl OUT tsync s BSync AND BeginSync ph AND s Ok OR s ESync AND EndSync AND s Ok AND UNCHANGED s1 SyncAll Sync syno Driverl phase Driverl sync Database OR Sync sync Database phase Database sync Driverl SPEC INITIAL BEGIN compCounter 2 endcomp F phase T ComputePhase sync_Driverl InitSync sync_Database InitSync END TRANSITIONS BEGIN WHILE TRUE DO upsync BSync WaitOk WHILE endcomp F DO SyncAll OD upsync ESync WaitOk OD END compCounter phase upsync endcomp sync Driverl sync Database 58 MAINBankSystem_Module_ MESSAGE MAINBankSystem Module MESSAGE Connectioni Scheduler EN A Connection En Connection States Connect
31. c Central Barrier sync Driverl lt Central Combine sync Driverl Central Barrier sync Database lt Central Combine sync Database 54 Driverl_Scheduler Driverl_Scheduler AF_Component inp lt Central_Combine inpl Driverl Scheduler AF Component CAck lt Central Combine ClAck Driverl Scheduler AF Component Answer Central Combine Answerl Driverl Scheduler AF Component Tout lt Database Scheduler AF Component Tlout SHARED Driverl Scheduler sync lt Central Combine sync Driverl Database Scheduler Database Scheduler AF Component Tlin Driverl Scheduler AF Component Tin SHARED Database Scheduler sync lt Central Combine sync Database HIDE Central Combine sync Driverl Central Combine syno Database TLSPECEND Combine for AutoFocus Component BankingSystem TLSPEC BankingSystem0 Combine PURPOSE AutoFocus Combine for Component BankingSystemO USING ImportDataTheories Natural AF Sync MAINCHANNEL 55 DATA INTERNAL sync_Connectionl tsync INTERNAL sync_Central tsync COMBINE BankingSystemO Barrier BankingSystem0_Barrier phase_Connectionl lt Connectionl_Scheduler schedulePhase BankingSystem0_Barrier phase_Central lt Central_Combine schedulePhase SHARED BankingSystem0_Barrier sync_Connectionl lt BankingSystem0_Combine sync_Connectionl BankingSystem0_Barrier sync_Central lt B
32. cheduler is similar to the scheduler of component Connectionl The compo nent Driver is included in the scheduler as AF Component The Compute action calls the Next Step action of the component This action performs one step of the automaton or if no transition is possible then the Id1eStep is taken The Copy action calls the CopyPorts action of the component which copies the values of the internal buffers to the out variables In Driverl_States the states of the automaton Waiting and Driving are defined These are used as values for the AFi ControlState which stores the current state of the automaton As described above besides the in and out variables of the component internal buffer variables for the out variables are de fined in the component for a description of the used channel type see Section 8 2 3 The result of a compute action is stored in their internal buffers so that they cannot be seen outside the component In the CopyPorts action these in ternal values are copied to the external out variables For every transition of the automaton an action which describes the transition is generated The action is named by the start state and the end state of a transition For hierarchical automa tons the transition segments are merged so that there is only one transition and so that the resulting automaton is flat In a transition first the control state is checked 60 and set appropriate and after this the precondition
33. cience pages 1 16 Springer Verlag 1995 96 M l98a M l98b Pau91 P1397 PS99 RSW97 Sad97 Sad98 SK97 S1098 SLW95 Olaf M ller A Verification Environment for I O Automata Based on Formalized Meta Theory PhD thesis Institut fiir Informatik Techn Univ Miinchen 1998 Olaf M ller A Verification Environment for I O Automata Based on Formalized Meta Theory PhD thesis Institut fiir Informatik Technische Universitat Miinchen 1998 L C Paulson ML for the Working Programmer Cambridge Uni versity Press 1991 T Plasa VSE II Benutzerhandbuch Grundsystem 1997 J Philipps and O Slotosch The Quest for Correct Systems Model Checking of Diagramms and Datatypes In Asia Pacific Software Engineering Conference 1999 1999 to appear G Rock W Stephan and A Wolpers Tool Support for the Compositional Development of Distributed Systems In Proc Formale Beschreibungstechniken f r verteilte Systeme GI ITG Fachgespr ch GMD Studien Nr 315 ISBN 3 88457 514 2 1997 S Sadeghipour Teststrategien auf Basis erweiterter endlicher Au tomaten 1997 Internes Papier S Sadeghipour Testing Cyclic Software Components of Reactive Systems on the Basis of Formal Specifications PhD thesis Tech nische Universit t Berlin Fachbereich Informatik 1998 S Sadeghipour and T Klein Testmethoden f ur formale graphis che Spezifikationen 1997 Internes Papier O Slot
34. component must be marked to read back the test cases from the CTE file The generated test automaton consists of a single state with one transition for each test case The transitions contain only the input values or the classes of input values determined by the CTE Concrete input data can be given in a later step see Section 9 2 5 Of course it is not possible to derive the desired outputs from the component s interface A reference implementation is needed to determine the outputs see Section 9 2 5 and 9 3 2 75 9 2 2 Test Basis SSD with STDs If the specification includes a behavior description the test case generation should include the given behavioral aspects in the generated test cases We will differen tiate the following two scenarios e one component with associated automaton unit test e several communicating components with associated automata integration test Unit Test The unit test tests a single component of the system Test cases are derived from the behavioral descripton of the component i e the associated STD Arbitrary STDs have not only a control state but also a data state This makes the test sequence generation more complicated If the data state of the automaton influences the change of the control state i e influences the ability of some tran sitions to fire not all transisition sequences are feasible Such automata should be transformed to simple automata where all transition sequences are feas
35. de the actual selection is shown The right panel is there only to control the current selection modifications always have to be done on the left side For maximal flexibility and usability there are two main selection modes The au tomatic selection mode tries to select always a complete consistent model while the user has maximal freedom in the manual selection mode First we describe the automatic selection mode 8Panels are windows which are contained in a real window 25 The automatic selection mode can be started by clicking on the toolbar button AutoSelect or by selecting the corresponding menu entry If the automatic selection mode is on the button AutoSelect is enlightened Automatic selection mode The component tree will be folded to the root com ponent If the root component has an automaton then it will be selected otherwise their subcomponents will be unfolded Again for each subcompo nent which has an automaton it will be selected Each subcomponent with out an behavior will be unfolded and so on So at the beginning the most abstract system with a complete behavioral description and the necessary data type definitions will be selected After this subtrees can be unfolded to get a more concrete selection A left mouse button click deletes the selec tion and starts the selection algorithm from the component on which was clicked A right mouse button click adds the selected compone
36. dition there are some attributes that are not present in AUTOFOCUS for example properties abstractions or an implementing code Every component can have subcomponents This reflects the hierarchy in AUTO Focus SSDs In contrast to the browser of AUTOFOCUS the STDs assigned to a component are also displayed see Fig 3 In the model browser the following model structures are displayed e Component with attributes Subcomponents Ports Automaton STD EET Project Edit Testing Verify Options Repository SingleAFRepository generated on Tue Jul 13 10 11 22 CEST 1999 Q Project Comparator Q Ei Component Combine 3 Port Intiwe 3 Port IntowL 3 Port Wwe 3 Port owL 3 Port OPENDit 3 Port OPENOK Q gs Component Concrete 3 Port Intiwe 3 Port IntowL 3 Port OPENDit Q e Automaton Compare1 State Compare State Main do TransitionSegment Main gt Main owl openDifference iwi ntlWL iwl IntOWL ow OP E NDif P resent Pre Condition owl openDifference X iwl In Input Int iwl In Input IntOWL owI Out Output OPENDIfIP resent E Property is Msg Zomparator Combine Concrete IntOWL amp amp Val Zomparator Combine Concrete IntOVWL Property is Msg Comparator Combine Concrete IntOWL amp amp val Comparator Combine Concrete IntOWL Property val Comparator Combine Concrete IntOWL 0 Property Val Comparator Cornbine Concrete IntlWL 0 w Abstraction Int2 Sensor
37. dle the following items 22 e refinement of axes in EETs i e sub EETs for axes e textual annotations of all objects e reuse of STDs in several components e STD documents which are not associated with an SSD document e combinations of input output statements that are delimieted with can not be exported use as delimiter Items that cannot be imported in AUTOFOCUS e all kinds of test data e properties e abstractions e java code Therefore when exporting an AUTOFOCUS projects to the Quest format and reim porting it again in AUTOFOCUS you will automatically loose the refinement of axes in EETs 5 2 Integration in VSE One part of Quest is the connection to the VSE Pla97 KBRS98 tool In this section we give a short overview how VSE is integrated in AUTOFOCUS Quest Then we describe how projects or part of projects are imported to VSE or exported from VSE At last some limitations are shown 5 2 1 Overview The integration of VSE is loose which leads to the fact that the user has to follow some rules But the user is guaranteed the greatest flexibility Figure 5 shows the process from AUTOFOCUS Quest to VSE II and back As it can be seen there are three programs involved For the translation of AUTOFOCUS Quest specifications to VSE the Quest Selector can be used to select some parts of a project which should be translated After this the appropriate generator can be started to generate a VSE SL UBR 99
38. e S30 lt lt x False x lt lt y True add SensorSig gt SensorSig gt SensorSig fun add x S00 x add S00 x x add x y None 39 On the concrete system we want to check the property Val IntOWL lt Val IntIWL gt lt gt OPENDif Present In terms of the abstract model this property is Val OWL lt lt Val IWL gt lt gt OPENOK Present To ensure that the concrete property holds we have to show that the abstract prop erty implies the concrete one i e that is is stronger The homomorphism property of the abstraction function the relation between the concrete and abstract states and transitions states that every concrete step including the idle steps has a cor responding abstract step We generate one VSE II theory for the definition of the abstraction see Appendix C 1 one theory for the homomorphism predicate and one for the satisfies relation see Appendix C 2 Our experience with sim ilar proofs in the Isabelle system Ham98 M l98b showed that the correctness conditions for the homomorphism predicate can be proved easily mainly using simplification With the abstraction chooser of Section 7 3 it is very easy to de fine correct abstractions The homomorphism property allows us to eliminate the temporal operators and to concentrate on the correctness of the pure formulas for proving strengthenings To show the strengthening of an imp
39. e language QuestF functions can be defined by pattern matching like in func tional languages In the example of the banking system see Appendix B 2 we have the following example 14 data Card Invalid Valid info Cardinfo dayAmount Int Date const maxAmount 2 fun maxForToday day Valid ci amt lastDay if lastDay day then maxAmount amt else maxAmount E It defines a constant maxAmount and a function maxForToday using the con structor function Valid for pattern matching Since the function maxForToday has no branch for invalid cards it is undefined for this pattern Infix operations can also be defined for example fun Nil s s Cons x s 4 t Cons x s t Defines a concatenation operator for lists The grammar for constants and functions is decl const id cterm fun cterm fundeclsx 5 fundecls cterm For function definitions the form le ft right is required see Section 3 6 On the left side only variables and constructors are allowed All variables used in the right part of the function definition have to occur in the left part Every variable may occur only once within the left part of the equation 3 4 Module Definitions The QuestF languages has a modular structure Every component see Section 2 has a list of DTDs A DTD is a module within the QuestF language the name of the DTD is the name of the module Every DTD has a tree of sub DTDs that corr
40. ect the sample multimedia frontends provided with the distribution the traffic lights example and the elevator example to AUTOFOCUS simu lation environment SIMCENTER you need a PC running Windows NT and the multimedia tool FormulaGraphics A self installable version of AUTOFOCUS is available from the AUTOFOCUS home page http autofocus informatik tu muenchen de index e html Note that you have to register and to accept our license agreement which can be done online to download AUTOFOCUS Compiled versions of the GNU RCS 5 7 and of an Unix like rm commando for Windows NT are available from the AUTOFOCUS download page The Quest extensions are not freely available so there is no public available download page Requirement for the Quest extensions are e preferable an Unix like platform or with some shortcomings a PC running Windows NT The operating system must be capable to run Java 2 The Quest extensions are tested with Solaris 2 6 Solaris 7 Linux Kernel 2 2 and Windows NT 4 0 For the connection to VSE Solaris 2 5 or later is needed For the connection to CTE Solaris 2 5 or later or Linux Kernel 2 2 is needed e a run time version of Java 2 The Quest extensions are tested with the Sun version of Java 2 JDK 1 2 2 e an unzip commando to unpack the archive containing Quest Optional requirements are e for the connection to the theorem prover VSE II version 1 02c or later e for the connection to the mode
41. erent views of AUTOFOCUS are translated and how the retranslation works in detail 8 1 Introduction In AUTOFOCUS there are four different views on systems System structure dia grams SSDs describe the static aspects of a distributed system by a network of connected components exchanging data over channels State transition diagrams STDs which are similar to finite automata are used to describe the dynamic as pects i e the behavior of the components Extended event traces EETs are used to describe exemplary runs of a system from a component based view Datatype definitions DTDs define the types of data processed by a system and are used in the other views The used views are hierarchical For a further description of AUTOFOCUS and its views see HS97 and HMS 98 and HEea96 In AUTOFOCUS Quest we use these views to model systems which are based on a synchronous execution model where time is divided into a sequence of intervals In each interval a channel in the system can carry at most one value and each component executes a reaction where input values are read from the component s input ports and output values are written on the component s output ports Data values on ports that are not read by a component are lost Output written by a component in one reaction is visible to other components only in the next interval If for a component no reaction is explicitly specified it remains in its current state and produces no o
42. erfaces works as follows e STEP 1 produce CTA file from component interface and data type defi nitions The cta file contains the information for the classification tree assistant in the cte 74 e STEP 2 start CTE with generated CTA File and save test cases in CTE File e STEP 3 read CTE file and generate test automton for component All three steps can be done in one guided procedure of the browser First mark the desired component in the browser window Then click on start CTE in the test ing menu see Fig 26 Project Edit Verify Options Repository SingleAFR Create Test Automaton 9 Project BSIDemo 7 Compute Transition Tour EE Component Cd Create Component From Function 3 Port alarmin 3 Port input 3 Port action 3 Port outputA G Port outputE ES Componen O Componen DJ DTD thomes 77 Testdata Comp Testdata Classify Transition Read Transition Classification Classify Component Interface Read Component Classification uu UL U US OU one VOU JUIG z U Figure 26 Starting the CTE It is also possible to do the steps one by one Step 1 is done by clicking on Classify component interface This writes out the CTA information to a file Then you can start the CTE and write the classification tree and test cases to an arbitrary CTE file With Read Component Classification you can read back the test cases and generate the test automaton Note that the appropriate
43. escription of properties is in Section 3 5 After a general introduc tion Section 6 1 we describe how counter examples can be visualized Section 6 2 In the following Section 6 3 1 and Section 6 3 2 we describe how the the different checkers can be used The technical details of the translations are described in other documents See PS99 for the SMV connection and Wim00 for the translation to SATO 6 1 Introduction In this section we give general information for model checking such as parameter selections for model checking and bounded model checking For model checking only finite types are allowed Since many models use integer values we decided to provide an ad hoc abstraction for them We implemented the checking of QuestF integers within a range from 0 to the value of MaxInt This can be used to benchmark different model checkers by changing the value of MaxInt This can be done within the Verify menu of the model browser Since 31 JA AWTapp Praject Edit Testing Verify Options Repository SingleAFRepository geni d Properti 1 49 GMT 03 30 1999 Q Project FM99 9 EI Component BankingSystem 3 Port Slot 3 Port slot2 Port Keypad1 D us Define Maxint R Port Keypad2 re Start SMV 3 Port RadiTime1 3 Port RadioTime2 Start SATO Defining Max Int x Enter max value for representation of unsigned type Int current value 16 i Figure 1
44. espond to imported modules For each DTD and the corresponding tree the export into QuestF format generates a file with a module structure The user can create imported sub DTDs using the Navigate menu of the DTD Editor see Figure 4 therefore it is not necessary to look at the grammar for modules in QuestF 15 dA DTD Editor edit MESSAGE E File Navigate Import finer Pawee Ce YTS LS B La L Ete ar 9 D Li DTD Get next DTD Open new DTD MESSAGE Open existing DTD DTD Description data Message Money Int NoMoney Ballance MailSent data Msg EnterCard EnterPIN EnterAction waiting NoMoneyAvailable MaillsComming ShowBallance GoodBuy ErrorTimeout ErrorwrongPIN ErrorDayLimitExceeded fun withdraw M oney TACwith draw x acc M oney s fun otherAction TA SendMailaca MailSent otherAction TA ViewBallance aco Ballance S Figure 4 Importing a DTD Module In the DTDs of AUTOFOCUS only tree structures are supported whereas the QuestF language supports arbitrary imports 3 5 Properties The QuestF language allows to formulate properties Properties can be defined for every component see Section 4 for the user interface Properties are temporal formulas over components The following temporal operators are supported e f f is always true e lt gt f f is true sometimes in the future e f f is true in the next state Formulas can be connected with the boolea
45. ession testing can be realized by using protocolls from former test runs as inputs 9 3 Performing Tests In order to perform a test an implementing class file must be assigned to the com ponent The class file mus fulfill the conventions determinde in Sect 9 3 1 Then you can run the test as describen in Sect 9 3 2 Sect 9 3 3 gives some hints how to interpret the results of the test run 9 3 1 The Test Object Interface see Reference Manual 9 3 2 Running the Test Bevore running a test you have to associate a class file with the component under test Therefore mark the component and click on Edit Create Subnode Then choose Code and enter the file name of the class When determining the file name use slashes as delimiter and omit the ending class Example home QuestUser ClassesUnderTest Example Then you can mark an arbitrary EET that is associated with the component and start the test with Testing gt Run Test The test driver will now load the class into the virtual machine and try to execute the I O sequence that is contained in the EET Note that boxes and loops are not yes supported by the test driver After the test is finished a protocoll of the test run will be generated and stored as an EET of the component under test 78 9 3 3 Interpreting the Results There may be three possible types of errors in the protocol EET e WRONG_VALUE_ERROR Message has a wrong value e UNEXPECTED_MESSAGE_ERROR This is a
46. ever plus a fixed difference is lower that the inner water level Water levels are measured by sensors sending integer values to the comparators For the critical properties of the system it suffices to differentiate only a few number of integer ranges Therefore we defined the following type for the abstract system model data SensorSig None SNeg SOO S25 S30 The structure of both systems is in Figure 13 The type Signal has only one OWL SensorSig OPENOK Signal IWL SensorSig OPENDif Signal Figure 13 Interfaces of Abstract and Concrete Models signal element Present to indicate that the comparison is positive 38 The behaviour of the system is quite simple see Figure 14 for the concrete and Figure 15 for the abstract model It consists of an STD with only one state and one transition however within the transition there are constants openDiffer ence and operations lt that have to be abstracted as well Therefore we defined the following operations on the type SensorSig owlt topenDifference lt iwl IntIWL iwl IntOWL owl OPENDif Present Figure 14 Concrete Behaviour add owl S00 lt lt iwl IWL iwl OWL 0wl OPENOK Present Figure 15 Abstract Behaviour op lt lt SensorSig gt SensorSig gt Bool fun None lt lt x False x lt lt None False x lt lt SNeg False S00 lt lt S00 False S25 lt lt S00 False S25 lt lt 525 Fals
47. everal unexpected behaviours that can be found out using model checking for example the timer does not necessarily produce timeouts if it has been set The reason counter example is that it can be set again before it produces the timeout In this case the timer starts again In the complete model however this situation does not occur since the timer is used correctly The timer can also be used to benchmark model checking because there are in the File Quest TL Module TimeConstants constants that determine the length of the phases Setting them to high values and increasing the MaxInt value in the browser can lead every system to its limit B 4 Other Work In this section we refer to further work not contained in the Examples directory that has been done using the tools and methods of Quest e The internal paper Testgenerierung in Quest from S Sadeghipour and T Klein describes the test methods of Quest especially how the communi cation test method has been applied to test communication channels of the storm surge barrier model e Within the analysis of the storm surge barrier several models have been built The AUTOFOCUS Quest models have been described within the pre vious sections Another model has been built using a direct encoding into VSE The model has been build such that it allows for the specification of real time properties and several critical aspects have been verified The work is described in the inter
48. fficient abstraction concept and thus decreases the amount of intuition usually required for abstractions The abstraction function relates concrete and abstract components in AUTOFOCUS Quest This requires that the abstraction function relates e control states e local variables e input and output ports e types with the following informations name of the type constants and functions and a mapping from concrete to abstract values e the relevant properties Therefore abstractions functions consist of several parts that all have to be de fined and that have to fit together for example the mapping of the ports has to respect the mapping of the types 37 According to our methodology abstraction functions are an attribute of the con crete component therefore abstraction functions are treated as attributes of the concrete component in the model browser To facilitate the input of abstraction functions Quest provides an abstraction chooser that helps in defining type correct abstractions First in Section 7 2 we shortly present a small example for abstractions and in Section 7 3 we ex plain how to use the abstraction chooser 7 2 Abstraction Example Comparator The comparator has been modeled as a part of the storm surge barrier case study This comparator compares the inner water level with the outer water level to determine whether the barrier can be opened This is the case if the outer water l
49. ficLights QuestTL contains the model The case studies are stored within the QuestML format and can be loaded into AUTOFOCUS and into the model browser Furthermore there are some properties available that can be loaded into the model browser to check something The files are located in the Examples directory see installation A and can be loaded into the model browser as described in Section 4 2 Figure 29 shows the subdi rectories of the Examples directory each containing a case study B 1 Emergency Closing System of Storm Surge Barrier The emergency closing system of the storm surge barrier in the Oostershelde is the biggest case study It has been analyzed with different methods and several models have been build In the directory StormSurgeBarrier there are the following files 85 Look in C Examples x rs 99 Es EI FM39 J StomS urgeBarrier EI TrafficLights File name Open Files of type all Files 7 7 v Cancel Figure 29 Content of the Examples directory e SSB the original model see Section B 1 1 e QSS an improved model see Section B 1 2 e Comparator a comparator for sensor signals see Section B 1 3 Section B 4 concludes with references to further work Starting point of our activities was an internal paper of the Dutch SIMTECH com pany vdMvdW98 that should be the basis for a public offer for building a new emergency closing system because the old sys
50. file which contains all the information This file can be imported to VSE For the retranslation the VSE specification has to be exported and the appropriate generator has to be started The resulting Quest repository can be imported to AUTOFOCUS Quest afterwards 23 AutoFocus gt VSE Quest Selector Generator AutoFocus Quest VSE gt AutoFocus Generator Figure 5 Connection AUTOFOCUS VSE 5 2 2 Importing Projects in VSE If you want to import an AUTOFOCUS project to VSE you have to export it first from AUTOFOCUS For further help on exporting a project in the Quest format see 5 1 1 Now the selector can be used to choose a part of the project which should be translated to VSE or the translation can be started on the whole project Translation of a whole project To generate a VSE SL file for the whole project start the following command in a shell af2vse useinclude withoutsubgraphs lt QML filename gt VSE filename lt PropertyFilename gt You have to specify the filename of the AUTOFOCUS Quest repository and the filename of a VSE SL file in which the translated code should be saved Also a file with properties in text format may be specified which then will be translated to VSE There are two other optional arguments which control the structure of the generated VSE SL code The option useinclude controls if the translation of an AUTOFOCUS component with its automaton will be inlined or incl
51. ible Otherwise the test sequentialization produces transition sequences which have no corresponding trace of input output values that is executable on the test object and on the specification The Quest development method provides the combined function and trace test CFTT Sad98 Sad97 strategy for deriving suitable test cases for single compo nents This strategy includes a data partition that transfers a part of the data state into the control state of the automaton Actually this task is not supported by the AUTOFOCUS Quest tool and has to be done manually but methodical support is provided in analysis paper of the quest project SK97 Integration Test The objective of the integration test is the detection of faults in the interaction of two or more previously tested components AUTOFOCUS Quest supports the integration test with the channel test The channel test finds errors on a specific channel between two components Possible sources of errors can be wrongly interconnected components or different implementations of used proto cols Actually AUTOFOCUS Quest provides methodical support for generating a test automaton that fits the needs for the channel test For details see analyisis paper of quest SK97 Classifying Transitions One of the core AUTOFOCUS Quest benefits is the creation of a classification proposal of the input data space of certain transi tions These proposed classifcations are imported to the CTE tool The CTE too
52. in http www fmse cs reading ac uk fm99 In the Examples directory there is a subdirectory FM99 containing e FM99 the complete model in QuestML format 87 e BankAbs an abstract model in QuestML format Both Files contain some critical properties of the system B 2 1 Complete Model We modeled the banking system with different hierarchic graphical description techniques for structure and behavior The model is based on a finite functional description of datatypes for example for credit cards and operations likes max ForToday The model includes two tills user interaction simple checks communication with the system two lossy connections and a central including drivers for the lossy connections and a database We did not model the database in detail but we used nondeterminism of AUTOFOCUS to decide whether money can be withdrawn or not This level of abstraction allowed to prove many interesting properties especially on the lossy connections and the drivers The model is hierarchic reuses several state transition diagrams for example both tills have the same behaviour and it is based on a rich set of data definitions describing the information on credit cards and transactions This made the model very complex such that it could not be model checked completely but bounded model checking could be applied To model check the complete system we built an abstraction see Section B 2 2 B 2 2 Abstract Model The file Ban
53. ion Selected nodes are displayed inverted Select operations add nodes to the already selected nodes 28 MAINBankSystem_Module_MESSAGE MAINBankSystem_Module_MESSAGE Drivert_Scheduler Database_Combine E Driver2_Scheduler Database_Barrier Process2_Scheduler Processi Scheduler p jn Figure 8 VSE Select Quest So more than one select operation may be used and the operations to describe the set of objects to be exported may be mixed There are two special operations for the use with Quest The popup menu of Theory and Tlspec contains a sub menu Select Quest with the operations Rest ricted and A11 see Figure 8 With A11 all objects are selected with Rest ricted all objects in the graph which are referenced from the actual object including the actual object itself are selected Since it is not always obvious which nodes are selected you may want to choose Deselect AllinActions menu ofthe VSE main window before you begin your selection Export After you have chosen all objects you want to reimport to Quest the the export can be started with File only or Call Transformer in the Ex port Quest submenu of the VSE main window see Figure 9 With File only you have to start the VSE to AUTOFOCUS translation yourself if you 29 Figure 9 VSE Export Quest choose Call Transformer then the retranslation to Quest is started automat ically Before the export it
54. ion Properties Driveri Scheduler Database Combine og 7 Driver2 Scheduler Database Barrier Process2_Scheduler Processi Scheduler Figure 23 Development Graph of the Banking System HIDE compCounter endcomp TLSPECEND The missing TLSPECs for the components Driverl and Database of the example are similar to the TLSPECs of the component Connectionl and are therefore not presented here In Fig 23 the development graph of the whole example like presented in Ap pendix B 2 is shown 8 2 2 STD In this section we explain the translation of components with automatons to VSE SL As in the example above we use the withincludes option so that the scheduler and the automaton of a component are split into two separate TLSPECS This is simpler for understanding and editing the generated specification but it may be more unhandy when doing proofs In the following example the component Driver1 is shown In Fig 22 the SSD of the component Cent ral with the component Driverl is shown In Fig 24 the automaton which describes the behavior of Driverl is presented Below the VSE SL specification of the scheduler and the component itself is shown The 29 Inp i CAck Present Tinli Inp CAck Present Inp Tout m store m Inp i Tout m Tinli store m Lera aiaee gt C m Inp i Tout CAck Tyn i Answer store Inp i Tout m CAck Tin i Answer m store m Figure 24 Automaton of Component Driverl s
55. ironment 91 Dniroduction s s uos Sew eek OES AERE de x EEE REESE SB 9 2 Creating Test Sequences cn os eRe RR ERR kr OA Vest Base Sas 2d Rak Rr REOR X EGRE 922 Test Basis SSD with STDs ss 02 3 Test Basis Functions uu z ss sss Soe aa Ha 9 2 4 Deriving sequences from test automata 929 SERA BETE c etare ees mau e q Ey a xg 93 Perlormins Tests 2265224 x REESE Ed URS AUR AES 9 3 1 The Test Object Interface 25 o o 4 4 2 32 R nnne the Test o s se Doo ew OAS e Rx Oa 9 3 3 Interpreting the Results a as Ro RR m Installation Al System Requirements suu sue sock ana EXE B TSAR auos Xu Soon Ox Xx Be SD MOX RC RE 45 45 47 47 39 66 71 71 T2 T2 73 73 74 74 76 T 77 78 78 78 78 79 AO AONDBHIBUG X suce pocs cor os WR HH FOE REEK 84 AJ Uninstallation 6 2 oe SK cR Dex HSS SS HS OE SHE 84 Case Studies and Examples 84 B 1 Emergency Closing System of Storm Surge Barrier 85 Bid Tae Cemal MOOR sace Hore et Re yox 86 B 1 2 An Improved Model 2 2 2 xo es zu ur ai 87 B 1 3 A Comparator for Sensor Signals 87 B 2 FM99 Banking System 2 e ose R ana aa se wat 87 B 2 1 Complete Model 24 42 as 446 44 88 B22 Abstract Model ss es bok sw x eR OGRE 88 Bo Traffic Light Control System 35 8 RE bee be 88 B4 Other Work keke ae bueedeXe Be oe edes here 89 Correctness of Abstractions 90 C 1 Definition of the Abstraction Function 90 C 2 Homomorphos
56. kAbs contains an abstraction of the system that has been generated by replacing all data types of the system by single valued types For example a the new type Card for credit cards contains only the element AnyCard Fur thermore the file contains two properties of the complete system stating that the connection between the tills and the central is working i e if the till sends any message sometimes there will be a response Of course in this model no state ments concerning the content of the messages hold however model checking the complete system only takes about one minute and one minute for the generation B 3 Traffic Light Control System The traffic light control system is the smallest case study in the Examples direc tory It contains the following files 88 e Quest TL The model in QuestML Format including the DTD Files QuestTL Module Signal QuestTL Module Lights QuestTL Module Keys QuestTL Module TimeConstants e Timer prop a true property of the timer e System prop a true property of the system The model can be used for demonstrations because it is very small fast and understandable The model describes a small traffic light system similar to the traffic light system described in HMS 98 However it has more components for example a timer and it uses functional datatypes for the Lights This reduces complexity of the state transition diagrams and increases understandability of the model The model contains s
57. l 76 enables the tester to partition the input data according to the classification tree method GWG95 As long as the tester sticks to some conventions the marked tests can be reimported to the AUTOFOCUS Quest tool Alike the classification of component interface the classification of transitions can be either done in one guided procedure or three single steps e STEP 1 produce CTA File from single transition and data type definitions e STEP 2 start CTE with generated CTA File and save test cases in CTE File e STEP 3 read CTE File and insert new transitions in automaton The guided procedure is started with startCTE in the Testing menu Note that a transition node has to be selected because st art CTE is sensitiv with regard to the selected node If a transition node is selected st art CTE will start the pro cedure to classify the input data of a transition If a component node is selected startCTE will classify the component interface If you prefer to do the steps one by one step 1 is initiated by pressing on Testing gt Classify Tran sition and step 3 is done with Testing gt Read Transition Classi fication Be aware that the same transition is selected in the browser when doing step 1 and 3 Otherwise the test cases cannot be reimported to AUTO FocuS Quest correctly 9 2 3 Test Basis Functions Function definitions are the third test basis By selecting a function definition and executing Testing gt Create Componen
58. l checkers SMV version 2 5 SATO version 3 2 e for the testing environment CTE 80 A 2 Installation For further notes on installation and configuration of AUTOFOCUS see the readme file contained in the zip archive For the installation of the Quest tools follow these steps 1 Unpack the archive quest zip with your favorite unzipper to a temporary directory E g on Unix like platforms cd tmp unzip quest zip This will create a directory Quest Install with two files Readme txt and install class 2 Please readme file for up to date instructions 3 Change to the directory Quest Install and start the installer cd Quest Install java install 4 After a while you should see the Welcome to the Quest Setup program see Fig 27 5 The steps through the Quest setup should be self explanatory The main thing is that you have to enter a directory in which the Quest tools will be installed see Fig 28 That directory is the Quest Home 6 After the installation process the Quest tools reside in Quest Home bin It is recommanded that you expand your path settings appropirate export PATH Quest Home bin S PATH A file named quest with environmentvariable settings will be created in the Quest Home directory and if Quest setup is not started as a user with root privileges then it will be copied to the installers home directory This configuration file is needed for the Quest tools
59. lication we have to strengthen the cor rectness conditions for this implication is a strengthening of the right conclusion OPENOK Present gt OPENDif Present and a weakening of the condi tions Val OWL lt lt Val IWL lt Val IntOWL lt Val IntIWL For the definition of strengthenings in VSE II see Appendix C 3 the definition of the elements mapping from concrete to abstract elements is required The cor rectness conditions are in a separate theory as well as the satisfies statement see Appendix C 3 Our experiences showed that proving strengthenings mostly involves simple rea soning on data structures for which the VSE II system is very appropriate How ever it takes much time to realize that an abstraction is not correct especially on the level of theorem provers Therefore the most important step is to define cor rect abstractions This is done on the modelling level and not within the theorem prover 7 3 Using the Abstraction Chooser To define an abstraction in Quest the concrete component has to be selected If an abstraction already exists it is stored as an attribute of this component and can 40 be edited In this section we show how to define a new abstraction After the con crete component is marked in the Verify menu the button New Abstraction is enabled that starts the abstraction chooser In general there are two possibilities to define abstractions 1 to compute
60. m Proof Obligation 91 C 3 Strengthening Proof Obligation 93 1 Introduction In this user guide we describe the tools developed within the project Quest The goal of the project Quest was to combine graphical software development tools with tool to ensure the quality of the developed software There are different kinds of such tools e model checker can be used to check temporal properties of finite models automatically e theorem prover support manual verification of arbitrary models and prop erties e test tools test the developed software During the analysis phase of the project we selected AUTOFOCUS HMR 98 HMS 98 for graphical system specifications and decided to connect the model checkers SMV RSW97 and SATO Zha97 and the theorem prover VSE II to AUTOFOCUS For testing we selected the CTE GWG95 for the classification of variables and implemented several methods to generate test cases from AUTO FOCUS specifications Furthermore a test driver has been implemented to test Java programs against the test cases Figure shows the structure of the tools of the project Quest The boxes represent the connected tools and the arrows between them denote the connections that are designed and implemented within the project Quest We integrate the tools by defining interfaces and sometimes partial translations between the used con cepts The interfaces use the QML Quest model language
61. mar for data definitions ddata is in BNF Syntax ddata data string tvars dconstr dconstrs 5 tvars tvar cotvar cotvar tvar tvar string dconstrs dconstr dconstr string id karg kargs karg infid karg kargs karg karg type id type Type definitions can be used in DTDs to define additional functions see Section 3 3 The only exception is the predefined polymorphic type Channel m see Section 3 8 13 3 2 Terms In the language QuestF the following terms are allowed e atoms constants variables like 2 or X e applications like not x or mult x y e infix applications like 2 3 or x y e conditionalslike if x then y else z fi wherethe else branch can be omitted and e unnamed functions lambda abstractions like param x y t Around arbitrary infix operators there are brackets required Predefined infix oper ators see Section 3 8 2 have priorities that allow to write terms like atb c d The important grammar rules for building terms are cterm cbase typean typean 3 type cbase sign id param string cterm L cterm infid cterm if cterm then cterm else cterm fi if cterm then cterm fi unop cterm cterm sign Lambda abstraction is not supported for model checking and VSE generation In the next section we show how to define functions in QuestF 3 3 Function Definitions In th
62. mm Test Case Design Us ing Classification Trees and the Classification Tree Editor In Pro ceedings of 8th International Quality Week San Francisco pages Paper 4 A 4 May 30 June 2 1995 Tobias Hamberger Verifikation einer Hub schrauber berwachungskomponente mit Isabelle und STeP 1998 Student software development project Technische Universitat M nchen Germany Tobias Hamberger Kombination von Theorembeweisen und Model Checking f r I O Automaten Master s thesis Computer Science Department Technical University Munich 1999 F Huber G Einert and et al AutoFocus User s Manual 1996 F Huber S Molterer A Rausch B Sch tz M Sihling and O Slotosch Tool supported Specification and Simulation of Dis tributed Systems In nternational Symposium on Software En gineering for Parallel and Distributed Systems pages 155 164 1998 95 HMS 98 HS96 HS97 HSE97 Jon93 KBRS98 Kur87 LGST95 Mer97 MN95 F Huber S Molterer B Schatz O Slotosch and A Vilbig Traf fic Lights An AutoFocus Case Study In 1998 International Con ference on Application of Concurrency to System Design pages 282 294 IEEE Computer Society 1998 K Havelund and N Shankar Experiments in theorem proving and model checking for protocol verification In M Gaudel and J Woodcock editors Formal Methods Europe Lecture Notes in Computer Science pages 662 681 Springer Verlag 1996
63. model format and can also be used by other tools All tools are connected to the models of AUTO Focus The models are exported from AUTOFOCUS that is be used to specify the model using graphical views The models are represented in a textual format QML and can be managed using the model browser Furthermore many quest programs can be started from this model browser For the connections of AUTOFOCUS to the other tools two new features have been integrated into AUTOFOCUS e the functional language QuestF and e the textual interface export and import QML The functional language QuestF is used in DTDs transitions in STDs and in prop erties It is the logical basis for the translations to the other tools The interface is used to import and export projects from AUTOFOCUS to the model browser 5 SMV Verification Bounded Model Checking Graphical Views Selecting VSE II CTE Test Cases Theorem Proving Conformance Testing Test Java Program Figure 1 Tool Structure of Quest This user manual is a description of the Quest extensions of AUTOFOCUS We assume the user to be familiar with AUTOFOCUS models and terms like STD or type This manual describes the features implemented within the project Quest and the user interface to use them There are several publications available on the Quest homepage that describe more general aspects e Quest Overview over the project Quest S1098 e Pr
64. mparator is identical to the compara tor modelled within the above models of the storm surge barrier Using abstrac tions and the verified abstract model we can insure the correctness of the concrete model The correctness proofs have not been carried out using VSE due to lim ited resources within the project However similar proofs have been carried out using the Isabelle system Ham99 The essence of this work has been that it is much easier to discharge the proof obligations compared with the finding of cor rect and useful abstractions To ease this process we integrated the abstraction chooser within our framework The comparators are described within Section 7 2 the generated correctness con ditions can be found in Appendix C B 2 FM99 Banking System On the Formal Method World Congress 1999 in Toulouse there was a tool exhibi tion with a competition Every participating tool was invited to model a banking system with tills and transactions to withdraw money from accounts Critical properties had to be formulated and verified We participated with our tool and modelled the banking system Due to the simple modelling language and the rich possibilities to verify properties our tool AUTOFOCUS with Quest won the first price Descriptions of the requirement document and a paper describing our solution can be found under http autofocus in tum de More information on the formal method world conference and the competition can be found
65. mpty represented by NoVal For polymorphic data types the are parameter theory generated that contain all param eters of the defined and imported data types Therefore different parameters have to be used ifthey should not be unified The translation of the type Channel m are the following VSE II specifications THEORY mParam TYPES m THEORYEND BASIC ChannelBase PARAMS mParam Channelm NoVal WITH is_NoVal Msg Val m WITH is_Msg BAS ICEND THEORY CHANNEL PARAMS mParam USING BOOLEAN INTEGER 69 ChannelBase m THEORYEND The type channel is instantiated for every defined data type in the main module of the translation that is imported from the translations of the AUTOFOCUS Quest components THEORY MAINFM99 Module MESSAGE el Card CHANNEL Card el Date CHANNEL Date Chan Chan THEORYEND USING MESSAGE TRANSACTION SIGNAL Channel Bool CHANNEL Bool Channel Int CHANNEL Int Channel Message CHANNEL Message Channel Msg CHANNEL Msg Channel Action CHANNEL Action Channel Info CHANNEL Info Channel Keys CHANNEL Keys Channel Cardinfo CHANNEL Cardinfo Chann n n el Signal CHANNEL Signal Translation of Properties Properties in AUTOFOCUS Quest hold at the speci fied states No intermediate states are possible due to the synchronous semantics of AUTO
66. n additional message and does not exist in the original test e NOT_RECEIVED_ERROR The test driver expected this message but did not receive it A Installation In this section the requirements and the installation for AUTOFOCUS and Quest are described While a freely available version from AUTOFOCUS is download able from the AUTOFOCUS home page http autofocus informatik tu muenchen de Quest isn t public available Both tools are provided in zip archives and have a self installable archive included See the readme file contained in the archive for latest informations A 1 System Requirements Both AUTOFOCUS and the Quest extensions run under Unix platforms and Win dows NT AUTOFOCUS is a freely available case tool prototype Requirements for AUTOFOCUS are e an Unix like platform or a PC running Windows NT The operating system must be capable to run Java 2 AUTOFOCUS is tested with Solaris 2 6 Solaris 7 Linux Kernel 2 2 and Windows NT 4 0 e arun time version of Java 2 AUTOFOCUS is tested with the Sun version of Java 2 JDK 1 2 2 e GNU RCS Revision Control System version 5 0 or higher as the reposi tory server uses RCS to provide access and version control AUTOFOCUS is tested with GNU RCS version 5 7 e an Unix like rm commando Of course this is available for all Unix plat forms and only needed for Windows NT 79 e an unzip commando to unpack the archive containing AUTOFOCUS e to conn
67. n operators for terms see Section 3 8 2 Formulas can refer to attributes of the component and to the operations available on these model attributes e StateName refers to a state named StateName is the current state On states the only operations are 16 equality inequality e PortName refers to a port named PortName On ports the following operations can be applied p x port p sends the value x p x port p receives the value x x can also be a pattern consisting of variables and contructor functions Furthermore all functions available on the type Channel see Section 3 8 1 can be applied for example to state that a port p is empty by is NoVal p e LocVar refers to a local variable LocVar of this component All opera tions available on the variable can be applied e SubName refers to a subcomponent named SubName On subcompo nents all attributes can be refered using a as delimiter With the possibility to refer to subcomponents we have a qualification mechanism for properties Properties are automatically translated into a fully qualified form after they have been entered An example for a property of the component Connect ionl is Answer NoMoney CentralMsg NoMoney It is expanded to the fully quantified property FM99 BankingSystem Connectionl Answer NoMoney gt FM99 BankingSystem Connectionl CentralMsg NoMoney Since properties are built like usual terms
68. nal paper Modelling Specification and Veri fication of an Emergency Closing System by W Stephan G Roch and M Brodski 89 e The Adelard company has verified the design of the storm surge barrier vdMC99 Some parts have been modelled with HOL other parts have been encoded directly into the SMV system C Correctness of Abstractions This section contains all proof obligations that are generated for the correctness of the abstraction defined in Section 7 2 C 1 Definition of the Abstraction Function Since the generation of proof obligation involves the application of the abstraction function it is not necessary to explicitly define in terms of VSE II the abstraction for all elements of the model Port Types etc however since the relation between the states is essential the abstraction function has to be defined for states In the example this is specification of state abstractions THEORY OpenBarrier_AbsState_Definition USING Concrete_States Abstract_States FUNCTIONS AbsStates tConcrete_States gt tAbstract_States PREDICATES AbsInitial tAbstract_States ConcInitial tConcrete_States VARS Abs tAbstract_States Conc tConcrete_States AXIOMS FOR AbsInitial DEFPRED AbsInitial Abs lt gt IF Abs Abstract_States sMAIN THEN TRUE ELSE FALSE FI FOR ConcInitial DEFPRED ConcInitial Conc lt gt IF Conc Concrete_States sMain THEN TRUE 90 ELSE FALSE FI
69. nelBase is_Msg IWL AND Channel_SensorSig ChannelBase is_Msg OWL AND add Channel SensorSig ChannelBase Val OWL S00 Channel SensorSig ChannelBase Val IWL AND AbsStates Conc AFi ControlState AbsStates Conc Concrete_States sMain correctness for idle transition in state Main ALL Vl lt gt Conc AFi ControlState Conc Concrete States sMain AND Vl Conc l gt Conc AFi_ControlState Conc Concrete_States sMain AND NOT Channel_Int ChannelBase is_Msg IntIWL AND Channel_Int ChannelBase is_Msg IntOWL AND Channel_Int ChannelBase Val IntOWL openDifference lt Channel_Int ChannelBase Val IntIWL AND Conc AFi ControlState Conc Concrete States sMain AbsStates Conc AFi ControlState AbsStates Conc Concrete States sMain AND NOT Channel SensorSig ChannelBase is Msg IWL AND Channel SensorSig ChannelBase is Msg OWL AND add Channel SensorSig ChannelBase Val OWL Channel SensorSig ChannelBase Val IWL AND AbsStates Conc AFi ControlState AbsStates Conc Concrete States sMain 92 S00 TLSPECEND C 3 Strengthening Proof Obligation The strengthening proof obligation defines the mappings between the concrete and theabstract types in thefollwoing theory THEORY OpenBarrier_Strengthen_Definition USING OpenBarrier_AbsState_Definition MATNComparator_Module_HWSignal FUNCTIONS Int2SensorSig SensorSig
70. nnelBase NoVal AND store Channel_Message ChannelBase Val Tout D Waiting2Waiting AFi Cont Col SL ate sWaiting 63 AND AFi_ControlState sWaiting AND Channel_Info ChannelBase is_Msg Inp AND AFi_Tin Channel_Info ChannelBase Msg Channel_Info ChannelBase Val Inp AND AFi_Answer Channel_Message ChannelBase NoVal AND UNCHANGED store Waiting2Driving 1 AFi ControlState sWaiting AND AFi ControlState sDriving AND Channel Info ChannelBase is NoVal Inp AND Channel Message ChannelBase is Msg Tout AND AFi Tin Channel Info ChannelBase NoVal AND AFi Answer Channel Message ChannelBase NoVal AND store Channel Message ChannelBase Val Tout Driving2Driving AFi ControlState sDriving AND AFi ControlState sDriving AND Channel Info ChannelBase is Msg Inp AND Channel Message ChannelBase is Msg Tout AND Channel Signal ChannelBase is NoVal CAck AND AFi Tin Channel Info ChannelBase Msg Channel Info ChannelBase Val Inp AND AFi Answer Channel Message ChannelBase Msg Channel Message ChannelBase Val Tout AND store Channel Message ChannelBase Val Tout Driving2Driving 1 AFi ControlState sDriving AND AFi ControlState sDriving AND Channel Info ChannelBase is Msg Inp AND Channel Message ChannelBase is NoVal Tout AND Channel Signal ChannelBase is
71. nt Manual selection mode A left mouse button click deletes the selection and adds the component on which the mouse was positioned A right mouse button click selects or unselects the current object under the mouse If a tree was folded all objects in it will be unselected With the Select button the current selection can be activated So the selected objects in the left panel will be presented in lists in the right panel These lists in the right panel can only be viewed to control the selection no operation on the right side is possible With the Select AI1 button the whole specification can be selected The current selection can be deleted with the button Deselect All If you want to export only a subtree of the whole project you have to select one component left click and then you have to choose Set Root Afterwards only the selected subtree will be presented To reset this operation unselect all se lected objects e g with right mouse button clicks and then click on Set Root To export the current selection presented in the right panel choose Export Afterwards a filename for the VSE SL specification can be chosen and then the translation to VSE II starts Import in VSE After the appropriate VSE SL file has been generated it can be imported to VSE To start the import use the menu Import Quest in the File menu of the VSE main window see Figure
72. oO Component Abstract 9 C OTD home wiss slotosch QUE S T quest Software BSI Comparator Module HWSignal 3 Module HWS na 9 EI Module HWFloat D FunctDef op lt lt 3 FunctDet add Fj Module OPENDIF Figure 3 The Model Browser 10 DTD Property Abstraction e Automaton STD with an attribute state for the description of the be haviour e State with attributes Substates transition segments parts of transitions e Transition Segment with attributes Precondition Input patterns Output patterns Actions e EET with attributes e DTD with several modules e Modules related types and functions See Section 4 for a description of the features of the model browser 3 The Language QuestF DTDs and Properties In this section we describe the language QuestF QuestF is a functional language extended with some constructs for the description of system properties The functional part of QuestF ist similar to ML Pau91 or Gofer Jon93 the tem poral operations are like those in TLS Miil98a a subset of LTL The operations for the system descriptions are close to the notations used in the AUTOFOCUS tool The model supports the concatenation of different transition segments to one transition Inter level transitions In AUTOFOCUS inter level transitions between documents require identical labels semantics otherwise they cannot be unified during the simulati
73. ocess Enriching the Software Development Process by Formal Methods BS99 e Integration concept Consistent Integration of Formal Methods BLSS00 e Model checking design The Quest for Correct Systems Model Checking of Diagrams and Datatypes PS99 This user manual is structured as follows In Section 2 we present the document and model structures within AUTOFOCUS including the extensions like properties that are not part of AUTOFOCUS In Section 3 we present the language QuestF by introducing and explaining examples for types functions and properties Section 4 contains a description of the user interface of the model Browser and Section 5 describes how the browser is integrated into AUTOFOCUS and into VSE The translation of models to SMV is described in Section 6 and Section 7 explains the usage abstractions to extend the applicability of model checking to larger and infinite systems Section 8 describes the connection to the theorem proving environment VSE The test environment and the methods to generate specification based test cases are explained in Section 9 The appendices A and B conclude the manual with an installation guide and an overview over the examples shipped with the software 1 1 Conventions used in this manual This manual uses different fonts to represent different types of information Shell commands appear in a monospaced font For example command optional argument lt filename gt l www4 in t
74. of Quest enables you to perform the following tasks of the testing process e Derivation of test sequences from specifications e Manual creation of test sequences e Running the tests on test objects Although the test environment has a test driver that allows you to perform the specified test sequences the test environment focuses more on the creation of reasonable test sequences than on the execution of given tests Fig 25 shows an overview over all testing tasks of the Quest development process The rectangles of the diagram are components of the Quest repository and the arrows are testing tasks that produce new components or alter existing components in the repository component TS 2 CTE java class SSD DTD test sequence EET TS 1 TS 2 TS 3 TS4 automaton TS 3 SSD STD CFTT testautomato function def TS 4 testsequentialization DTD Quest repository regression tests Figure 25 Overview about the test activities in Quest 73 9 2 Creating Test Sequences There are several possibilities to create reasonable test sequences that can be used for testing the target software the test object The choice of the appropriate test sequence creation method is mainly determined by the type of the given specifi cations i e the more detailed the specifications are the more specific is the test sequence generation process The kind of the given specification is called the test basis In Quest
75. on a repository and open a new one the current repository will be closed before the new one is opened So be patient and save the contents of the current repository before opening a new one Close repostory Closes the repository and throws away all changes since last save Save repository Save the repostitory to the same file where it was loaded from In the current version it is not possible to save the repository to another file Therefore the repositories should be copied to a new file before they are loaded into the browser Beside the repository file you also have to copy all module files in order to read in the copied repository properly Import repository Import all projects of the specified repository into the repository that is currently loaded into the browser This function does not per form the type check 4 3 Viewing and editing nodes If you want to view the attributes of the selected elements check the box in Options gt Show Attribute Window All nodes of the current selection will be displayed in a separate window The attributes of some nodes can be edited in the attributes window e g messages 4 4 Creating new nodes With the model browser new subnodes can be created The current version does only support the creation of a Code subnode for a component Future versions 21 will allow the creation of arbitrary nodes In order to create a new Code subn ode first select the associated component node and then press
76. on or the QML export 11 In the following subsections we provide syntax for the language QuestF and ex plain it by some examples of a banking system see Appendix B 2 or http www4 in tum de proj quest for a description of the example Fur thermore we characterize the subsets of QuestF that can be used for model check ing and for the export to VSE 3 1 Type Definitions Type definitions are the central part in the DTDs of AUTOFOCUS Quest They define types and elements of QuestF For example data Message Money Int NoMoney Balance MailSent defines the type Message and the elements NoMoney Balance andMailSent and the function Money Int gt Message that constructs an element of type Message for each argument of type Int The elements and functions defined within the data construct are called constructors and can be used in patterns to define functions or transitions with pattern matching see Section 3 3 The defined types can be used in SSDs together with the default types Bool Int Float The defined elements can be used in the transitions of STDs for example in m lt 0 x Money m s m ans NoMoney Msg Money m This transition reads from the channel x of type Message and writes to the channels s of type Int and ack of type Message The transition can only be executed if the following conditions hold e a value is on the channel connected to the port m e the value matches the
77. onential com plexity it is possible to enter a maximum time bound for the checking time If 32 this time bound is exceeded checking is aborted In addition it is possible to can cel the model checking manually The selection of the time bound is done after the start SMVorthe start SATO in the verify menu The relation from the passed time and the maximum time is displayed in a progress bar Of course it is possible to run several checks in parallel however not of the same component For bounded model checking a search bound is required This reduces the search to counter examples of this length If the search bound is greater than the diameter of a system than the result of bounded model checking is equal to model check ing i e if no counter examples are found than he checked properties are verified The diameter is the maximum of the shortest path to every reachable state 6 2 Counter Examples Model checking and bounded model checking produce counter examples They are inserted automatically into the model browser in form of a MSC The name of the generated MSC corresponds to the property The attributes like channels and messages can be inspected using the model browser To visualize the counter examples graphically as EET views of the MSC models the repository has to be saved and imported from the AUTOFOCUS tool 6 3 Connected Checkers Within the project Quest two checkers have been connected to AUTOFOCUS SMV and SATO In
78. ons using the FUNCDEF keyword Since functions cannot be defined in BASIC theories every DTD is translated into a THEORY that includes the BASIC theories for the data types Functions with result type Bool are translated into predicates An example from the banking system see Section B 2 is module TRANSACTION data Action SendMail Withdraw Int ViewBallance data Info TA Action account Int fun isMoneyRequest TA Withdraw x acc True isMoneyRequest x False end It is translated into THEORY TRANSACTION USING BOOLEAN INTEGER ActionBase InfoBase PREDICATES isMoneyRequest Info VARS VlisMoneyRequest Info AXIOMS FOR isMoneyRequest DEFPRED isMoneyRequest VlisMoneyRequest 68 IF is_TA VlisMoneyRequest AND is Withdraw TASell VlisMoneyRequest THEN TRUE ELSE FALSE FI THEORYEND The name of this theory is the name of the DTD Translation of Polymorphic Data Types Polymorphic data types are types that have arguments type variables like List a Set a Within Quest the translation of polymorphic data types is supported even if the concept of pa rameterization in VSE II is slightly different The most important example of polymorphic data types is data Channel m NoVal Msg Val m It is in the VSE II translation of every AUTOFOCUS Quest component since the channels and ports of AUTOFOCUS can be e
79. ortant part of the definition of the abstraction functions is the relation of properties The correctness of the abstraction function is defined only for the related properties For them strengthening proof obligations are generated In principle every concrete property could be abstracted to arbitrary abstract prop erties however a similar temporal structure is recommended i e an gt lt gt property should be related to a property with a similar structure otherwise the strengthening proof obligation can become very difficult The abstraction chooser displays for each property of the concrete component a choose box with all properties entered to the abstract component and the value not related The abstraction chooser allows to enter a related property for each concrete in our example only one property is related see Figure 20 If all parts of the abstraction function are defined correctly the Finish button is enabled Pressing it stores the abstraction to the concrete component The proof obligations for the correctness are generated when the repository is exported to VSE II 43 A AbstractionChooser Em ai tComp araor Combine Conerete mow fnot rime 7 MG val Comparator Combine Concrete now RIVER Comparator rnae nps v S la pd Figure 20 Relating the Properties 44 8 Connection to VSE In this section we describe the translation from AUTOFOCUS to VSE and the retranslation We show how the diff
80. osch Quest Overview over the Project In D Hutter W Stephan P Traverso and M Ullmann editors Applied Formal Methods FM Trends 98 pages 346 350 Springer LNCS 1641 1998 B Steffen K G Larsen and C Weise A constraint oriented proof methodology based on modal transition systems In Proc Ist Workshop on Tools and Algorithms for the Construction and Analysis of Systems volume 1019 of Lecture Notes in Computer Science pages 17 40 Springer Verlag 1995 97 UBR 99 vdMC99 vdMvdW98 Wim00 Wol86 Zha97 Ullmann Baur Reif Siekmann Scheer and Moik Specification Language VSE SL Version 2 1999 Meine van der Meulen and Tim Clement Formal Methods in the Specification of the Emergency Closing System of the Eastern Scheld Storm Surge Barrier In Current Trends in Applied Formal Methods 98 LNCS 1641 1999 Meine van der Meulen and K van de Wetering Requirements Specification NSS October 19th 1998 G Wimmel Using SATO for the Generation of Input Values for Test Sequences Master s thesis Technische Universit t M nchen 2000 Pierre Wolper Expressing interesting properties of programs in propositional temporal logic In Proc 13th ACM Symp Principles of Programming Languages pages 184 193 ACM Press 1986 H Zhang SATO An efficient propositional prover In William McCune editor Proceedings of the 14th International Conference on Automated deduction volume 1249 of LNAI pages
81. over temporal operators and model selectors there is no additional grammar required for properties Note Since identifiers in QuestF must not contain blanks properties must not contains identifiers with blanks Since qualified names contain the name of the project and the name of all components these names must not contain blanks as well if qualified properties should be stored or loaded 17 3 6 Correctness Conditions The most important correctness condition for expressions in QuestF is type cor rectness Furthermore input and output ports must not be confused An additional source of errors are reference problems for example to non existing attributes of components or due to wrong qualified names Some of these errors are detected when the model is used i e when the model is exported or translated This causes exceptions that point to the invalid references 3 7 Integration and Application The QuestF languages cannot be type checked in the AUTOFOCUS tool However when importing a model into the model browser type checks can be applied 3 8 Predefined Elements In this section we describe the predefined elements of QuestF 3 8 Types The following data types are predefined in QuestF e Bool boolean Boolean with True False and true false e Int int with 0 1 1 e Float float with 0 0 e a b for functions from type a to type b e Channel m NoVal Msg Val m The type Bool can be translated
82. pattern Money m and e the reconditionm lt 0 holds For example the transition cannot be executed if x has no value or MailSent or Money 100 In the case x has the value Money 0 the transition can be executed and sends the value 0 to the port s Type definitions can also be used to define polymorphic types for example lists by gt The transition variable m is instantiated to the value 0 during the pattern matching of the conditions 12 data List a Nil Cons first a rest List a In this definition two selector functions are defined first List a gt aandrest List a gt List a Both are partial functions and can only be applied to list elements constructed with Cons Therefore type definitions introduce predicates discriminator functions is Nil and is Cons The se mantics of discriminator and selector functions are see Section 3 3 for function definitions generated selector functions fun first Cons x1 x2 xl fun rest Cons x1 x2 x2 generated discriminator functions fun is Nil Nil True is Nil x False fun is Cons Cons x1 x2 True is_Cons x False For model checking finite types are required Therefore the type definitions must not be recursive i e the defined type must not occur in the definition For example the above type List is not finite Furthermore polymorphic types cannot be used for model checking The gram
83. place the objects in the abstract system by one of its preimages in the concrete system i e we have to invert the abstraction function Since the inversion of the abstraction function may lead to many preimages the test might require to back track among the different alternatives until the error is located within the concrete model 2 If no error can be found when simulating the system the error is if all relevant cases have been considered in the abstraction function In 36 this case the abstraction should be improved The simplest possibility is to come up with a completely new abstraction function that works in the desired way However there are several more refined possibilities for such an improvement See M l98b for details When repeating this step this results in an incremental process that finally reaches an appropriate abstraction e The correctness of this abstraction function then should be shown by theorem proving In the context of Quest this should be done by the VSE II tool component The criteria for the correctness of the abstraction functions abs are 1 if s is an initial state the abs s is also an initial state in abs s 2 if t is a successor of s the abs t is a successor of abs s See M l98b for the mathematical definitions of the correctness and Ap pendix C 1 for an example This methodology enables the reuse of simple abstraction functions in order to come up with a powerful and su
84. priate phase Note that in the example below the Compute action is empty because for simplicity reasons no automaton for Connectionl is included Initially the schedulePhase is set to T as the global phase sync is set to InitSync so that there is a defined value The scheduler then enters an endless loop where it tries to enter the next phase by setting sync to BSync It waits for a Ok from the barrier and then executes the appropriate action After this it signals the end of his phase to the barrier In TLSPEC Connection the ports Answer inp and CAck of its component are defined The type of these ports is derived from the appropriate channel type see Section 8 2 3 For all out ports an internal port is defined which is used as a buffer of length one The Next Step action and the coding of the automaton of Connectionl is missing in the example below see Section 8 2 2 This 50 action uses the internal ports for storing the computed results The CopyPorts action copies these results to the external ports which can be seen from other components AutoFocus Scheduler for Component Connectionl x TLSPEC Connectionl_Scheduler PURPOSE AutoFocus Scheduler for Component Connection USING ImportDataTheories Natural Boolean AF_Sync MAINCHANNEL INCLUDE AF_Component Connectionl DATA OUT schedulePhase bool SHARED INOUT sync tsync ACTIONS WaitOk sync ok AND UNCHANGED schedulePha
85. project Quest These examples are part of the distribution and can be used to test the tool There are three case studies each of them has some examples Further work on the case studies is mentioned in Appendix B 4 To run an example the QML representation has to be loaded from the Examples directory of Quest 84 1 Storm Surge Barrier A model of the emergency closing system of storm surge barrier in the Oostershelde The presented models have been used in 1998 to improve the specification of the system which now has evolved further e StormSurgeBarrier SSB Version without initialization close to original specification e StormSurgeBarrier QSS a version with initialization like the running FriscoF simulation e StormSurgeBarrier Comparator two models of a compara tor with different types See Appendix B 1 for a description of this case study 2 The Banking System presented at the FM99 with two examples e The complete model FM99 FM99 contains the complete specification e The abstract model FM99 BankAbs contains a version with only sin gle valued types This is an ad hoc abstraction of the model and can be used to model check the complete system See Appendix B 2 for a description of this case study 3 A Traffic Light Control System The old AUTOFOCUS example of the traf fic light system for a pedestrian crossing over a street HMS 98 has been re modelled using the expressive power of functional data types e Traf
86. ral require interactive proof techniques In a second step the smaller system A is analyzed using automatic tools Usually the smaller system A is obtained by partitioning the state space of C via a function h between the two state spaces CGL92 If h is a homomorphism 35 i aut tem po ox wea ren Figure 12 Abstraction abstraction function the abstraction is guaranteed to be sound i e if the abstract system satisfies a property so does the original system In the following we sketch how those abstraction techniques could be integrated into the process model and tool environment of Quest We propose the follow ing methodology that allows to generate appropriate abstractions incrementally It is an instance of the more general methodology for abstractions developed in M l98b e Start with a primitive abstraction function for a safety property e If model checking fails the reason may be either that the desired property is refuted already or that the abstraction is not sophisticated enough This question should be answered by testing simulating the generated counterex ample w r t the original automaton 1 If we feel that the generated counterexample is indeed a counterex ample in the concrete system we have to check this in the concrete system Here we have to consider that the generated counterexam ple is given in terms of the abstract system i e in order to run it on the concrete system we first have to re
87. s are not checked Changes there will be ignored without warnings 8 3 2 STD For the retranslation of STDs only the following parts are recognized Location Specification part Component States States Component Transitions with preconditions input patterns output actions and actions All retranslated automatons are flat even if the original automaton was an hierar chic one All view informations e g positions of the drawn ellipsoids are lost 8 3 57 DTD The retranslation of data types is restricted to the subset of the generated con structs and requires that the theories have the structure as described in the gener ation in Section 8 2 3 Furthermore pattern matching definitions cannot be infered from the case distinctions Compared which the large possibilities VSE II offers to define data types this s quite restricted however the retranslation can be used to integrate changes into the Quest data definitions or as a starting point for further developments that can be used for round trip engineering Due to the semantical differences synchronous vs asynchronous between AUTO Focus Quest and VSE II property translation generates very complex terms that correspond to the properties Up to now there is no method in VSE II to deal 712 with such synchronous properties Therefore no retranslation of properties is supported 9 The Test Environment 9 1 Introduction The test environment
88. se sync CopyPorts Copy AF Component CopyPorts AND schedulePhase T AND UNCHANGED sync Compute Compute schedulePhase F AND UNCHANGED sync SPEC INITIAL BEGIN 51 schedulePhase T Compute sync InitSync END TRANSITIONS BEGIN WHILE TRUE DO sync BSync WaitOk IF schedulePhase T THEN Compute ELSE Copy FI sync ESync Waitok OD END schedulePhase sync AF_Component AFi_ControlState inp AFi_inp CAck AFi_CAck TLSPECEND AutoFocus Component Connectionl XI TLSPEC Connectionl PURPOSE AutoFocus Component Connectionl USING ImportDataTheories Natural MAINCHANNEL DATA PortDeclarations IN Answer Channel_Message ChannelBase Channelm OUT inpl Channel_Info ChannelBase Channelm OUT ClAck Channel_Signal ChannelBase Channelm 52 inp1 Info T1in Info Q T1out Message O Answer1 Message C1Ack Signal Figure 22 Central PortDeclarations internal ports INTERNAL AFi inp Channel Info ChannelBase Channelm INTERNAL AFi_CAck Channel Signal ChannelBase Channelm ACTIONS CopyPorts inpl AFi inpl AND CAck AFi CAck AND UNCHANGED AFi inpl AFi_CAck Automaton definition is missing for simplicity reasons TLSPECEND The component Central is decomposed in two components Driverl and Database see Fig 22 So the component
89. self is started some heuristic checks are done e Type correctness every selected node is type checked e Completeness all nodes used by a selected node are selected too e Coherence only one root node is selected All other nodes are reachable from the root node If a check fails the user is warned but may proceed anyway The start of the retranslation program can be configured via the environment vari ables VSE2AF_B as N and VSE2AF PAR The translation program will be started SVSE2AF BIN SVSE2AF PAR tmp vse2af out See below and Section A for further information on the translation program and how the environment variables should be configured 30 Retranslation If you have exported VSE objects with File only or you want to retranslate an existing VSE SL file to Quest you can use the command vse2af lt VSE filename gt QML filename The filename of a VSE SL file and the filename to which the translation should be written have to be specified Import After these steps the resulting AUTOFOCUS repository file can be im ported to AUTOFOCUS or to the Quest tools 5 2 4 Limitations The retranslation from VSE to Quest is limited to VSE SL specifications which are similar structured like those generated from AUTOFOCUS Quest specifica tions For more details see Section 8 6 Model Checking with AUTOFOCUS In this section we describe how to use model checking with the models of AUTO Focus The d
90. t from Function AUTO FOCUS Quest creates a new component in the Test data folder The new com ponent has the same name and interface as the function definition and its associ ated automaton consists of one single state and a loop transition for each defining equation The automaton reflects the behavior of the function definition except for the sequence of the equations resp transitions In function definitions the order is significant whereas the choice fo the transitions in an automaton may be non deterministic 9 2 4 Deriving sequences from test automata For the derivation of suitable test sequences AUTOFOCUS Quest provides the tran sition tour algorithm The transition tour algorithm computes a path of minimal length that covers all transitions of the automaton Note that the automaton must 77 be strongly connected i e all states must be reachable from each state otherwise the algorithm fails In order to start the transition tour algorithm just mark the desired automaton and click on Testing gt Compute Transition Tour If the automaton is strongly connected the transition tour algorithm produces an EET that represents a test which covers all transition of the automaton 9 2 5 Test Basis EETs All tests are stored as EETs Therefore it is possible to use manually created EETs for testing This is especially useful for the system test EETs from use cases are a good source for creating tests for the system test Beyond that regr
91. tem running on a PDP11 is out dated However since several flaws have been found and due to several other reasons the emergency closing system is designed in a different way Therefore the case study in the presented version can be published see vdMC99 B 1 1 The Original Model The original model is contained within the file SSB The model correspond to the original specification from the SIMTECH company in vdMvdW98 It contains the unexpected behaviour that at the system is started the output of the channel notCLOSE is not present This denotes that the close signal is given and the barrier closes With an initialization phase this unexpected behaviour could be avoided This unexpected behaviour was found during simulation of the system Furthermore the model contains the famous vdMC99 bug in the statemachine that can be found using model checking 86 B 1 2 An Improved Model The improved model is contained within the file OSS In this model we integrated an initialization phase and fixed the bug of the statemachine using a boolean vari able closeHappened to store whether a close signal has occured in the system run This model has been described very detailed in Gie99 B 1 3 A Comparator for Sensor Signals To illustrate the abstraction mechanisms and the generation of proof obligations for the correctness of the abstraction functions a comparator for sensor signal has been modelled The abstract model of the co
92. the input pattern the outputs and the actions are added An extra transition the IdleStep is added after the other transitions If for a compute phase no transition could be taken then the automaton stays in its current state the local variables are unchanged and the out variables are set to NoVal So the condition for an IdleStep is the negotiation of all preconditions and all input patterns of all transitions The Next Step ac tion calls one of the transitions or the IdleStep and so performs one reaction of the automaton Initially the control state and the local variables and the out variables of the component are set appropriate AutoFocus Scheduler for Component Driverl S TLSPEC Driverl Scheduler PURPOSE AutoFocus Scheduler for Component Driverl USING Natural Boolean MAINBankSystem Module MESSAGE AF Sync INCLUDE AF Component Driverl DATA OUT schedulePhase bool SHARED INOUT sync tsync ACTIONS WaitOk sync ok AND UNCHANGED schedulePhase sync CopyPorts Copy AF Component CopyPorts AND schedulePhase T AND UNCHANGED sync Compute Compute AF Component NextStep AND schedulePhase F AND UNCHANGED sync SPEC 61 INITIAL BEGIN schedulePhase T Compute sync InitSync END TRANSITIONS BEGIN WHILE TRUE DO sync BSync WaitOk IF schedulePhase T THEN Compute ELSE Copy FI sync ESync WaitOk
93. this section we describe some technical details of these con nections that are not relevant to the user of AUTOFOCUS Quest but they help to understand intermediate files that are generated and not removed for documenta tion Furthermore it might be interesting for experts to see and edit the generated files and to restart model checking 6 3 1 Using SMV After the determination of the maximal time a progress control window appears that contains information of the current steps This window disappears after the maximal time or if cancel is pressed An example for this window is in Figure 11 For experts the SMV Translation is done in four automatic steps with three intermediate files that can be inspected 33 H Checking FM99Abs 100 seconds 0 l s exporting model 42 2 s eliminating functions 42 3 s starting SMV 46 9 s processing SMV result specification AG Tilll quest port out D gt AF Connectio specification AF O is false resources used user time 3 39 s system time 0 045 BDD nodes allocated 138000 Bytes allocated 3801088 BDD nodes representing transition relation 99116 22 resources used usertime 3 45 s system time 0 05 s BDD nodes allocated 138000 Bytes allocated 3801088 BDD nodes representing transition relation 99116 22 49 9 s SMV run finised 4 Figure 11 Model Checking Information 34 1 name names name mapping from AUTOFOCUS Quest to SMV 2
94. to VSE and can be used for model checking Float and higher order functions like in ML are not supported within SMV and VSE The type Int is restricted to a finite domain for model checking rang ing from 0 to MazJnt a value that can be defined in the model browser The polymorphic type Channel m must not be used in AUTOFOCUS In QuestF it is used within properties for example to express x by is NoVal x In the Allowing alternative syntactic forms for some types and elements makes it easier to convert projects with from other languages to QuestF format 18 translations to SMV SATO and VSE this type is used for a type correct represen tations of channels see Sections 6 and 8 3 8 2 Operations In this section we describe predefined operations and their priority that can be used to build terms Priorities range from 1 low to 4 high and can have an associativity forexample amp amp 21 denotes that amp amp has priority 2 and associates to the left The following operations are allowed on all terms e equality 11 e inequality 31 e receive 3 e send 3 The following operations are allowed on boolean terms e negation not e implication gt 1r e biimplication lt gt 1r e disjunction 11 e conjunction amp amp 21 The following operations are allowed on numeric Int and Float terms e subtraction 21 e addition 21 e greater gt 3 e greater or equal gt 3
95. tput is computed and the copy phase where the com puted output is published to the other components Each scheduled component of a system must either finish its compute phase or its copy phase before a com ponent can enter the next phase The activation of this two phases is done by the barrier The barrier has an internal variable phase which stores the current phase of the system and a counter which stores the number of components which have not finished the current phase The barrier has to methods BeginSync and EndSync The general scheme of the barrier synchronization algorithm is shown blow PROCESS Component DATA schedulePhase boolean IN SPEC WHILE true DO Barrier BeginSync schedulePhase IF schedulePhase true THEN Compute ELSE Copy H AL true FI Barrier EndSync schedulePhase schedulePhase END PROCESS Barrier DATA phase boolean INITIAL true compCounter nat INITIAL N number of synchronized components ACTIONS We use a pseudo language to shorten the description 46 BeginSync schedulePhase boolean phase schedulePhase EndSync IF compCounter 1 THEN phase phase AND compCounter N ELSE compCounter compCounter 1 FI END 8 2 Translation from AUTOFOCUS to VSE In this section the way how AUTOFOCUS Quest specifications are translated to VSE is shown As mentioned above we
96. translate SSDs STDs and DTDs to VSE 8 2 1 SSD At first we show the translation of SSDs SSDs are somehow the main part of the translation because the components contain or include all other translated parts As mentioned above in AUTOFOCUS we use a synchronous execution model while VSE is based on an asynchronous interleaving semantics So we have to use the barrier synchronization scheduling algorithm which was described above In the following examples we show how this algorithm is used concretely The first example shows a simple SSD with two components Connect ionl1 and Central see Fig 21 This is a clipping of the example presented in Section B 2 In this example we translated the SSD as if both components had an asso ciated automaton The automaton is not shown in the code example presented below First the BASIC type AF Sync is defined t sync is used for the communica tion between the barrier and the schedulers After this the global synchronization barrier BankingSystem0 Barrier is defined As in its scope there are two components its internal variable comp Counter is initialized with 2 The global phase is initialized with T which V Properties entered in the Quest Browser are also translated to VSE IINote Prefixes AF_ and AFi_ are used to mark Quest internal objects Note that sometimes numbers are appended to a name to avoid name clashes 47 inp1 Info Q Answer1 Message C1Ack Signal
97. uded in the scheduled component wrapper see Section 8 for further details Translation of selected parts To select parts of a specification which should be exported to VSE II the selector has to be started af2vse s elect useinclude withoutsubgraphs lt OML filename gt lt VSE filename gt lt PropertyFilename gt Note The start of af 2vse should be possible from the Quest Browser in later versions Note This will be possible from the Quest Browser in a later version 24 File Edit 9 IE BankingSystem 9 W Centrale Driveri E Driver2 Q Database E Process1 E Process2 Till E Connection E Till2 E Connection2 Figure 6 The Selector Note when using the selector it is not necessary to specify any filename on the command line An AUTOFOCUS Quest specification filename can be selected in a file requester later by clicking on the button Load or by selecting the Load in the File menu If properties are stored in a separate file they can load with Add Prop The selector is presented in Fig 6 There is a menu bar and a toolbar where some actions can be started All actions besides Exit which is only present in the File menu are available via the menus and via the toolbar Below the toolbar there are two panels with tabs in it On the left side objects like components automata data types and properties can be selected on the right si
98. um de proj quest In this example you have to type command in your command shell and you can give it an optional argument and you have to specify a filename Menus also appear in a monospaced font For example File Buttons are presented like this OK Cancel 2 Views and Models of AUTOFOCUS AUTOFOCUS has a view oriented structure whereas the extensions of the project Quest use the model semantics The main model of AUTOFOCUS are compo nents Within the model browser there are some additional attributes available that cannot be represented graphically within the views of AUTOFOCUS Exporting a project from AUTOFOCUS into the QML generates a model for the views and requires that the views are consistent for example each component in a SSD should have a refinement or a behaviour This can be checked using the consistency test of AUTOFOCUS see HSE97 Since the model browser and the browsers of AUTOFOCUS represent the struc tures of models and views we use them to present the structures 2 1 Structure of Views in AUTOFOCUS AUTOFOCUS has a view oriented structure see for example HMR 98 HMS 98 Every document describes a graphical view on the model The main structure of the views are the kinds they belong to There are SSDs STDs EETs and DTDs in the browser of AUTOFOCUS see Figure 2 Since the views in AUTOFOCUS are hierarchic within each document class there can be substructures Components in
99. utput This default behavior is referred to as an idle transition TLA which is used in the VSE II system is based on an asynchronous interleav ing semantics This mismatch between synchronous and interleaving semantics can be solved by augmenting the system with a scheduling algorithm In order to keep the translated specifications as modular as possible we use a hierarchic scheduling algorithm The order in which parallel components executes their re action is arbitrary So a well known scheduling algorithm the barrier synchro nization algorithm is used The connection to VSE uses only SSDs STDs and DTDs The datatype defined in DTDs are translated directly to VSE and are retranslated in a similar way from VSE The hierarchical structure of a system will be presented in VSE com pletely Behavior of an AUTOFOCUS component will be present in the appropriate VSE component 45 Each scheduled component in a group of concurrently executing scheduled com ponents perform their reaction in a sequence of phases It is required that no scheduled component begin executing its p 1 phase until all scheduled com ponents in its group have completed their p phase Each scheduled component has a variable schedulePhase which stores the phase which the scheduled component would enter For the synchronization only two different phases are needed Internally each interval is split in two phases the compute phase where the input is read and the ou

Quest UserGuide - Software and Systems Engineering

Contents

Download Pdf Manuals

Related Search

Related Contents