Home

Validas Validator Manual - Software and Systems Engineering

1. synchronized components ACTIONS BeginSync schedulePhase boolean phase schedulePhase EndSync IF compCounter 1 THEN phase phase AND compCounter N ELSE We use a pseudo language to shorten the description 81 inp1 Info Q Answer1 Message O C1Ack Signal Figure 5 15 Banking System with two components compCounter compCounter 1 END 5 6 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 translate SSDs STDs and DTDs to VSE 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 Connectionl and Central see Fig 5 15 This is a clipping of the example presented in Section A 2 In this example we translated the SSD as if both components had an associated automaton The automaton is not shown in the code example presented below Properties entered in the Quest Browser are also tran
2. AFi_Answer Channel Message ChannelBase Msg store 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 UNCHANGED AFi_ControlState Tin Answer AND NOT Channel_Info ChannelBase is_Msg Inp Channel_Message ChannelBase is_Msg Tout NOT Channel_Info ChannelBase is_Msg Inp NOT Channel Info ChannelBase is NoVal Inp hannel_Message ChannelBase is_Msg Tout OT Channel_Info ChannelBase is_Msg Inp hannel_Message ChannelBase is_Msg Tout hannel_Signal ChannelBase is_NoVal CAck OT Channel_Info ChannelBase is_Msg Inp hannel_Message ChannelBase is_NoVal Tout hannel_Signal ChannelBase is_NoVal CAck OT Channel Info ChannelBase is NoVal Inp Z A 22 2 2 2 CA A Z Z hannel_Message ChannelBase is_NoVal Tout GA ar CY MO A On Oe ZO Z hannel_Signal ChannelBase is_NoVal CAck T Channel_Info ChannelBase is_Msg Inp Channel_Signal ChannelBase is_Msg CAck is_Present Channel_Signal ChannelBase Val CAck NOT Channel_Info ChannelBase is_NoVal Inp
3. 70 34 1 MEMO gt oars 225 DARA AR 70 5 4 2 Abstraction Example Comparator 13 5 43 Using the Abstraction Chooser 75 5 5 Modal Model Checking Mucke Export 78 3 6 Conmectonto VSE gt naaa ya a 78 gt 01 Introductions sei si Nee ee 80 5 6 2 Translation from AUTOFOCUS to VSE 82 5 6 3 Translation from VSE to AUTOFOCUS 106 5 6 4 Integration in VSE oia o Sues Goes Sora kuk 107 Case Studies and Examples 117 A 1 Emergency Closing System of Storm Surge Barrier 118 A 1 1 The Original Model 119 A 1 2 An Improved Model 119 A 1 3 A Comparator for Sensor Signals 119 A 2 FM99 Banking System o 120 A 2 1 Complete Model robe taa a kite 120 A 2 2 Abstract Model o ane 121 A 3 Traffic Light Control System o kr re avs 121 Correctness of Abstractions 123 B 1 Definition of the Abstraction Function 123 B 2 Homomorphosm Proof Obligation 124 B 3 Strengthening Proof Obligation 126 Chapter 1 Introduction The Validas Validator is the implementation of the software quality framework see Figure 1 1 It provides many validation techniques that can be applied in different stages of the development process see Section 1 3 In the center of the framework is the model browser Validator that allows you to manage your models
4. e MSC The arbitrary transition mode tries to find inputs from the initial state that lead to an execution of the selected transition For this mode it is like in bounded model checking see 5 1 necessary to determine the maximal search depth i e the maximal length of the transition sequences 58 The transition sequence mode allows you to construct a sequence from transitions that should be executed These transitions have to be from one Automaton The sequence can be build by adding selected transtions to the sequence The MSC mode works with a MSC with variables 4 3 3 Usage Use the submenu Transition Checker of the menu Verify and respect the tooltips of the buttons that explain what to do 4 4 Export of Test data Exporting test sequences into test data is a powerful alternative for interactive testing It allows to generate test data for external systems as well as for the generated code C and Java 4 4 1 Method The generation of test data allows to export test data from simple MSCs Simple MSCs must not contain variables on the messages or loops and the message have to have the form with a and on the messages The test data export creates a test data file t df which has for each time interval one line of patterns of the following form lt port gt lt value gt or lt port gt lt value gt Since in the semantics of AUTOFOCUS considers all messages between two ticks of one line in the tdf file as concurren
5. MAINCHANNEL DATA INTERNAL sync_Connectionl tsync INTERNAL sync_Central tsync COMBINE 90 BankingSystem0_Barrier BankingSystem0_Barrier phase_Connectionl lt Connectionl Scheduler schedulePhase BankingSystemO Barrier phase Central lt Central Combine schedulePhas SHARED BankingSystem0_Barrier sync_Connectionl lt BankingSystem0_Combine sync_Connectionl BankingSystem0_Barrier sync_Central lt BankingSystem0_Combine sync_Central Connectionl_Scheduler Connectionl Scheduler AF Component Answer lt Central Combine Answerl SHARED Connectionl Scheduler sync lt BankingSystemO0 Combine sync Connectionl Central Combine Central Combine inpl lt Connectionl Scheduler AF Component inp Central Combine Cl1Ack SHARED Central_Combine sync lt Connectionl_Scheduler AF_Component CAck 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 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
6. SendMail WITH is SendMail Withdraw WithdrawSell Int WITH is Withdraw ViewBallance WITH is ViewBallance BASICEND BASIC InfoBase USING 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 102 with the generated discriminator and selector functions This allows us to gen erate executable algorithms for functions 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 A 2 is module TRANSACTI ON data Action SendMail data Info TA Act fun isMoneyRequest isMoneyReq end It is translated into THEORY TRANSACTI USING BOOLEAN INTEGER ActionBase InfoBase PREDICATES ON isMoneyRequest VARS VlisMoneyRequest AXIOMS FOR isMoneyRequest Withdraw Int ViewBallance tion account Int t TA Withdraw x acc True uest x False Info Inf
7. The starting options can be defined in the starting scripts see Section 2 1 3 and 2 1 3 The configuration file contains more general settings The starting op tions have priority over the configuration options The interactive options have the highest priority If a configuration item is omitted a default value is assumed The following options can be defined default values val val val val val val val idas idas idas idas idas idas idas tkeclipse C l Programme Validas prologl eclipse lib_tcl prologgen PathToPrologBin smvstart smv l reorder MaxInt 15 config validas cfg licence Val lic debuglevel 0 24 Example Windows Starting File The following File is an example for the startup of the Validator under window systems REM Validas Validator startup script for Win95 NT E Validator cfg REM Begin of configurable section REM SET JAVA_HOME C Programme JDK jdk2 2 SET VALIDAS_HOME C Programme Validas SET SMV C Programme Validas SMV smv2 5 SET SATO C Programme Validas Sato SET CTE C Programme Validas CTE SET PROLOG C Programme Validas prolog eclipse lib i386_nt SET TCL C Programme Validas Tcl bin REM SET CYGWIN C Programme cygwin usr bin REM End of configurable section RE RE REM Begin of Setting Section RE REM main
8. alidas Validator Manual Validas Model Validation AG Version 1 2 of May 25 2001 Contents 1 Introduction 7 1 1 Softwrae Quality Framework 2 22 2 o 7 ED General 4 Aa ee Se ea 7 1 3 Validation Process 222 2 228 ss AES ar here 9 1 4 Licenses Features and Bundles 10 1 4 1 Validas License Concepts sa dara ee 10 1 4 2 Validas Features and Bundles 11 14 3 Usme th Licenses es 23 00 a Haar 16 1 3 Pie ODO s io 17 2 Validas Validator 19 21 Installation shader a fa 19 211 System Requirements sea 2 a aaa Sr 3 20 212 SAMOA aa cl E pand ed 21 213 C nficutatioi s oa Dado DATA RI EETA 24 2 2 Using the Model Browser a 27 2 2 1 Starting the browser abi edi a 27 2 2 2 Working with repositories 27 2 2 3 Viewing and editing nodes 28 2 2 4 Editing Models 2 4224 44 064 a 29 225 gt Deleting nodes a ra et ee 30 2 3 The Language QuestF DTDs and Properties 30 3 2 3 1 Type Definitions 22 pa 24 o KER 30 222 O A aoe Ede Bee Bade ae Bs 32 2 3 3 Function Definitions a ic 33 2 3 4 Module Definitions 34 255 Properties wa ae e dat dale N SG 35 2 3 6 Correctness Conditions 2 22222 36 2 3 7 Integration and Application 36 2 3 8 Predefined Elements s x 2 1a van hen a 36 2 4 Integration in AUTOFOCUS 2 2 Kia are G Ve 38 2 4 1 Exporting Projects f
9. After this the appropriate generator can be started to generate a VSE SL UBR 99 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 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 2 4 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 lt VSE filename gt 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 Note The start of a 2vse should be possible from the Quest Browser in later versions 108 of an AUTOFOCUS component with its automaton will be
10. Channel_Signal ChannelBase is_Msg CAck is_Present Channel_Signal ChannelBase Val CAck Z Z O Z Z Z Z SEE A ea vi at A a UJ Jo J 000 000000000000 Z 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 100 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 SPEC AFi_ControlState sWaiting ND store NoMoney ND Tin Channel_Info ChannelBase NoVal D AFi_Tin Channel_Info ChannelBase NoVal D Answer Channel_Message ChannelBase NoVal D AFi_Answer Channel_Message ChannelBase NoVal Z Z A A A A A Z TLSPECEND DTD In this section we describe the translation of data types and functions from the Quest language see Section 2 3 to the VSE II specification language Further more 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 princ
11. 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 ELSE FALSE FI FOR AbsStates DEFFUNC AbsStates Conc IF Conc Concrete_States sMain THEN Abstract_States sMAIN FI THEORYEND B 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 VL EENE SPEC ALL Conc ConcInitial Conc gt AbsInitial AbsStates Conc correctness for transition 124 owl openDifference lt iwl IntIWL iwl IntOWL owl OPENDif Present ALL V1 lt gt Conc AFi ControlState Conc Concrete_States sMain AND V1 Conc 1 gt Conc AFi_ControlState Conc Concrete_States sMain AND Channel_Int ChannelBase is_Msg IntIWL AND Channel_Int ChannelBase is_Msg IntOWL AND Channel_Int ChannelBase Val IntOWL
12. Java 4 1 The Quest Test Environment In this section the test features build within the project Quest are described All of these features are integrated into the Validator framework 47 4 1 1 Introduction The test environment 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 4 1 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 I TS 2 TS 3 automaton TS 3 SSD STD MCETT testautomato function def TS 4 testsequentialization DID TS4 test sequence __ _ protocol EET EET Quest repository regression tests Figure 4 1 Overview about the test activities in Quest 4 1 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
13. Properties Properties describe additional features of the AUTOFOCUS models We use a sim ple temporal language to formulate the properties see Section 2 3 5 Properties are attributes of components 1 e they belong to a component they are stored and verified together with components In order to reuse Properties they can be stored in separate files extension prop 65 The property editor supports the edition of properties especially inserting specifi cation patterns inserting model elements parsing fixing searching for unbound variables and type checking Load Property Ifacomponentis selected this item is activated After choos ing a property to load the property editor is started Within the project Quest two checkers have been connected to AUTOFOCUS SMV and SATO In this sec tion we describe some technical details of these connections that are not relevant to the user of AUTOFOCUS Quest but they help to understand intermediate files that are generated and not removed for documentation Furthermore it might be interesting for experts to see and edit the generated files and to restart model checking 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 5 2 For experts the SMV Translation is done in four automatic steps
14. SATO The Validas SATO connection does no allow a maximal time greater than 60 s Transition Sequence Checker Transition Sequence Checker does no allow a maximal time greater than 60 s SMV The Validas SMV connection does no allow a maximal time greater than 60 s 12 e Java Code Generation The Validas Java Code generator does not generate code for more than three components e C Code Generation The Validas C Code generator does not generate code for more than three components The following bundles are available e New Editors for developing new models and properties Validator MSC Editor Property Editor e BSI Features the features developed for the Bundesamt fiir Sicherheit in der Informationstechnik during the project Quest Validator SMV SATO Mucke VSE Java Code Generation Transition Tour CTE Property Editor e Prototyping for developing models Validator MSC Editor MSC2STD Java Code Generation Test data Generation e All Validation Features no Prototyping Deterministic Check 13 C Code Generation Test Driver CTE Property Editor Abstraction Chooser SATO Transition Sequence Checker SMV Java Code Generation OCL Consistency Check VSE Validator ECLIPSE Test data Generation Transition Tour MSC Editor Mucke e Deluxe All Features Deterministic Check C Code
15. 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 Ingolf Kr ger Distributed System Design with Mes sage Sequence Charts PhD thesis Technische Universit t M nchen 2000 http tumb1 biblio tu muenchen de publ diss in 2000 krueger html 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 130 Mer97 MN95 M l98a M l98b Pau91 Pla97 PS99 Sad97 Sad98 SK97 SLW95 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
16. and can be loaded into the model browser as described in Section 2 2 2 Figure A 1 shows the subdirectories of the Examples directory each containing a case study Look in C Examples v rs tt bo FG CJ rmag J stomsuneBarrier EI TrafficLights File name Open Files of type All Files v Cancel Figure A 1 Content of the Examples directory A 1 Emergency Closing System of Storm Surge Bar rier 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 Note that this format has changed with Version 1 2 and the AUTOFOCUS Version 0 4 1 such that old files cannot be imported however there is a converter available Therefore most examples have a new qml file _neu 118 e SSB the original model see Section A 1 1 e OSS an improved model see Section A 1 2 e Comparator a comparator for sensor signals see Section A 1 3 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 system 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 d
17. for the mathematical definitions of the correctness and Ap pendix B 1 for an example This methodology enables the reuse of simple abstraction functions in order to come up with a powerful and sufficient 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 input and output ports types with the following informations name of the type constants and functions and a mapping from concrete to abstract values 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 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 5 4 2 we shortly present a small example for abstractions and in Section 5 4 3 we ex plain how to use the abstraction chooser 72 5 4 2 Abstraction Example Comparator The comparator has been modeled as a
18. jar 1 CLASSPATH CLASSES SSABLECC SABLEUTIL SICEBROWSER java mx100m classpath CLASSPATH OPTIONS quest testing application TiniTest 1 Example Configuration File The following file is an example for configuration file The path to this file should be specified with the Dvalidas config option or it should be called val idas cfg in the execution directory validas prologgen home oscar QUEST quest Software Tools PrologBin validas tkeclipse C Programme Validas prolog eclipse lib_tc validas smvstart smv l reorder To uninstall the validation framework tools on Unix platforms follow those steps 1 Log in as the user who installed the validation framework 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 validation framework on Windows platforms go to the Add Remove Programs dialog in the Windows Control Panel and remove the program 26 2 2 Using the Model Browser The model browser is the core of the Validas Validation Framework It is also called Validator It 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 The models are c
19. with three intermediate files that can be inspected 1 name names name mapping from AUTOFOCUS Quest to SMV 2 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 Using SATO SATO works completely automatic and does not generate inter mediate files 5 3 Determinism Checking The determinism checker allows you to detect possibly nondeterministic situa tions in your models It is fully integrated into the validator and does not use third party tools 66 Y Checking FM99Abs 100 seconds EX 0 1s exporting model 42 25 eliminating functions 42 35 starting SMV 46 9 s processing SMY result specification AG Tilll quest port out 0 gt AF Connectio specification AF 0 is false resources used user time 3 39 s system time 0 04 s BDD nodes allocated 138000 Bytes allocated 3801088 BDD nodes representing transition relation 99116 22 resources used user time 3 45 s system time 0 05 s BDD nodes allocated 138000 Bytes allocated 3801088 BDD nodes representing transition relation 99116 22 49 9 5 SMV run finised Figure 5 2 Model Checking Information 67 5 3 1 Method The determinism check checks for possible nondeterminism in the model For example one input might enable tw
20. 1009 See on in file ineg dd 2 i 4 in file eh gt Spe eg pg definition in Hie ARNING 2 in file en replaces previous definition in n tile AATRE 2 7 4 in file ee ity pl replaces previous definition in vality ineg list file dal fig Figure 4 5 TKECLIPSE for ATM Example 57 which have variables This is an automatic alternative to the manual mode using the CTE tool Test Sequence checker is based on bounded model checking and therefore re stricted to finite models For more information see Wim00 4 3 1 Installation The transition checker is based on bounded model checking and requires therefore the installation of the SATO tool 4 3 2 Method The transition checker finds input lead to the execution of certain transitions It is important to select the model of interest due to two reasons e complexity e scope The complexity of hierachical models is a product of the complexity of the sub models therefore it is more efficient to generate test cases for smaller models The scope 1 e the environment of an Automaton Component detemines the results since it restricts the possible inputs For example a timer component can be set to any value whereas a time in a specific system is mostly used only with specific values Therefore the results of the test generation can depent on the selected model There are several modes of the transition checker available e arbitrary transition e transition sequence
21. 2 1 we describe how counter examples can be visualized Section 5 2 1 In the following Section 5 2 2 and Section 5 2 2 we describe how the the different checkers can be used The technical details of the transla tions are described in other documents See PS99 for the SMV connection and Wim00 for the translation to SATO 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 63 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 MaxInt is an attribute of projects a project has to be selected The default value for MaxInt is 15 See Figure 5 1 for a changing of MaxInt 4 AWTapp Project Edit Testing Verify Options O Repository SingleAFRepository gene d Pi rties 49 GMT 03 30 1999 Q Project FM99 Q O Component BankingSystem y Port Slot y Port Slot2 t 3 Port Keypad1 D dd Define MaxInt IN Port Keypad2 HR Start SMY y Port RadiTimel Port RadioTime2 Start SATO A Defining Max Int x Enter max value for repr
22. Computer Science pages 32 45 Kathmandu Nepal December 1997 Springer Verlag Olaf Miiller 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 Science pages 1 16 Springer Verlag 1995 Olaf M ller A Verification Environment for I O Automata Based on Formalized Meta Theory PhD thesis Institut f r 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 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 B Steffen K G Larsen and C Weise A constraint oriented proof methodolo
23. Driver executes test sequences by loading Java code e Test data Generation Exports MSCs in test data format for running batch tests e Property Editor allows to specify temporal system properties e SATO connects to bounded model checker 11 Transition Sequence Checker checks if transition sequences can be exe cuted SMV connects to model checker SATO Mucke Exports to the modal y calculus model checker Mucke Abstraction Chooser help to define abstraction functions between models VSE connects to the verification support environment VSE II Java Code Generation generates Java code C Code Generation generates C code Note that the validator model browser is required for almost all features how ever there is a demo version that can be used The only exception is the C code generator it is also available as a plug in to AUTOFOCUS The following features have restricted demo versions Validator The Validas Validator does not allow to save and to export models Deterministic Check The Deterministic Check does not work for more than 20 pairs of transitions Transition Tour The Transition Tour does not generate tours for automatons with more than three states ECLIPSE works only for atomic components and does not allow to store protocols Test data Generation The Test data Generation does not generate test data for more than 20 messages Property Editor The Property Editor does not allow to save properties
24. Generation Test Driver CTE Property Editor Abstraction Chooser SATO Transition Sequence Checker SMV Java Code Generation OCL Consistency Check VSE 14 Validator ECLIPSE MSC2STD Test data Generation Transition Tour MSC Editor Mucke e Advanced Model Checking model checking and abstractions without VSE Validator SMV SATO Mucke Property Editor MSC Editor Transition Sequence Checker Deterministic Check Abstraction Chooser e Testing Validator CTE Transition Tour Test data Generation Test Driver ECLIPSE e Very Formal Verification Validator VSE Abstraction Chooser 15 OCL Consistency Check e Code Generation Validator C Code Generation Java Code Generation Test data Generation Test Driver e Model Checking Validator SMV SATO Property Editor MSC Editor 1 4 3 Using the Licenses The list of activated features is maintained in a file val lic in the directory where the program is started Do not edit this list If you start a unregistered feature you will be asked to register or to use a demo mode if present as in Figure 1 2 If you use the demo mode you will be informed on the restriction of x Licence Check ol gl 2 No licence for Validator found Figure 1 2 License Question the selected features
25. In this section we describe the translation from AUTOFOCUS to VSE and the retranslation We show how the different views of AUTOFOCUS are translated and how the retranslation works in detail 78 AbstractionChooser r 21 gt fis_Msg Comparator Combine Concrete Int IKs Msg Comparator Combine Concrete Int Val Comparator Combine Concrete IntOWL mot related I val Comparator Combine Concrete IntIWL Nival Comparator Combine Concrete IntOWL LUY An Corp pr ss a BEN Figure 5 14 Relating the Properties 79 5 6 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 cha
26. Prototyping Option Dialog Depth First Search If this is marked a depth first search is performed on the generated automaton starting with the initial state All unreachable states are then cut off Epsilon Elimination This option turned on causes the so called e elimination This algorithm eliminates empty transitions and generates and equivalent automaton Subset Construction The subset construction algorithm generates a determin istic automaton equivalent to the original automaton However this is only true for automata that only read input In this case it eliminates undetermin istic transitions with the same in and output Therefor the new automaton 44 maybe be still undeterministic The algorithm requires an e free automa ton Therefor if this feature is turned on an e elimination is automatically performed Minimization This option marked causes the automaton to be minimized The algorithm is from Myhill and Nerode It requires an deterministic e free automaton and final states Therefor all last states of the used MSCs are used as final states of the automaton Drop down box 3 possibilities Do not insert time ticks No time ticks are inserted into the MSCs Insert minimum time ticks The least possible time ticks are inserted start ing from the top Insert maximum time ticks A time tick is inserted after every message 3 3 Java Code Generation Java code generation allows to generate code
27. 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 INITIAL BEGIN schedulePhase T Compute sync InitSync END TRANSITIONS BEGIN WHILE TRUE DO sync BSync WaitOk IF schedulePhase T THEN 96 Compute ELSE Copy FI syne ESync Waitok 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 my TLSPEC Driver PURPOSE AutoFocus Component Driverl USING Natural MAINBankSystem Module MESSAGE Driverl States 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 97 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 tDr
28. 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 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 data List a Nil Cons first a rest List a In this definition two selector functions are defined first List a gt aand rest List a gt List a Both are partial functions and can only be applied to list elements constructed with Cons Therefore type defini tions introduce predicates discriminator functions is_Nil and is_Cons The semantics of discriminator and selector functions are see Section 2 3 3 for func tion definitions generated selector functions fun first Cons x1 x2 x1 n rest Cons x1 x2 x2 fu generated discriminator functions fun is Nil Nil True is_Nil x False fun is_Cons Cons x1 x2 True is_Cons x False The transition variable m is instantiated to the value 0 during the pattern matching of the conditions 31 For model checking finite
29. inlined or included in the scheduled component wrapper see Section 5 6 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 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 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 5 20 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 side 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 th
30. itself signals the end of its step to his super barrier In contrast to the root barrier which only performs SyncAll actions sub barriers have to synchronize with their super barriers So they have a TRANS schedulers 91 I ONS section like AutoFocus Barrier for Central ER TLSPEC Central_Barrier PURPOSE AutoFocus Barrier for Component Central USING Boolean Natural AF_Sync DATA SHARED INOUT sync_Driverl tsync IN phase_Driverl bool SHARED INOUT sync_Database tsync IN phase_Database bool INTERNAL compCounter nat INTERNAL endcomp bool OUT phase bool SHARED INOUT upsync tsync ACTIONS BeginSync ph IN bool phase ph AND UNCHANGED compCounter phase endcomp upsync EndSync IF compCounter 1 THEN phase phase AND compCounter 2 AND endcomp T AND UNCHANGED upsync ELSE compCounter compCounter 1 AND UNCHANGED phase endcomp upsync FI WaitOk upsync ok AND endcomp F AND UNCHANGED compCounter phase upsync sync_Driverl sync_Database 92 IN bool Sync s OUT tsync ph sl OUT tsync BSync AND BeginSync ph r s AND s OR s ESync AND EndSync AND s Ok AND UNCHANGED s1 Ok SyncAll Sync sync_Driverl sync_Database OR Sync sync Database phase Database phase Driverl sync Driverl SPEC INITIAL BEGIN compCounter endcomp F phase T sync_Driverl sy
31. openDif ference lt Channel_Int ChannelBase Val IntIWL AND Conc AFi_ControlState Conc Concrete_States sMain Vi gt AbsStates Conc AFi ControlState AbsStates Conc Concrete States sMain AND Channel SensorSig ChannelBase is Msg IWL AND Channel SensorSig ChannelBase is Msg OWL AND add Channel SensorSig ChannelBase Val OWL SOO lt lt Channel SensorSig ChannelBase Val IWL AND AbsStates Conc AFi_ControlState AbsStates Conc Concrete_States sMain correctness for idle transition in state Main ALL V1 lt gt Conc AFi_ControlState Conc Concrete_States sMain AND V1 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 Je AbsStates Conc AFi_ControlState AbsStates Conc Concrete_States sMain AND NOT Channel_SensorSig ChannelBase is_Msg IWL AND 125 Channel_SensorSig ChannelBase is_Msg OWL AND add Channel_SensorSig ChannelBase Val OWL lt lt Channel_SensorSig ChannelBase Val IWL AND AbsStates Conc AFi ControlSta AbsStates Conc Concrete_St TLSPECEND te tates sMain B 3 Strengthening Proof Obligation The strengthening proof obli
32. the retranslation of SSDs only the following parts are recognized Specification part Combine Component components and SSDs Component local variables i e internal variables except those ee AA initial values of local variables ae omponent Combine in and out variables which are retranslated to in and out ports 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 schedulers are not checked Changes there will be ignored without warnings 106 STD For the retranslation of STDs only the following parts are recognized Specification par Component 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 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 12 Furthermore pattern matching definitions cannot be infered from the case distinctions Compared which the large possibilities VSE II offers to define data
33. BankAbs an abstract model in QuestML format Both Files contain some critical properties of the system A 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 120 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 A 2 2 A 2 2 Abstract Model The file BankAbs 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 C
34. Question see Figure 3 5 with allows to select properties for nondeterministic situations the selected properties from the list of numbers no property The inserted property of the FM99 Example is not lt gt is Msg Connectionl out amp amp is_Msg Connectionl Answer 69 x Property Insertion ol Fl 4 Select the Situatians for Property generation AIT og none Figure 5 5 Property Selection for Deterministic Check 5 4 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 5 4 3 In Section 5 4 2 we present an example and the resulting proof obligations 5 4 1 Methodology The general
35. _Connectionl bool 3Note Prefixes AF_ and AFi_ are used to mark Quest internal objects Note that sometimes numbers are appended to a name to avoid name clashes 83 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 ELSE compCounter compCounter 1 AND UNCHANGED phase FT 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 SPEC INITIAL compCounter 2 AND phase T ComputePhase AND sync Connectionl InitSync AND sync Central InitSync 84 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 6 4 and the notes on useinclude In the scheduler Connectionl_Scheduler it can be seen that the des
36. an complement them manually 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 interfaces works as follows e STEP 1 produce CTA file from component interface and data type defini tions 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 startCTE in the testing menu see Fig 4 2 The cta file contains the information for the classification tree assistant in the cte 49 Praject Edit Repository Single FA Project BSIDemo L Component Cc G Port alamin G Port input G Port actionQ G Port output G Port output H Componen Read Component Classification Verify Options Create Test Automaton 5T 1999 Compute Transition Tour Create Component From Function Classify Transition Read Transition Classification Classify Component Interface Run Test FF Testdata Comp Testdata Figure 4 2 Starting the CTE It is also possible to do the steps one by one Step I is done by clicking on Classify component interface This writes out the CTA information to a file T
37. 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 5 11 the abstrac tion 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 76 AbstractionChooser EI Define Abstractians Main MAIN Cance tack efes nnnuons md peve rem os i Figure 5 11 Definition Window of Abstraction Chooser suggestion for the abstraction of types that matches to the abstracted types of the ports see Figure 5 12 If there are inconsistencies for example if the type of H AbstractionChooser EX Define Abstractians Concrete Type Name Abstract Type Name int i puna ny Figure 5 12 Selecting the Abstract Types a function abstraction does not match the type define for local variables the error is reported and the inconsistent fields are marked with red colors in the definition window see Figure 5 13 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 abstract
38. and to start the different validation steps The framework provides you with a rich set of features see Section 1 4 2 and it is constantly extended by new features see Section 1 5 1 1 Softwrae Quality Framework The framework has several connections to other tools and languages currently SMV SATO Mucke ECLIPSE VSE CTE Java C This architecture allows you to use efficient third party tools and the other tools benefit from this integra tion Therefore the list of connected tools is increasing see Section 1 4 2 In this manual we describe the usage of the validation steps and give a brief intro duction to the validation methods For more details on methods and concepts we refer to scientific publications 1 2 General 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 3 pasta EN OAFR ETT generakder Tus dem 3 Cerros Sard vatsyr ratrens Abacmcz Pater Secre EGEA ED Coronet rant pares anal Patin sacro P i ht Ct nt AS AE en AS BZ NS ee PTS oe in ie 6 ane BS rai om eit ME Ma DE PS Vente legen amet AII ewe os FPS lantarfiegnent hub Fre brnsren ania Fe pair bait Out Orr Cie at Frat horna ante eu t FS tia nw DENS Iota b tien medl DEN beaten E brak 1 Fp tene UNG TE ea Dy Merca mente Dette D etma ian op Merenge ni Til cows sarsayn m IT caco Y Und meu
39. ange 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 feasible 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 Classi
40. appropriate test sequence creation method is mainly determined by the type of the given specifi cations 1 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 we distinguish the following test bases 48 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 c
41. ard 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 A 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 e QuestTL 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 121 complexity of the state transition diagrams and increases understandability of the model The model contains several unexpected behaviours that can be found out using model checking for example the timer does not necessarily produce timeouts if it has bee
42. as depicted in Figure 1 3 before the feature is started in demo mode and you are always asked to register if you want to perform a restricted feature in the example you are prompted for registration when you want to save the model if you register you will be displayed the license condition which you should accept for further registration The next step is to enter your company name After these steps you will be asked to enter the registration key for that 16 x Demo restriction ol 71 4 Demo mode for feature Validator has restriction The Validas Validator does not allow to save and to export models Figure 1 3 Restriction for Demo Mode Validator Registration Ds 2 Validas AG oscar enter registration code for Validator Figure 1 4 Registration feature as depicted in Figure 1 4 Now you have to enter the valid key for this feature or a key for a bundle that contains the feature Otherwise registration will fail 1 5 Future Work The Validas Validation Framework has a modular architecture centered around the component oriented models of AUTOFOCUS The framework offers close connections to third party tools that thus can be integrated into the development process Validas integrates more tools into the framework especially the following features will be available e Ada code generator e connection to ATOL Ada test tools e Database foundation Co
43. bstract OPENOK Present Int2SensorSig IntOWL lt lt Int2SensorSig IntIWL gt IntOWL lt IntIWL AND Signal2Signal OPENDif Present gt OPENDif Present THEORYEND again the fact that this condition is true is expresed in atheory witha SATISFIES section THEORY OpenBarrier_Strengthen_Correct USING OpenBarrier_Strengthen_Definition SATISFIES OpenBarrier_Strengthen_Property 127 THEORYEND 128 Bibliography BLSS00 BS99 CGL92 DGG97 Gie99 GL93 GWG95 Ham98 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 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 Miinchen Susanne Graf and Claire Loiseaux A tool for symbolic pro gram ve
44. cheduler Database_Barrier Process2 Scheduler Process1 Schedule QQ _ _______ RR Figure 5 22 VSE Select Quest 114 Figure 5 23 VSE Export Quest SVSE2AF_BIN SVSE2AF_PAR tmp vse2af out See below and Section 2 1 for further information on the translation program and how the environment variables should be configured 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 lt OML filename gt 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 Limitations The retranslation from VSE to Quest is limited to VSE SL specifications which are similar structured like those generated from AUTOFOCUS Quest specifica 115 tions For more details see Section 5 6 116 Appendix A Case Studies and Examples In this section we present the examples case studies that have been modeled and checked within the 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 To run an example the QML representation has to be loaded from the Examples directory of Quest 1 Storm Surge Barrier A model of the emergency closing system of
45. ck AFi Tin Channel Info ChannelBase Msg Channel Info ChannelBase Val Inp AFi_Answer Channel_Message ChannelBase Msg Channel_Message ChannelBase Val Tout store Channel_Message ChannelBase Val Tout Driving2Driving 1 AFi_ControlState sDriving A ND D D D D AFi_ControlState sDriving Channel_Info ChannelBase is_Msg Inp Channel_Message ChannelBase is_NoVal Tout Channel Signal ChannelBase is NoVal CAck AFi Tin Channel Info ChannelBase Msg Channel Info ChannelBase Val Inp AFi_Answer Channel_Message ChannelBase Msg store UNCHANGED store Driving2Driving_2 AFi_ControlState sDriving A PPP PPP Z ND ZZZ VUVUUUOU DV AFi_ControlState sDriving Channel_Info ChannelBase is_NoVal Inp Channel_Message ChannelBase is_NoVal Tout Channel Signal ChannelBase is NoVal CAck AFi Tin Channel Info ChannelBase NoVal UNCHANGED store Driving2Waiting AFi_ControlState sDriving A gt ppp D ND N N N D D D ND ND AFi_ControlState sWaiting Channel Info ChannelBase is Msg Inp Channel Signal ChannelBase is Msg CAck is Present Channel Signal ChannelBase Val CAck AFi Tin Channel Info ChannelBase Msg Channel Info ChannelBase Val Inp AFi_Answer Channel_Message ChannelBase NoVal 99
46. cription of the component Connection 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 appropriate phase Note that in the example below the Compute action is empty because for simplicity reasons no automaton for Connection 1 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 Connectionl the ports Answer inp and CAck of its compo nent are defined The type of these ports is derived from the appropriate channel type see Section 12 For all out ports an internal port is defined which is used as a buffer of length one The NextStep action and the coding of the automa ton of Connection is missing in the example below see Section 12 This action uses the internal ports for storing the computed results The CopyPorts action copies th
47. ction 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 the abstract component from an abstraction function and 2 to define the abstraction function between a concrete and an abstract model 75 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 5 10 This requires that both compo nents the concrete and the abstract are specified within one SSD 4 AbstractionChooser ao Choose an abstract Component press Select for Abstract E Combine Campute W Concrete Select far Abstraction E Abstract Figure 5 10 Selecting the Abstract Component 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 5 11 It suggests
48. ctory has to be installed into the validator using the button Prolog Path of the menu Test ing This path is stored in the file Prolog src permanently For running ECLIPSE it is important that eclipse is included into your path Since ECLIPSE and TKECLIPSE are started and working differently under Unix and window platforms there is a difference in starting TKECLIPSE for Unix it suffices if TKECLIPSE is in the path for windows it is required that the validator knows the path to the file tkeclipse tcl which is located in the directory 1ib_tcl of your windows eclipse installation This path has to be selected using The main difference are path names While Unix ECLIPSE can read ordinary path names like usr Examples ATM the windows version requires a different format instead of C usr Examples ATM the special form C usr Examples ATM has to be used The Validator respects these differences automatically 54 the button TKECLIPSE Path of the menu Testing This path is also stored permanently in the file Prolog sre With these settings you can use the constraint based generation of test sequences 4 2 2 Usage The usage of constraint based generation of test sequences is based on a genera tion of Prolog code and constraint handlers for the system and the used datatypes The working method with Prolog is 1 generate Prolog and constraints 2 start ECLIPSE and read the model 3 generate te
49. d the MSCEditor See the presentation QuestModel ppt for an instruction how to build models with the Validator prototyping features For in serting new model elements you have to select the corresponding model element for example components can be inserted into projects and components In the menu Edit there is a submenu Insert new with a list of supported elements e Project Q O 3 ct ct xe Q Q O w w 3 u ct D D w 3 e new MSC e Code e Test e Test e Test e PrologQuery e Property e Abstraction Furthermore it is possible to create new repositories create Repository or to insert new elements of data module using the submenu New Data After the selection of a model element to insert you are asked for a new name if necessary and the element is inserted 29 Renaming nodes With the model browser nodes can be renamed Select the model element and press the Rename node Then you get a dialog that allows you to change the name of the node 2 2 5 Deleting nodes Nodes can also be deleted within the model browser To delete a node first select the desired node and then click on Delete node Be aware that all subnodes i e the subtree of the selected node will also be deleted instantaneously 2 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
50. e automatic selection mode 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 Aut oSelect 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 TNote This will be possible from the Quest Browser in a later version 8Panels are windows which are contained in a real window 109 File Edit Q KE Banking Systern Q E Centrale E Driveri E Driver2 Q Database IE Process1 E Process2 Till E Connection E Till2 E Connection2 Figure 5 20 The Selector 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 component Manual selection mode A left mouse button click deletes the selection and adds the component on which the mouse was p
51. e correctness of the concrete 119 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 5 4 2 the generated correctness conditions can be found in Appendix B A 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 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 e
52. e key for a feature e g for the validator you might also enter a valid bundle key that contains this feature In this case all other features of the bundle will also be enabled For many features there is a demo version available that allows to use the feature in a restricted mode Therefore there is only one configuration of the validation framework and different features can be enabled using different keys This allows you to enable additional features without installing additional software The Validas Validation Framework does not include licenses for other tools We tried to select public domain tools like SATO and SMV as far as possible how ever some commercial tools like VSE CTE and ECLIPSE have to be purchased independently A cooperation of with distributors of some connected tools is likely to come 1 4 2 Validas Features and Bundles The following features can be obtained from Validas e Validator model browser e OCL Consistency Check allows to define and execute using the UML ob ject constraint language e MSC Editor allows to edit MSCs for prototyping or visualization of counter examples e MSC2STD generates prototype automatons STDs from MSCs e Deterministic Check checks if the models are deterministic complete e Transition Tour computes a transition tour MSC on an automaton e ECLIPSE exports prolog constraint code for the ECLIPSE constraint solver e CTE connection to classification tree editor e Test
53. eclarations IN inpl Channel_Info ChannelBase Channelm IN ClAck Channel_Signal ChannelBase Channelm OUT Answerl Channel Message ChannelBase Channelm COMBINE Central Barrier Central Barrier phase gt 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 sync Central_Barrier sync_Driverl lt Central_Combine sync_Driverl Central_Barrier sync_Database lt Central_Combine sync_Database Driverl_Scheduler Driverl Scheduler AF Component inp lt Central Combine inpl Driverl Scheduler AF Component CAck lt Central Combine ClaAck Driverl Scheduler AF Component Answer 89 gt 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 lt Driverl_Scheduler AF_Component Tin SHARED Database_Scheduler sync lt Central Combine sync Database HIDE Central Combine sync Driverl Central Combine sync Database TLSPECEND Combine for AutoFocus Component BankingSystem TLSPEC BankingSystem0_Combine PURPOSE AutoFocus Combine for Component BankingSystem0 USING ImportDataTheories Natural AF_Sync
54. ee branch since only components of the same branch are described by an MSC You can also select only a component Then all MSCs belonging to the component are used and STDs for all subcom ponents are generated You will have to do all further described steps for each of them To make a multiple selection hold the control key down and click on the desired MSC or component After the selection is done click on Create Prototype Automaton in the menu Test 43 ing Now a dialog appears in which some options can be adjusted They will be described in section 3 2 2 After pressing the Yes button the generation starts With No can be aborted After the first automaton is generated the user is asked to select an initial state Then the optimization process is started After that is finished the new STD will appear as the automaton of the selected component If the component already has an automaton the user will be asked for permission to override it 3 2 2 Options Figure 3 1 shows the option dialog The first 4 options specify optimization algo rithms the last option how to insert time ticks Here is what they do Start Prototype Generation x Automaton will be generated far campanent Timer fram MSCs BankSystem slotasch Mar 21 2000 Please select algorithms for aptimization Y Depth First Search Y Epsilan Eliminatian zi SubSet Canstructian y Minimizatian Da not insert time ticks Yes Na Figure 3 1
55. ents THEORY MAINFM99 Module MESSAGE USING MESSAGE TRANSACTION SIGNAL 104 Chan Chan Chan el_Bool CHANNEL Bool el_Int CHANNEL Int el_Message CHANNEL Message Channel_Msg CHANNEL Msg Channel Action CHANNEL Action n n n n n Channel_Info CHANNEL Info n n n n n Channel_Keys CHANNEL Keys Channel Cardinfo CHANNEL Cardinfo Channel Card CHANNEL Card Channel Date CHANNEL Date Chan el_Signal CHANNEL Signal THEORYEND Translation of Properties Properties in AUTOFOCUS Quest hold at the speci fied states No intermediate states are possible due to the synchronous semantics of AUTOFOCUS Due to the differences in the interaction semantics synchronous asynchronous schedulers are generated for the representation of AUTOFOCUS models in VSE II see Section 5 6 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 2 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 TLSPEC Connectionl_Properties INCLUDE Proper
56. enu Select Quest with the operations Restricted and A11 see Fig ure 5 22 With A11 all objects are selected with Restricted all objects in the graph which are referenced from the actual object including the actual ob ject itself are selected Since it is not always obvious which nodes are selected you may want to choose Deselect All in Actions menu of the 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 Export Quest submenu of the VSE main window see Figure 5 23 With File only you have to start the VSE to AUTOFOCUS translation yourself if you choose Call Transformer then the retranslation to Quest is started au tomatically Before the export itself 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_BIN and VSE2AF_PAR The translation program will be started as 113 MAINBankSystem_Module_MESSAGE MAINBankSystem_Module_MESSAGE nectioni_Properti Driveri_Scheduler Database_Combine Driver2_S
57. erpreting the Results There may be three possible types of errors in the protocol EET e WRONG_VALUE_ERROR Message has a wrong value 53 e UNEXPECTED_MESSAGE_ERROR This is an 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 4 2 Constraint based Testing Constraint based testing is a very powerful feature It does use the formal se mantics of the models it can be applied to infinite systems and searching can be tailored using user defined heuristics In this section we describe how to use constraint based testing For the general methods we refer to our scientific publi cations for concrete instructions we recommend you some consulting In this section we describe installation and usage more detailed 4 2 1 Installation The generation of Prolog and the connection to ECLIPSE are part of the validator framework and therefore within the jar files The Constraint based testing uses the ECLIPSE tool and some Prolog sources The Eclipse tools can be achieved from http www icparc ic ac uk eclipse for research purposes ECLIPSE is free but not available for commercial use therefore in the future there will be a connection to Sixtus Prolog which is commercially available The Prolog sources for testing are in the directory PrologBin of your distribu tion and have to be copied to your system The path to this dire
58. ese results to the external ports which can be seen from other components AutoFocus Scheduler for Component Connectionl ar 85 TLSPEC Connectionl Scheduler PURPOSE AutoFocus Scheduler for Component Connectionl 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 schedulePhase sync CopyPorts Copy AF_Component CopyPorts AND schedulePhase T AND UNCHANGED sync Compute Compute schedulePhase F AND UNCHANGED sync SPEC INITIAL BEGIN schedulePhase T Compute sync InitSync END TRANSITIONS BEGIN WHILE TRUE DO sync BSync 86 WaitOk IF schedulePhase T THEN Compute ELSE Copy EI sync ESync WaitOk OD END schedulePhase sync AF Component AFi_ControlState inp AFi inp CAck AFi CAck TLSPECEND AutoFocus Component Connectionl ag 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 C1Ack Channel_Signal ChannelBase Channelm PortDeclarations internal ports INTERNAL AFi_inp Channel_Info ChannelBase Channelm INTERNAL AFi_CAck Channel_S
59. esentation of unsigned type Int current value 16 l Figure 5 1 Changing 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 64 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 exponential com plexity it is possible to enter a maximum time bound f
60. from executable models models that can be simulated with AUTOFOCUS The target directory and the package can be configured Furthermore the generated code can be compiled and loaded See Section 4 4 for a description of features from the code 3 4 C Code Generation C code generation can be started by selecting a component It will start the gen eration window that allows to set option The C code generator is also available as a plugin for AUTOFOCUS see Figure 3 2 Compilation of C Code is system dependent For Unix systems a compile command is printed to the stdout 45 Validas C Code Generator Figure 3 2 C Code Generator 46 Chapter 4 Testing There is a rich set of testing features integrated into the Validas Validator in cluding the generation of test sequences classifications execution of tests and generation of test input data for batch tests In this chapter we first describe Section 4 1 the testing features build within the project Quest e the transition tour for sequence generation e several classification methods based on CTE and e test execution with the test driver The following sections describe additional test features e Section 4 3 Transition Checker generates Sequences for certain transi tions based on SATO bounded model checking e Section 4 2 Constraint based Search searches with ECLIPSE Prolog for Test sequences e Section 4 4 Generation of test data for batch execution C
61. fying 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 tool 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 51 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 startCTE is sensitiv with regard to the selected node If a transition node is selected startCTE 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 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 tes
62. gation defines the mappings between the concrete and theabstract types in thefollwoing theory THEORY OpenBarrier Strengthen Definition USING OpenBarrier AbsState Definition MAINCOmparator Module HWSignal FUNCTIONS Int2SensorSig Signal2Signal SensorSig gt SensorSig Signal gt Signal VARS variables for function Int2SensorSig VlInt2Sensorsig Int variables for function Signal2Signal V1Signal2Signal Signal EINE THES cSignal Signal AXIOMS axiom for the function Int2SensorSig fun Int2SensorSig x 500 u FOR Int2SensorSig DEFFUNC Int2SensorSig VlInt2SensorSig axiom for the function Signal2Signal fun Signal2Signal x x 126 wea u r S00 mf FOR Signal2Signal DEFFUNC Signal2Signal V1Signal2Signal V1lSignal2Signal THEORYEND The corectness condition of the abstraction function with respect to the selected properties the strengthening is THEORY OpenBarrier_Strengthen_Property USING OpenBarrier_Strengthen_Definition VARS IntIWL Int IntOWL Int ls Int AXTOMS 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 lt gt Comparator Combine A
63. gy 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 131 UBR 99 vdMC99 vdMvdW98 Wim00 Wol86 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 132
64. he user interface Properties are temporal formulas over components The following temporal operators are supported e f fis 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 boolean operators for terms see Section 5 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 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 2 3 8 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 Connectionl
65. hen 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 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 4 1 2 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 4 1 2 and 4 1 3 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 50 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 ch
66. idea of abstraction is depicted in Fig 5 6 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 general 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 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 70 gt automaton temporal pos weakening strengthening Figure 5 6 Abstraction 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 i
67. 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 2 3 3 Function Definitions In the language QuestF functions can be defined by pattern matching like in func tional languages In the example of the banking system see Appendix A 2 we have the following example data Card Invalid Valid info Cardinfo dayAmount Int Date const maxAmount 2 fun maxForToday day Valid ci amt 1lastDay if lastDay day then maxAmount amt else maxAmount Ei 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 t Cons x s t Defines a concatenation operator for lists The grammar for constants and functions is 33 decl const id cterm fun cterm fundecls fundecls cterm For function definitions the form left right is required see Section 2 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 2 3 4 Modu
68. ifferent way Therefore the case study in the presented version can be published see vdMC99 A 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 vdMvdW93 It contains the unexpected behaviour that at the system is started the output of the channel not CLOSE 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 A 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 A 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 comparator 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 th
69. ignal ChannelBase Channelm 87 inp1 Info T1in Info Q Answer1 Message ES C1Ack Signal 6 1out Message Figure 5 16 Central 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 5 16 So the component Central is a combination of those two components as the root component BankingSystem is a combi nation 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 u TLSPEC Central_Combine PURPOSE AutoFocus Combine for Component Central USING gt The port inp1 of the 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 5 16 88 ImportDataTheories Natural AF Sync MAINCHANNEL DATA INTERNAL sync_Driverl tsync INTERNAL sync_Database tsync SHARED INOUT sync tsync OUT schedulePhase bool PortD
70. ion function Pattern matching for abstraction functions is not supported in this version An important 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 77 j AbstractionChooser OX Define Abstractians Concrete Variable Abstract Variable SensorSig Figure 5 13 Inconsistencies are marked with red color 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 5 14 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 5 5 Modal Model Checking Mucke Export 5 6 Connection to VSE
71. ior 1 ubComponents gt s1ze gt 0 or Automaton gt size 1 lt type gt Channel Channel_is_Bound SSD Channel is bound to one InPort and one OutPort Channel InPort OutPort have the same type Error Remedy Make sure that each channel_is associated to an InPort an OutPort of the same type as the channel channel TEOR 1 Type Text DestinationPort Type az and self Type Text SourcePort Type Tex Figure 2 4 OCL Constraint Editor 41 TestEnvironment File Options Help ATM BS Timer Component has refinement or behavior 1 FAILED Done E ATM BS Timer W ATM BS Till W ATM BS Central Property Channel Port Automaton State InterfacePoint TransitionSeg ment LocVariable DTDFile MSCThread MSC Figure 2 5 OCL Constraint Checker 42 Chapter 3 Development 3 1 MSC Editor The MSC Editor is still a prootype It can be started by double clicking on a MSC in the validator 3 2 Prototyping MSC to STD Translation Generation of State Transition Diagrams STDs from Message Sequence Charts MSC is possible according to a patented algorithm This you to create prototype automata from MSCs 3 2 1 Usage This feature allows a user to generate STDs that behave according to given MSCs The theory behind that mechanism can be found in Kr 00 Select one or more MSCs and one component for which you want to generate an automaton They have to be of the same tr
72. iple 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 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 BASIC specifications Since data types in Quest have canonical discriminators is Zero is Succ these are also gen erated The resulting VSE specification is 101 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 2 3 or data type definition that use data type definitions of the same DTD For example the DTD TRANSACTION of Appendix A 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
73. is 35 Answer NoMoney gt 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 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 2 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 2 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 2 3 8 Predefined Elements In this section we describe the predefined elements of QuestF Types The following data type
74. iverl 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 ChannelBase NoVal AND store Channel Message ChannelBase Val Tout D Waiting2Waiting AFi_ControlState sWaiting 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 98 AND Channel_Message ChannelBase is_Msg Tout AND AFi_Tin Channel Info ChannelBase NoVal AND AFi Answer Channel Message ChannelBase NoVal A ND store Channel_Message ChannelBase Val Tout Driving2Driving AFi_ControlState sDriving A ND D D D D AFi_ControlState sDriving Channel_Info ChannelBase is_Msg Inp Channel_Message ChannelBase is_Msg Tout Channel Signal ChannelBase is NoVal CA
75. l values are copied to the external out variables For every transition of the automa ton 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 automatons 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 and set appropriate and after this the precondition 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 95 AutoFocus Scheduler for Component Driverl ER 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
76. le Definitions The QuestF languages has a modular structure Every project of AUTOFOCUS 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 correspond 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 2 3 therefore it is not necessary to look at the grammar for modules in QuestF H DTD Editor lt edit gt MESSAGE EINA File Navigate Import AT Parse TA HER VIET BIEN IGEN LEER ENE Get next DTD l 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 ErrorDayLimitExcee de d fun withdrawMoney TA Withdraw x aco Money x fun other ction TA SendMailaco Mailsent other amp ction TA viewBallance acd Ballance Figure 2 3 Importing a DTD Module In the DTDs of AUTOFOCUS only tree structures are supported whereas the QuestF language supports arbitrary imports 34 2 3 5 Properties The QuestF language allows to formulate properties Properties can be defined for every component see Section 2 2 for t
77. lso runs on these systems however installation has to be done manually For this purpose a script file Val idator bat is available into which the paths of your systems have to be set The third party tools except C and Java which are available on most computers can be achieved from the following locations 19 e AUTOFOCUS freely available fromhttp autofocus informatik tu muenchen de e SMV freely available from http www cs cmu edu char126 relaxmodelcheck e SATO freely available from http www cs uiowa edu hzhang sato html e ECLIPSE freely available only for research from http www icparc ic ac uk eclipse e CTE from ATS Software GmbH and Daimler Chrysler Research e VSE II from DFKI GmbH http www dfki de In the reminder of this section the requirements and the installation for the Validas Validation Framework under Linux are described The framework is provided in zip archives and has a self installable archive included See the readme file contained in the archive for latest informations The installation of the ECLIPSE connection is described in Section 4 2 2 1 1 System Requirements The Validas Validation Framework run under Unix platforms and Windows NT Requirement 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 Validation Framework is tested with Solaris 2 6 Solaris 7 Linux Kernel 2 2 and Wi
78. m 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 80 the input is read and the output 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 1ts 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 INITIAL true SPEC WHILE true DO Barrier BeginSync schedulePhase IF schedulePhase true THEN Compute ELSE Copy FI Barrier EndSync schedulePhase schedulePhase OD END PROCESS Barrier DATA phase boolean INITIAL true compCounter nat INITIAL N number of
79. n For more information on the consistency checks see BLSS00 HSE97 2 5 2 OCL Usage To start the OCL checks load a model into the validator select a project and start the OCL environment with the command start OCL of the menu Verify Then two windpws appear e OCL constraint editor see Figure 2 4 and e OCL test environment see Figure 2 5 The constraint editor can be used to edit the consistency checks the test environ ment executes the checks and reports the evaluation The constrains are grouped to the model structures in the example we have a constraint for Component and one for Channel For the evaluation of the checks the types have to be selected in the upper left window of the test environment After the selection of the types the available checks can be selected in the lower left window The test can be started using the button check and the result is displayed in the right window Model elements that are consistent are marked green inconsistent ones are marked red 40 ConstraintEditor a Parse Save Clear Clear Scan Scan Courier 16 lt invariants gt lt type gt Component Component_has_refinement_or_behavior Description Simulation Feature Each SSDComponent has a refinement or a coresp ponding STDDocument with specified behavior Unsimulatbility Remedy Either supply a subsystem or a behaviour for the component 1n question component _has_refinement_or_behav
80. n 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 QuestTL_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 122 Appendix B Correctness of Abstractions This section contains all proof obligations that are generated for the correctness of the abstraction defined in Section 5 4 2 B 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 Il 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 123 AXIOMS FOR AbsInitial
81. n 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 replace 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 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 71 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
82. nc_Database END 2 ComputePhase InitSync InitSync TRANSITIONS BEGIN WHILE TRUE DO upsync WaitOk WHILE endcomp SyncAll OD upsync WaitOk OD END compCounter sync Driverl BSync DO EN ESync phase HIDE compCounter endcomp TLSPECEND upsync sync_Database endcomp The missing TLSPECs for the components example are similar to the TLSPECs of the c therefore not presented here 93 Driverl and Database of the omponent Connection and are MAINBankSystem_Module_ MESSAGE MAINBankSystem Module MESSAGE Tin Ex Lj Tine ai lt A X Connection2 E gt Connection1_Scheduler AA Er Driver1_Scheduler Database Combine 7 Y N Driver2_Scheduler Database Barrier Process2_Scheduler Process Scheduler Figure 5 17 Development Graph of the Banking System In Fig 5 17 the development graph of the whole example like presented in Ap pendix A 2 is shown 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 Driver is shown In Fig 5 16 the SSD of the component Central wi
83. nd 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 Verification 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 112 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 5 23 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 operation Selected nodes are displayed inverted Select operations add nodes to the already selected nodes 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 subm
84. ndix with examples concludes this manual 1 4 Licenses Features and Bundles In this section we describe the license concept of Validas see Section 1 4 1 The lists of available features and bundles is in Section 1 4 2 Usage of registration is presented in Section 1 4 3 1 4 1 Validas License Concept The Validas Validation Framework see Section 1 1 consists of several modules features that can be used in different development steps see Section 1 3 Every feature can be obtained separately see our list of prices Several bundles 1 e combinations of features are meaningful and have special prices see again our list of prices The single features do not have single version numbers There exists only one ver sion number for the whole validation framework The current Version is Version 1 2 the actual release is Release 1 2 0 The licenses are for single users however it is easy to migrate with the framework to new computers i e the licenses are not restricted to specific computers The license refers to a version and includes updates for all releases of this version For each feature there exists a key that allow to enable the feature The keys will be provided to you when you buy features For bundles also exists keys that Note that you can achieve EAL7 the highest level of Common Criteria using AUTOFOCUS and the Validas Validation Framework 10 enable all features of the bundle If you are asked to enter th
85. ndows NT 4 0 For the connection to VSE Solaris 2 5 or later 1s needed For the connection to CTE Solaris 2 5 or later or Linux Kernel 2 2 is needed e arun time version of Java 2 The Validas Validation Framework is tested with the Sun version of Java 2 JDK 1 2 2 e an unzip commando to unpack the archive containing the validator Optional requirements are e for the connection to the theorem prover VSE II version 1 02c or later 20 e for the connection to the model checkers SMV version 2 5 SATO version 3 2 e for the testing environment CTE 2 1 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 framework follow these steps 1 Unpack the archive validator zip with your favorite unzipper to a temporary directory E g on Unix like platforms cd tmp unzip validator 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 2 1 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 2 2 That di
86. nnection to the SPIN model checker new editors e more plugins into AUTOFOCUS 17 e DOORS connection import RMI export e improved installers especially for windows In a second extension step Validas will provide a Java API that allows to access the models and to write arbitrary connections Using this API many other tools can be connected from partners 18 Chapter 2 Validas Validator The Validas Validator model browser is the center of the Validas Software Qual ity Framework In this chapter general functions of the Validas Validator are de scribed see Section 2 2 Furthermore installation see Section 2 1 and other general functions are described The component oriented models consist of two important parts e the structures models and views and e the underlying data modeling language Quest F for the description of data items and atomic functions The structures for SSDs STDs EETs are stored in the qml files the DTDs are stored in _Module files The integration into AUTOFOCUS is described in Section 2 4 the language QuestF in Section 2 3 Furthermore there are consistency checks available that can be applied to ensure the static consistency of models see Section 2 5 2 1 Installation This section describes the installation of the Validator Currently there is only an installer for Unix systems Since the validator and many connected tools are also available for windows systems the validator a
87. nnel 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 output 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 Each scheduled component in a group of concurrently executing scheduled com ponents perfor
88. o DEFPRED isMoneyRequest VlisMoneyRequest lt gt 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 103 translation of polymorphic data types is supported even if the concept of pa rameterization in VSE Il 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 empty 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 if they 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 BASICEND THEORY CHANNEL PARAMS mParam USING BOOLEAN INTEGER 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 compon
89. o transitions Usually this is not desired during the design of systems and therefore this check helps to detect such situations The determinism check compares all pairs of transitions in all states of the system There are two modes available e pattern check e complete The pattern check compares only the patterns of the transitions for example the transitions n gt 0 1 Succ n and i Succ Zero would be found as nonde terministic pattern even if they are not The transitions i Zero and i Succ n would be detected to be deterministic with this check The pattern check is an ap proximation that should be used if the complete check is impossible The complete check respects generates all possible input combinations for a com ponent and evaluates the pairs of transitions Furthermore it also checks all pos sible values for local variables Due to this enumeration the complete check is restricted to finite and not to large models If the model contains integers the maximal integer value can be set similar to model checking see Section 5 2 Since not all combinations of local variables and states are possible even the com plete check might find non reachable situations To determine whether a situation is reachable model checking has to be used To make this check more comfortable properties are generated that describe the sit uations such that a counter example to these properties directly leads to the non deterministic situati
90. ode and performs backtracking if necessary 4 4 2 Usage For the export of test data s MSC has to be selected The export is started with the button Test data of the menu Generate Then the selection Menu appears x Component Selection ol 3 1 s Select the Components for Message output gr COK Cancel Left Border Right Border Figure 4 6 Component Selection for Test data Generation see Figure 4 6 The component for which the test data is generated should be selected in this dialog The next selection box see Figure 4 7 allows for further filtering for example in only input values are relevant and the output should be ignored 60 Direction Selection Figure 4 7 Message Selection for Test data Generation 61 62 Chapter 5 Verification 5 1 Bounded Model Checking SATO Connection 5 2 Model Checking SMV Connection This section different formal verification techniques that are supported by AUTO Focus All techniques use other tools that are connected by generating input for them and by retranslating the their outputs The verification tools can be started using the Verify menue of the browser that is also explained in this section 5 2 1 Model Checking with AUTOFOCUS In this section we describe how to use model checking with the models of AUTO Focus The description of properties is in Section 2 3 5 After a general in troduction Section 5
91. 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 M l98a a subset of LTL The operations for the system descriptions are close to the notations used in the AUTOFOCUS tool In the following subsections we provide syntax for the language QuestF and ex plain it by some examples of a banking system see Appendix A 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 2 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 and MailSent 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 2 3 3 30 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
92. omponent oriented models similiar to the UML RT models that are exported from the AUTOFOCUS tool 2 2 1 Starting the browser The browser does automatically come up when you start the validation framework This is under Unix done by typing startQuest On Window systems you have to tun the Validator bat from a command shell See Section 2 1 for further details on the installation 2 2 2 Working with repositories With the Files menu in the menubar you can open close save and import the repository 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 27 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 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
93. on gt 1r e biimplication lt gt 1r 37 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 e less lt 3 e less or equal lt 3 e multiplication 41 e division 41 Note that multiplication and division cannot be translated to SATO see Wim00 2 4 Integration in AUTOFOCUS 2 4 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 2 4 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 38 2 43 Limitations Due to limitations of the quest data structures and the AUTOFOCUS data struc tures some information gets lost when converting a project from Validator Quest format to AUTOFOCUS or vice versa The Quest export can not handle
94. on If the properties are true the nondeterministic situations cannot be reached 5 3 2 Usage For deterministic check the following model elements can be selected e two Transition Segments or e a State or e an Automaton or e a hierarchic Component 68 The check is started using the button deterministic check of the menu verify Then the mode choice appears see Figure 5 3 Use button of this window for some help Determinsm question A Determinism check of Campanent BankSystem compares 14 TransitionSegment pairs check patterns cancel help Figure 5 3 Selecting the Mode for Deterministic Check At the end of the check the results are displayed for example the Connection1 component of the FM99 Example as in Figure 5 4 The last question is the x o F 1 4 e Component could not be statically determined ta be determinstic possible canflicts are The following transition pairs could not be resolved Situation 1 Nondeterminstic situation in Component Connection1 with Automaton EccanmicCable State Sleeping input values out i Answer m possible Transitians out i Answer m Situation 2 Nondeterminstic situation in Component Connection1 with Automaton EccanmicCable State Dawn input values out i Answer m possible Transitions Qut i Answer m Figure 5 4 Results of Deterministic Check Property insertion
95. option Config File SET CONFIG OPT Dvalidas config VALIDAS HOM SET MAXINT OPT Dvalidas MaxInt 15 SET DEBUG OPT Dvalidas debuglevel 2 LASSPATH VALIDAS HOM SET OPTIONS CONFIG_OPT SET P SET CLASSPATH VALIDAS HOM SET CLASSPATH SET CLASSPATH REM SET JAVA COMPILER none MAXINT OPT SDEBUG_OP1 ATH JAVA_HOME bin SMV SATO CTE SPA E jars quest jar JAVA HOM HS PROI SJAVA_HOME S bin java OPTIONS classpath SCLASSPATHS quest testing applica Example Unix Starting File tion TiniTest LIDAS_ HOM LOGS TCLS E lib classes zip CLASSPATH 3JAVA_HOME lib tools jar VAI E jars sableutil jar E jars sablecc jar The following File is an example for the startup of the Validator under Unix sys tems 25 usr bin bash export PATH opt jdk1 3 bin SPATH define options CONFIG_OPT Dvalidas config pwd Validator cfg MAXINT OPT Dvalidas MaxInt 2 DEBUG OPT Dvalidas debuglevel 0 HELP OPT Dquest help file pwd Documents UsersGuide onlinehelp onlinehelp html OPTIONS CONFIG OPT S MAXINT OPT S DEBUG_OPT S HELP OPT SABLECC Tools Sablecc 2 9 sablecc jar SABLEUTIL Tools Sablecc 2 9 sableutil jar CLASSES classes CLASSES jars quest jar to test quest jar ICEBROWSER Tools ICEBrowser 4 08 icebrowserbean
96. or the checking time If 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 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 5 2 2 The Verify Menue The Verify menue supports management of properties properties abstractions tool connections SMV SATO VSE and description oriented tailoring Sequence Checking
97. ore 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 regression testing can be realized by using protocolls from former test runs as inputs 4 1 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 4 1 3 Then you can run the test as describen in Sect 4 1 3 Sect 4 1 3 gives some hints how to interpret the results of the test run The Test Object Interface see Reference Manual 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 gt 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 Int
98. ositioned A right mouse button click selects or unselects the current object under the mouse If a tree was folded all objects in 1t will be unselected With the 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 A11 button the whole specification can be selected The current selection can be deleted with the button Deselect A11 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 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 110 Figure 5 21 VSE Import Quest To export the current selection presented in the right panel choose 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 inthe File menu of the VSE main window see Figure 5 21 Then the following steps are performed 1 If the current VSE repository is no new one i e it is already saved in a gt i file then the user can choose to create a new empty p
99. 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 lever 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 5 7 The type Signal has only one OWL SensorSig OPENOK Signal IWL SensorSig Int IWL Int OPENDif Signal IntOWL Int Figure 5 7 Interfaces of Abstract and Concrete Models signal element Present to indicate that the comparison is positive The behaviour of the system is quite simple see Figure 5 8 for the concrete and Figure 5 9 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 op lt lt SensorSig gt SensorSig gt Bool fun None lt lt x False 73 owl openDifference lt iwl IntIWL iwl IntOWL owl OPENDif Presentr Figure 5 8 Concrete Beha
100. rectory 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 appropriate On Unix systems the installer stores some information in the directory binor usr bin e g an uninstall program 21 Welcome to the Quest Setup program Figure 2 1 The welcome screen of the installer 22 er New Directory ME SS usr local DIR Quest Figure 2 2 Choose a destination directory 23 export PATH Quest Home bin SPATH 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 If not already done the other programs like VSE II SATO SMV CTE ECLIPSE needed for the validation tools have to be installed now and should be added to your path settings If another user wants to run the validation tools she he should expand her his path settings appropirate and she he have to copy the file quest to her his home directory 2 1 3 Configuration There are two several to configure the Validator e via starting Options of Java Doption value e via configuration file option value e interactively The interactive settings are described in the description of the relevant features
101. rification 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 Grimm 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 schrauberiiberwachungskomponente mit Isabelle und STeP 1998 Student software development project Technische Universitat Miinchen Germany 129 Ham99 HEea96 HMS 98 HS96 HS97 HSE97 Jon93 KBRS98 Krii00 Kur87 LGS 95 Tobias Hamberger Kombination von Theorembeweisen und Model Checking fiir 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 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 F Huber and B
102. roject a If is selected then a new project with the name noname will be created and used b If 1s 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 111 a Choose to import the file b Choose 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 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 ASCH 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 recomputed from the original state and the kind of the change Original state 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 a
103. rom AUTOFOCUS 38 2 4 2 Importing Projects in AUTOFOCUS 38 243 cs RA A ser 39 2 5 Consistency Checks with OCL 39 251 OCL Method da ae SER er 40 2 32 OCL sage 4 5 is acto ne A KER 40 Development 43 3 Mar Bk Lat AL S r al a re 43 3 2 Prototyping MSC to STD Translation 43 LL gt Sag ee e e A ds BEY edel are 43 322 POS 5 806 AAA A A E AAA A 44 3 3 Java Code Generation 2 dit a ad 45 34 C Code Generation su a a u a a e OS 45 Testing 47 4 1 The Quest Test Environment 47 4 1 1 Introduction 2 ASA A a Ad 48 4 1 2 Creating Test Sequences louis 20 N Set 48 413 Performing Tests ss A ORS 33 4 2 Constraint based Testing 54 42 1 Installation su sires snigti waere 54 5 422 MUSAS DAA NR EI SH Ben 55 4 3 Transition Sequence Checker u a 2 88 resa Ta 56 ASA Installation er a a 58 432e Method sara Rog Seen a se 58 A AUS AS ao ty a As a ea 59 4 4 Export of Test data corista as 59 240 Method e sudo dida e 59 AAD SACO Dear NTT re eee 60 Verification 63 5 1 Bounded Model Checking SATO Connection 63 5 2 Model Checking SMV Connection 63 5 2 1 Model Checking with AUTOFOCUS 63 522 The Verify Menue ias an ee oR eee ae A 65 5 3 Determinism Checking suser ser ae SER ANTE a a 66 SIL Methods e id A e 68 De ae re AI A A tte p 68 5 4 Abstraction Chooser o oo
104. s If you prefer manual implementation or the use of AUTOFOCUS to build your models the Validas development modules features can be easily omitted from your process and you can select bundles of validation features so that you do not have to pay for development features see Section 1 4 for features and bundles In Chapter 4 we describe the validation steps for model based testing These steps can be grouped into three areas e classification of variables to select interesting values e determination of test sequences and e execution of tests All areas are based on the models especially the traces EETs MSCs are used to describe test sequences The testing methods use the precise formal foundation of the models but they are not completely formal In contrast to the testing methods the verification methods described in Chapter 5 are formal methods that can be applied for very critical systems or parts of them 9 The complexity of the models and the required quality assurance level determine the selection of best suited verification modules The validation framework sup ports the following verification features e bounded model checking using SATO e model checking using SMV Mucke and e interactive verification using VSE I In addition the framework contains features to define system properties define and execute consistency checks and an abstraction mechanism to reduce complex systems to simpler ones An appe
105. s are predefined in QuestF 4 Allowing alternative syntactic forms for some types and elements makes it easier to convert projects with from other languages to QuestF format 36 Bool boolean Boolean with True False and true false e Int int with 0 1 1 Float float with 0 0 e a gt b for functions from type a to type b e Channel m NoVal Msg Val m The type Bool can be translated 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 MaxInt 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 translations to SMV SATO and VSE this type is used for a type correct represen tations of channels see Sections 5 2 1 and 5 6 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 for example 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 2 3 e send 3 The following operations are allowed on boolean terms e negation not e implicati
106. si Sacro lt som gt faro dares Turetbet atar KI Furt fun kurvet ns Geet lange MN Raed Ae DEE Ada auch fi DEL Ame OASE elect DESTET er alert Ir isleri Figure 1 1 Structure of Validas Validation Framework 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 1 3 Validation Process The validation process is modular and supplements your development process according to your needs during your development process This ensures you a smooth introduction to your development process A more detailed description of the combination of the development process and formal methods can be found in BS99 The Validas Validation Framework consists of several modules features that sup port different validation steps for different stages of your development process The validation steps and the structure of this manual is grouped according to the development process In Chapter 2 we describe the usage of the Validator model browser and some general steps for managing the models and checking their consistency Chapter 3 contains the supported steps for system development These steps allow you to build models from requirements and to generate code from the model
107. slated to VSE 82 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 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 Af TLSPEC BankingSystem0_Barrier PURPOSE AutoFocus Barrier for Component BankingSystemO USING Boolean Natural AF_Sync DATA SHARED INOUT sync_Connectionl tsync IN phase
108. st sequences according to your test goals 4 export test sequences in msc format same as qm1 format 5 import test sequences into the validator using the button Import MSC from the menu File For the generation you have to select a component in a loaded model and to press the button Export to Prolog of the menu Testing Then you are prompted to select a Prolog file name for the generation Then the following files are generated e lt file gt pl Prolog code for the model e lt file gt pl mpl meta Prolog code for the used data types This file is used to generate the constraint solvers for the data types which results into the following files e pg lt file gt chr constraint handling rules e pg lt file gt pl constraint handling rules translated into Prolog e pg lt file gt functions pl prolog code describing the available functions These files can be loaded into ECLIPSE to work with the model Starting ECLIPSE is done automatically if you select in the starting window see Figure 4 3 55 FA ECLIPSE Startup Window ole 21 19 Start ECLIPSE now Figure 4 3 starting ECLIPSE For working with Prolog it is important to make a protocol from the interactive step that lead to the generated test sequences Therefore a Prolog Protocol Pad see Figure 4 4 is started together with TKECLIPSE see Figure 4 5 The PPP allows you to copy and paste commands into the TKECLIPSE which has onl
109. 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_neu Version without initialization close to original specification e StormSurgeBarrier QSS_neua version with initialization like the running FriscoF simulation e StormSurgeBarrier Comparator_neutwo models of a com parator with different types See Appendix A 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_neu contains the complete speci fication e The abstract model FM99 BankAbs_neu contains a version with only single valued types This is an ad hoc abstraction of the model and can be used to model check the complete system 117 See Appendix A 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 TrafficLights QuestTL neu contains the model The case studies are stored within the new QuestML format and can be loaded into AUTOFOCUS and into the model browser Furthermore there are some prop erties available that can be loaded into the model browser to check something The files are located in the Examples directory see installation 2 1
110. t the order of the patterns within a line does not matter Empty lines denote empty the absence of messages A meaningful test like the generated code passes all input values of a line to a system and compares the output values of the line with the current values of the output ports Then a step of the system is executed and the next line is processed These semantics is not complete with respect to the outputs 1 e there might be more outputs than described within the test data file For the generation of test data the messages can be filtered for example only mes sages to one component of a sequence diagram might be relevant Executing test data is useful for testing the external messages of a component Therefore compo nents and messages from MSC which can contain also internal communication have to be selected 59 The following sequence demonstrates the round trip engineering for Java 1 Generate test sequences for example using the transition checker 2 Generate and compile Java code from the component 3 Generate test data into test t df same directory Select all messages of the component 4 execute the test using a Java call like java ACM components BankSystem test tdf Note that this round trip engineering works only for deterministic code since no backtracking is performed If nondeterministic code with backtracking should be tested the Quest test driver has to be used see Section 4 1 3 This driver loads the c
111. t cases cannot be reimported to AUTO FOCUS Quest correctly Test Basis Functions Function definitions are the third test basis By selecting a function definition and executing Testing gt Create Component from Function AUTO FOCUS Quest creates a new component in the Testdata 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 1s significant whereas the choice fo the transitions in an automaton may be non deterministic 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 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 52 Test Basis EETs All tests are stored as EETs Theref
112. th the component Driverl is shown In Fig 5 18 the automaton which describes the behavior of Driver1 is presented Below the VSE SL specification of the scheduler and the component itself is shown The scheduler is similar to the scheduler of component Connectionl The component Driver1 is included in the scheduler as AF Component The Compute action calls the Next Step action of the component This action per forms one step of the automaton or if no transition is possible then the IdleStep is taken The Copy action calls the CopyPorts action of the component which copies the values of the internal buffers to the out variables InDriverl States the states of the automaton Waiting and Driving are defined These are used as values for the AFi_ControlState which stores 94 Inp i CAck Present Tinli Inp CAck Present Inp Tout m store m Inp i Tout m Tinli store m Ing Tour Ansmartsore gt Inp i Tout CAck Bnli Answer store Inp i Tout m CAck Tin i Answer m store m Figure 5 18 Automaton of Component Driverl 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 12 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 interna
113. the following items e refinement of axes in EETs i e sub EETs for axes e textual annotations of all objects reuse of STDs in several components 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 2 5 Consistency Checks with OCL This section describes the OCL consistency checking feature of the Validas Vali dation framework The OCL consistency feature is still a prototype 39 2 5 1 OCL Method The OCL Obejct Constrain Language is a part of the UML unified modelling language It can be used to express constraints on models Using an interpreter and a conenction to the models these constraints can be evaluated The OCL features are based on a one of the first OCL interpreters that have been build worldwide The OCL feature allow the user to define consistenccy checks as in AUTOFOCUS but in contrast to the available checks of AUTOFOCUS the OCL feature allows to define checks on all parts of the model and it can easily use methods from the API for example to check the type correctness of a transitio
114. to the same file where it was loaded from The data module files are also saved Save repository as Save the repostitory and the data modules into a new file 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 Import MSC This feature allows to import single MSCs into repositories se lect a Component The MSC has to be in qml format and should have the exten sion msc This feature is useful for the importing of generated MSCs of third party tools in the current version of the ECLIPSE connection this is the way in which the generated test case are imported MSC messages can be exported with the Test data within the Generate in a more compact format for further processing see Section 4 4 2 2 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 28 2 2 4 Editing Models You can edit models with the model browser This is done with the menu Edit Editing models is meaningful for prototyping see Section 3 2 or doing some changes in the models Inserting nodes It is possible to develop models with the validator this can be done using the browser an
115. tyBase 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 105 TLSPECEND Again the patterns are eliminated as described for function definitions 5 6 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 fact 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 5 6 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 SSD For
116. types are required Therefore the type definitions must not be recursive 1 e the defined type must not occur in the definition For example the above type Li st is not finite Furthermore polymorphic types cannot be used for model checking The grammar for data definitions ddata is in BNF Syntax ddata data string tvars dconstr dconstr sx tvars tvar cotvar cotvar tvar tvar string dconstrs I 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 2 3 3 2 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 conditionals like if x then y else z fi where the 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 op erators see Section 5 have priorities that allow to write terms like a b c d The important grammar rules for building terms are 3The only exception is the predefined polymorphic type Channel m see Section 2 3 8 32 cterm cbase typean typean type cbase sign id param string cterm cterm infid cterm if cterm then cterm else cterm fi
117. 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 with such synchronous properties Therefore no retranslation of properties is supported 5 6 4 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 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 19 shows the process from AUTOFOCUS Quest to VSE II and back As it can be seen 107 AutoFocus gt VSE Quest Selector Generator AutoFocus Quest VSE gt AutoFocus Generator Figure 5 19 Connection AUTOFOCUS VSE 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
118. very easy to define 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 implication 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 B 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 B 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 5 4 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 be edited In this section we show how to define a new abstra
119. viour add owl S00 lt lt iwl IWL iwl 0OWL owl OPENOK Present Figure 5 9 Abstract Behaviour x lt lt None False x lt lt SNeg lse 500 lt lt 500 False S25 lt lt 500 False S25 lt lt 525 False S30 lt lt x False ll tj w x lt lt y True add SensorSig gt SensorSig gt SensorSig fun add x S00 x add S00 x x add x y None 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 74 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 B 1 one theory for the homomorphism predicate and one for the satisfies relation see Appendix B 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 5 4 3 it is
120. y one small line to accept commands in a comfortable way The PPP is initialized with the commands to set ECLIPSE options and to load the model Prolog Protocols should be saved for each component of the project separately Prolog Protocol Pad ATM neuBankSystem pl File Edit use module home oscar QUEST Testen bin operators home oscar QUEST Testen bin inequality home oscar QUEST Testen bin listc2 fhome oscar QUEST quest Examples ATM pg_atm fhome oscar QUEST quest Examples ATM pg_atm_functions home oscar QUEST quest Examples ATM atm use the following command to generate traces of length 10 init 10 use these commands for special traces and constraints doStepBankSystem stateReady stateReadyO stateMain 5 T Figure 4 4 Prolog Protocol Pad for ATM Example 4 3 Transition Sequence Checker The transition checker is fully atomic test sequence generation tool The transition sequence checker is used to find input values for transition sequences or MSCs 56 ECLiPSe 5 1 Toplevel File Tools Query Entry ee a f k set flag print depth 100000 set flag output mode mgPD set flag debug conp es 0 169 cpu SE eco cowna optimized chr ec mpiled optimized ze Spencers eco En 1 ee ter p pl cre Here i Hatch of pl p optimized sia EE 00 8 enpi pe Jona pl I eopended opt d Oe fee eg in a io seconda mpiled o ae bytes in 0 01 sec een g get ate che Be ee

Validas Validator Manual - Software and Systems Engineering

Contents

Download Pdf Manuals

Related Search

Related Contents