Home

REPORTRAPPORT

1. Weak bisimulation is then defined upon this relation and called the weak 5 We denote the largest one by Branching bisimulation first introduced in 39 and denoted by is a particular observational bisimulation refining the notion of unobservable moves taking into account the internal nondeterminism Its scheme is given by Definition 2 3 Branching Bisimulation A branching bisimulation is a binary sym metric relation R C Q such that pRq iff Va p gt a T p Rq or such that 1 q and 2 Vi 1 n peqi pRq Bisimulations are used to minimise transition systems as they define a minimal canonical form and also to compare systems Two systems are considered equivalent if and only if their respective initial states are related within some bisimulation over the product of the disjoint union of the sets of states of the two systems to compare Verification with automata widely uses these concepts for instance to check partial properties of systems and to compare an implementation with a particular specification 2 4 The ACTL Logic We now define the temporal action based and pure branching time logic ACTL 14 a logic of this type is appropriate to express properties of LTSs because its operators are based on actions Moreover ACTL is a temporal branching time logic as it has both operators for quantification over paths and linear time operators ACTL
2. The Integration Project for the JACK Environement Amar Bouali Stefania Gnesi Salvatore Larosa Computer Science Department of Software Technology CS R9443 1994 The Integration Project for the JACK Environment Amar Bouali CWI P O Box 94079 1090 GB Amsterdam The Netherlands amar cwi nl Stefania Gnesi Salvatore Larosa IE CNR via Santa Maria 46 1 56100 Pisa Italy gnesi larosa iei pi cnr it Abstract JACK standing for Just Another Concurrency Kit is a new environment integrating a set of verification tools supported by a graphical interface offering facilities to use these tools separately or in combination The environment proposes several functionalities for the design analysis and verification of concurrent systems specified using process algebra Tools exchange information through a text format called 2 Users are able to graphically layout their specifications that will be automatically converted into the F C2 format and then minimised with respect to various kinds of equivalences A branching time and action based logic ACTL is used to describe the properties that the specification must satisfy and model checking of ACTL formulae on the specification is performed in linear time A translator from Natural Language to ACTL formulae is provided in order to simplify the job to describe the specification properties by ACTL formulae A description of the graphical interface is given together with its functionalities
3. 32 33 34 35 36 14th ICSE In A Toolboz for the Verification of LOTOS Programs pages 246 261 Melbourne 1992 H Garavel and J Sifakis Compilation and verification of LOTOS specifications In L Logrippo R L Probert and H Ural editors Protocol Specification Testing and Verification X pages 379 394 North Holland 1990 J C Godskesen K G Larsen and M Zeeberg Tav user manual Internal Report 112 Aalborg University Center Denmark 1989 M Hennessy and R Milner Algebraic laws for nondeterminism and concurrency Journal of ACM 32 1 137 161 1985 P Inverardi C Priami and D Yankelevich Verifing concurrent systems in SML In SIGPLAN ML Workshop San Francisco June 1992 P Inverardi C Priami and D Yankelevich Automatizing parametric reasoning on distributed concurrent systems To appear in Formal Aspects of Computing 1993 P Inverardi C Priami and D Yankelevich Extended transition systems for para metric bisimulation In CALP 93 volume 700 of LNCS 1993 ISO Information processing systems open systems interconnection LOTOS a formal description technique based on the temporal ordering of observational behaviour ISO TC97 SC21 N DIS8807 1987 D Results on the propositional p calculus Theoretical Computer Science 27 2 333 354 1983 E Madelaine and R De Simone The FC2 Reference Manual Technical report INRIA 1993 E Madelaine and D Ver
4. C D E because we will refer to them in the following Working with MaAuTo When we have finished to use AUTOGRAPHto layout graph ically the specification we get three different outputs from the tool a PostScript one Figure 0 4 an 2 description of the automaton and a CCS MEUE specification file suitable as MAvTO input Notice that another way we can take to start the formal specification job is directly writing the controller specification in the CCS MEnuE language and using it as a MAUTO input Such a textual specification is shown in Figure 0 5 It describes the same automaton drawn by AUTOGRAPH but it is different from the automato 5 description o produced by such a tool The difference are owing to AUTOGRAPH uses only single transitions in its CCS MEUE output while the specification in Figure 0 5 sometimes uses sequences of transitions avoiding to explicitely give a name to dummy states The This way of starting the specification process has been found particulary convenient in this case because the informal specification of the system included already some state machine descriptions stopped noise noise lockfixed repaired Figure 0 4 The AUTOGRAPH controller specification parse PowerEngine let rec in 5 S sTg G1 H12 H21 G2 H23 H32 G3 gTtb gTpb gTs Tb Pb Start begin sTg test stopped
5. ACTL formulae is given by the grammar below T 9 9 0 9 0 where x X range over action formulae E and A are path quantifiers and X U are next and until operators respectively We now describe the conditions under which a state s a path of an LTS satisfies an ACTL formula a path formula written s Definition 2 8 ACTL semantics The satisfaction relation for ACTL formulae is de fined in the following way st always sk iff st ands d sk d iff nots k sE iff there exists a path II s such that o s An iff for all maximal paths II s e iff o gt 1 and o 2 R o 1 and o 2 E 9 ak ff o gt 1 and o 2 1 0 1 and 2 E 0 iff there exists i gt 1 such that o i and for alll lt j X i 1 e j 9 and e j t 1 0 TH GUY Qd iff there exists i gt 2 such that o 4 e 1 a t Roy a t 1 and for all 1 lt j lt i 2 a j 1je E469 9 Several useful modalities can be defined starting from the basic ones We write for and AX for EX 7 these are called the weak nezt opera tors e EF for E tt4U and for A tt4U these are called the eventually operators e for and AG for these are called the always operato
6. In this section we will give an example of use of the JACK environment to specify and test the behaviour of a part of a reactive system involving several functionalities from different tools The case study we chose is very simple but is a real one it is a piece of a hydro power plant control system specification Now we will give a brief description of such a plant 6 1 Presentation of the Case Study The plant is composed by a water basin from where the water flows into a number of energy production engines that convert the water mechanical energy to electrical energy Each engine has an embedded controller that can detect if the engine is working well or if a failure happens A general software control system monitors all the plant components and sends commands to the engines controllers Engine failures are dued to different reasons For example suppose that a piece of an engine gets broken the engine controller is able to detect this event and it can just signal the failure while it waits for someone repairs the broken piece This is an example of a persistent failure the controller cannot repair it it just waits for the signal the piece is repaired and then it continues to drive the engine In another situation it may happen that engine s temperature overcomes its security level this means that the engine should be put offline until its returns under that level In such a case the controller will block the engine waiting for the
7. commands is associated with this area e term file management commands for loading removing a file path name from the path name list for viewing the contain of a preselected file shortcut commands allowing the user to send a specific function of a particular tool For example if one wants to get the underlying automaton of a given term a shortcut operation is available in the interface calling MAUTO in a batch mode so not visible to the user getting directly the result without entering in a full session e commands starting a tool session initialised with some preselected term file further work is then available within that session as a normal use of the called tool This feature is provided for Pisa CRLAB MAUTO Not all the integrated tools dealing with terms currently accept this syntax However we shall provide translation functions from the Mauto syntax to these other syntaxes PREFERENCES JACK TOOL SET TERM MANAGEMENT MAUTO ftmp case_study Power ec AUTOGRAPH NLZACTL PISATOOL HOGGAR UTILITIES XTERM EDITUR LOAD VIEW CLEAR REMOVE FC2 AUTOMATON MODEL CHECKING NORMALFORM ANALYSIS TERM FILE Jtmp case study Power ec FC2 FILE MANAGEMENT LOAD VIEW CLEAR REMOVE MINIMISE MODEL CHECKING VISUALISATION ANALYSIS FC2 FILE Save Fc2 File As Ampicase study Power fc2 Figure 0 3 The JACK general control panel 5 2 Fc2 Files M
8. decreasing of the temperature the engine is not broken but it cannot be driven because it will be off line for a period of time The two examples above let us understand that two kind of failures exist one kind is related to engine failure and cannot be automatically repaired in this case we say the engine has a lock The second one is related to failures the controller can react to and this means that after a period the engine will return able to be driven in this case we say that the engine is off line The engines can produce a variable quantity of electrical power in relation with the increasing decreasing of the water flow but the flow variation does not automatically set the power output level of the engines they explicitly need commands from the control system to put themselves in states of greater less power production We assume each engine has just three productivity states to avoid a too complex specification The engine s controller can receive the following commands from the control system e inc dec to increase or decrease the energy production e start stop to start or stop the engine e test to send to the control system a signal about the engine status This signal can be one of the following pone ptwo pthree the current power production level of the engine is one of pone ptwo pthree stopped the engine is stopped offline the engine will be off line for a period locked the engine is
9. is a pure branching time logic because in its syntax each linear operator must be preceded by a branching one and vice versa this implies that only branching time properties are expressible Furthermore ACTL has an auxiliary calculus of actions embedded Here below we present the action calculus Definition 2 4 Action formulae syntax and semantics Given a set of observable actions Act the language AJ Act of the action formulae on Act is defined as follows xu tt b x xvx where b ranges over Act The satisfaction relation for action formulae is defined as follows abt always ak b uf a b a Fx iff nota if x From now on we let ff abbreviate the action formula at and y A xY abbreviate the action formula x V 7 Given an action formula x the set of the actions satisfying x can be characterized as follows Definition 2 5 AF Act 24 We define the function AF Act gt 24 as follows e k t Act b b x Act x e K x V x K x U K X Theorem 2 6 Let x AF Act then k x a Act a x Sketch of the proof The proof of this Theorem can be given by structural induction on X Definition 2 7 ACTL syntax ACTL is a branching time temporal logic of state for mulae denoted by in which a path quantifier prefixes an arbitrary path formula denoted by The syntax of
10. system The interface uses the Fc2 format see below FcTOoL works with a variety of static networks of parallel and communicating processes using symbolic techniques it allows global system computation and bisimulation minimisation of such networks The al gorithms are based on a symbolic representation of global transition systems by means of a Binary Decision Diagram BDD allowing the analysis of very large systems with a rea sonable cost in terms of time and space These two tools currently deal with strong weak and branching bisimulation but other equivalences and preorders can easily be added 4 8 The Fc2 format Each tool is presumed to have its own input and output format The Fc2 format is a common format adopted by many verification tools to describe input and output data Its main purpose is to enable communication between tools in a standardized way for instance when linking specification tools to property checking tools Historically the 2 syntax started with the efforts of some verification tool designers to be able to estabilish links between their tools This cooperation was based on the simplest exchangeable objects namely automata So the original provided syntax described these objects It has now been adopted by several tool makers and has been enriched in order to generalise the kind of objects that can be described The class of objects ranges over networks of transducers covering most kinds of input output objects
11. the user can manipulate the automata with respect to abstraction criteria or can perform their minimisation and or comparison with respect to behaviour or can produce diagnostics of equivalence checkings The verification principle can be generalised as follows First define an implementation of a system as a process algebra term involving several communicating processes running in parallel Then translate the term into a global automaton capturing all its possible com putations For partial property verification define properties with abstraction criteria abstracting the global automaton helps to verify whether the expressed property is satified by the implementation Users can also define a specification with respect to the desired external behavior using abstracted actions The global system is abstracted to meet the implementation the answer is given by bisimulation checking between the implementation and the specification The ACTL Model Checker IEI CNR AMC the model checker for ACTL logic formulae permits the validity of an ACTL formula to be verified on a labelled transition system in a linear time Whenever an ACTL formula does not hold the model checker produces a path from the LTS called a counterexample given in input which falsifies and provides useful information on how to modify the LTS to satisfy the formula This model checker allows the satisfiability of ACTL formulae on the model of a reactive system to be ver
12. to provide a general environment that offers a series of functionalities ranging from the specification of reactive systems to the verification of behavioural and logical properties It has been built beginning with a number of separately developed tools that have been successively integrated JACK covers much of the formal software development process including the formaliza tion of requirements 17 rewriting techniques 12 behavioural equivalence proofs 22 14 graph transformations 19 logic verifications 11 The logical properties are specified by an action based temporal logic ACTL defined in 14 wich is highly suitable to express safety and liveness properties of reactive systems modelled by Labelled Transition Systems The main functionalities of JACK are summarized below 1 NL2ACTL a generator of ACTL formulae that produces an ACTL formula starting from a natural language sentence NL2ACTL helps in the formalization of informal systems requirements 2 Behavioural equivalence verification by both rewriting on terms and on equivalence algorithms for finite state LTS a process algebra term rewriting laboratory CRLAB that can be used to prove equivalences of terms through equational reasoning has been integrated in JACK together with the AuTo MauTo AUTOGRAPH tool set developed at INRIA these tools can be used for the automatisation of the specifica tion and verification of process algebra terms in finite state cases S
13. write that if start is performed then lock is performed to mean that if we switch on the engine then it could get broken The above phrase does not express a possibility but a sure event To avoid natural language interpretation mistakes the tool asks the user to specify if he her whishes his her phrase refers to all the possible ways in which the engine runs or at least one of them Then Figure 0 10 the user has to specify if the action in the phrase can be performed after some other visible actions eventually or just after some unobservable actions soon the NL2ACTL translation of the above phrase is shown in Figure 0 11 Using the AMC model checker Now we are able to run AMC and check our formulae The Figure 0 12 shows a session with our model checker we input a formula to be checked and AMC displays if it is true or false The result of checking the NL2ACTL formula is obviously true suppose now we want to check if the synchronisation between the control system and the controller is consistent In particular we wish to verify that if the controller receives an engine command and starts the command execution after such execution the noise notdone notdone noise notdone notdone locked i test repaired lockfixed st_2 ko offline ee S online Figure 0 8 The reduced automaton gt if start is performed then lock is performed gt In the phrase then lock is p
14. CNR The Pisa Toot 22 23 is a system for specification verification that accepts specifications written in CCS and is parametric with respect to the properties the user wants to study This means that the user can choose a process observation function from a library of functions The represents the processes internally by the so called extended transition systems 24 i e transition systems labelled on nodes by regular expressions 8 37 36 that encode all the computations leading to the node from the starting state After the tool has converted a process into this type of internal representation the user is able to select an observation function to study interleaving causality locality and so on The process equivalences are checked through the algorithm of 32 and the implemented equivalence observations are the strong weak branching and trace ones A library of observations for studying truly concurrent aspects of distributed systems is provided moreover expert users can define their own observations The tool is equipped with a window based interface that makes the observation tasks easy Companion Tools ForooL Hocear INRIA These tools offer bisimulation min imisation procedures for systems described as a single transition system FCTOOL or networks of transition systems 5 6 HoGGAR is actually interfaced with MauTo which calls it whenever a bisimulation minimisation has to be performed on a single transition
15. Notes in Computer Science pages 37 47 Springer Verlag 1992 R De Nicola P Inverardi and M Nesi Using axiomatic presentation of behavioural equivalences for manipulating CCS specifications In automatic verification methods for finite state systems LNCS 407 1990 R De Nicola P Inverardi and M Nesi Equational reasoning about LOTOS specifi cations A rewriting approach In Sizth International Workshop on Software Specifi cation and Design pages 54 67 1991 To appear in IEEE R De Nicola and F W Vaandrager Action versus state based logics for transition systems In I Guessarian editor Semantics of Systems of Concurrent Processes Proceedings LITP Spring School on Theoretical Computer Science La Roche Posay France volume 469 of Lecture Notes in Computer Science pages 407 419 Springer Verlag 1990 R de Simone and D Vergamini Aboard auto Rapports Techniques 111 INRIA Sophia Antipolis 1989 E A Emerson Temporal and modal logic in handbook of theoretical computer science J van Leeuwen Editor Elsevier Science 1990 A Fantechi S Gnesi G Ristori M Carenini M Vanocchi and P Moreschini As sisting requirement formalization by means of natural language translation Formal Methods in Systems Design 4 2 243 263 1994 J C Fernandez H Garavel L Mounier A Rasse C Rodriguez and J Sifakis 19 20 21 22 23 24 25 26 27 28 29 30 31
16. OVE CLEAR ALL REFRESH Figure 0 12 An AMC session a part of this work to a small case study entirely treated from specification to verification in the JACK environment Several directions for future works e Improve the graphical interface in order to enrich the set of functionalities a user can have as shortcuts saving from tool session callings and command typings e Enrich tool links tool results like AMC failure path diagnostics should be dis playable within AUTOGRAPH This can be achieved by describing the path using the Fc2 syntax More generally increasing as much as possible tool cooperation by letting a tool interpreting results and diagnostics when possible e Experiment on several case studies toy or real life examples and improve the in terface on user demand e Compare our environment with other verification environments ACKNOWLEDGEMENTS The authors would like to thank Giovanni Ferro for his helpful comments and his work on interfacing AMC with the Fc2 format Rosario Pugliese for allowing us to use his speci fication as a case study R De Nicola A Fantechi P Inverardi G Ristori R De Simone and E Madelaine for their contributions on the topics of this paper REFERENCES 1 10 11 12 13 14 15 16 17 18 D Austry and G Boudol Alg bre de processus et synchronisation Theorical Com puter Sciences 1 30 1984 M Ben Ari A Pnueli and Z Manna The t
17. S ok G1 noise gTtb lock gTpb dec begin ok G1 inc begin H12 halt begin gTs test pone G1 notdone G1 ok G2 ok G1 notdone G2 noise gTtb lock gTpb inc begin H23 dec begin H21 halt begin gTs test ptwo G2 notdone G2 ok G3 ok G2 notdone G3 noise gTtb lock gTbp dec begin H32 inc begin ok G3 halt begin gTs test pthree G3 ko Tb ko Pb ok S noise gTtb lock gTpb online S test offline Tb repaired lockfixed S test locked Pb Figure 0 5 A textual controller specification audit Power add search path tmp case_study calculus meije set ccs true set debug algo true set debug cycle true set debug gc true load Power set automaton mini PowerEngine write MiniPower automaton autograph write MiniPower automaton fc2 close end Figure 0 6 script created by JACK AUTOGRAPH output saved in the file Power ec will be used in the rest of this case study Now we going to use MAUTO We can start now a MAUTO session from JACKto study some bisimulation properties of our automaton and we select the CCS MEIJE calculus from JACK s Mauro configura tion panel A MAUTO script to transform the Power ec specification into an Fc2 on
18. and the exchange format used by the tools As an example of use of JACK we present a small case study within JACK that covers both verification of a software system and verification of its properties AMS Subject Classification 1991 68N99 68Q10 68Q22 68Q60 CR Subject Classification 1991 D 2 2 D 2 4 D 2 6 F 1 1 F 3 1 Keywords amp Phrases Specification tools verification tools reactive systems integrated environment methodology bisimulation model checking Note The first author started this work while visiting the stituto di Elaborazione dell Informazione of CNR in Pisa and was funded by the European Research Consortium for Informatics and Mathematics fellowship programme The other authors were funded by the LAMBRUSCO project supported by the CNR Finalized Project for Information Systems and Parallel Computation unit operativa IEI University La Sapienza Rome 1 INTRODUCTION When the verification of system properties is an important issue automatic tools are needed Some verification environments are now available which can be used to verify properties of reactive systems specified by means of terms belonging to process alge brae and modelled by means of finite state Labelled Transition Systems automata with respect to behavioural relations and logical properties 4 9 28 38 20 18 Recently a new verification environment JACK 10 was defined to deal with reactive sytems The purpose of JACK is
19. anipulation Fc2 files represent essentially either a single automaton or a network of automata When automata are translated into the Fc2format they can be submitted to the various tools of the JACK system Like for terms JACK provides a 2 file management area see Figure 0 3 that has associated the following commands e Fc2 file management commands to load remove a file path name from the list and to view the contain of a preselected file e shortcut commands which are basically abstraction reduction of the global au tomaton a graphical panel offers to the user different choices regarding bisimula tion equivalences and a simplified edition area to set up abstraction criteria When a choice is made then either HoGGAR machinery is called if no abstraction criteria is given or else MAUTO is called which anyway calls HoGGAR to perform efficiently minimisations Of course tool executions are not visible from the user who deals just with the output Fc2 files e commands to start tool sessions initialised with a preselected Fc2 file It is the case for AMC MauTO HoGGAR AUTOGRAPH 5 9 Other Integrated Graphical Interfaces In JACK some of the integrated tools have their own graphical interface Some of them are displayed in section 6 It is the case for AUTOGRAPH which has a menu for the selection of its functions and manipulates graphical objects through a window hierarchy It is also the case for HoGGAR which has a small interfa
20. broken When the embedded controller receives an engine command i e one of start stop inc dec it must return an answer message to the control system moreover the controller must send a begin signal when it starts to execute an engine command The generic synchronisation scheme between the control system and an engine controller is 1 the control system sends an engine commend to the engine s controller 2 when the controller starts the execution of such a command then it sends begin to the control system 3 when the controller detects the engine command termination then it sends an answer to the control system Such an answer can be e ok the engine command was successfully executed notdone the command cannot be executed for security reasons there are situations in which the controller cannot obey to inc dec commands if it wants to let the engine hardware safe Moreover the controller can send asynchronous signals to the control system these ones are e ko there was a failure in the engine It could have a lock or could be off line e online the engine is again on line e lockfixed someone has repaired the engine In the following we will specify the general functionalities of an engine s embedded con troller in a formal way What we said above should be sufficient to make clear the under standing of the specification 3Notice that test does not change the engine status it simply reads it so that the
21. ce for the selection of Fc2 files and options before processing We have built during the development of JACK also a graphical interface for AMC this interface allows interactive session of the model checker making ist use easier For instance an automatic command of select load Fc2 files is included avoiding the typing of commands to the user The same for ACTL formulae which are saved in a history list after submission The history list can be displayed and the user can select one ot its element to re apply it or to slightly modify it and apply the new one Other graphical supports are available for formulae files and formulae shortcuts management 5 4 Concluding Remarks Following 11 JACK offers natural strategies using some of the differents tools it contains The specification problem is made easier by AUTOGRAPH Designing graphically networks of communicating processes save effort and is less error prone than writing terms by hand Terms are then automatically generated from specifications AUTOGRAPH provides also the translation of such a graphical design into an Fc2 file The Fc2 file can be submitted to Mauto AMC or Fcroor HogaaR The way to do is submitting the file for transition system computation abstraction minimisation to offer a reduced model for model checking and or further automata analysis When results can be saved as Fc2 files then graphical display can be performed within AUTOGRAPH 6 A CasE STUDY WITHIN JACK
22. change the power production level from the 2 level to the y level Notice that if the increasing decreasing cannot be made the controller maintains its current production level and sends a notdone to the control system It is also possible to switch off an engine when it is in one of the Gx states the controller can receive an halt command and then goes in an intermediate state gTs Generating To Stopped that represents the period needed to stop the engine in general this is not an immediate operation In the case of a start command there is a symmetrical behaviour The signals noise and lock do not come from the control system they represent events that respectively obly the controller to put the engine off line or to declare the engine locked When noise is received the controller waits for the engine stops this is rep resented by the gTtb Generating To Timed Block state and then says the control system that the engine is ko then it goes in the Tb Timed Block state waits for the noise conditions will disappear and finally it signals the engine is online again returning to the initial state S The signal lock is managed in a similar way in this case gTpb means Generating To Persistent Block when the controller is in the Pb Persistent Block state it waits for someone that repairs the engine and signals to the controller the engine is 0K again this event is represented by the repaired signal We label the states A B
23. e is shown in Figure 0 6 JACK automatically generates such a script in agreement with the user selections in the control panel shown in Figure 0 7 then JACK pipes it into MAUTO and lets the user eventually run MauTo interactively Notice that the setting of the flag ccs replaces the MEIJE semantic of the operator with that one of CCS Let s explain the script of Figure 0 6 The second step of our specification job is to study our automaton trying to reduce it in a simpler form if it is possible We use the Mauro function mini that tries to reduce the automaton associated to the PowerEngine process into a newer simpler automaton that is strongly equivalent and then observational equivalent too to the original one We need to simplify the automaton because e we can perform a better visual debugging by a second AUTOGRAPH session if we have less states to handle To do it we get a new AuTOGRAPH loadable automaton using the first write command e the task to test ACTL formulae over it will be faster The AMC tool inputs 2 files so using the last write command in the script we get the file MiniPower fc2 that contains the minimized automaton The results of the second AUTOGRAPH session are visible in the Figure 0 8 It is possible to see that the state D collapsed with the state A and the state E with the state sTg moreover notice that the state B was not necessary it could be cut so that Al Mauto Control Pan
24. ehavior to be described and to verify these properties on some system model e g a Kripke structure or a transition system 16 21 2 26 These logics are such that if a property holds in a system then that system is a model for the formula representing the property Another approach to system verification has been studied This approach is based on au tomata observations and analysis properties are also expressed as automata and equiv alence notions such as bisimulation are used to check whether a given system possesses some un desired property or not In both cases methods automatization has played an important role Due to computability problems automatic methods can only be proposed for finitely represented systems Model checking is the name for automatized verification with logics For the automata based methods a set of algorithms on graphs such as bisimulation equivalence checking forms the kernel of verification tools based on transition systems In the next section we will present the JACK system and the glue of the tools integra tion project the Fc2 automata description format 4 THE JACK INTEGRATION PROJECT The idea behind the JACK environment was to put together different specification and verification tools developed separately at two research sites IEI CNR in Italy and INRIA in France A first experiment in building verification tools starting from existing ones is described in 11 Following this first at
25. el Flags Languages Mauto File Search Path N ccs Meije fimp case_study debug algo Esterel s MiniPower aud W debug cycle Blotos MiniPower ec E debug gc CCS MiniPower fc2 melhom MiniPower ps pt MiniPower sa Power aud Power ec Power fc2 EL p gt fimp case_study Term To Study Run Mauto Reduction mini Interactive Session Automaton To Get OK g 1 all Figure 0 7 The MauTo Control Panel the edge that before was entering it now is entering the state C You can notice the way used by AUTOGRAPH to label dummy states Thus after having reduced the automaton we are ready to study it using the tools NL2ACTL and AMC that let us write and check ACTL formulae respectively Describing properties with NL2ACTL There are two ways to handle formulae The first one is to use NL2ACTL to write in natural English language the property we wish to check NL2ACTL will give us the related ACTL formula and we will be able to put it into AMC The second one is to directly use the AMC formulae editor to write the formulae related to our properties avoiding the usage of NL2ACTL A logic skilled user probably will prefer the latter way while if an user is not sure about the way to write the properties he keeps in mind s he could use the interactive and question based tool NL2ACTL In Figure 0 9 there is an example of use of NL2AC TL Here we wish to verify that if it is possible that our system crashes so we
26. emporal logic of branching time Acta Informatica 20 207 226 1983 G Berry and L Cosserat The synchronous programming language ESTEREL and its mathematical semantics LNCS 197 1984 T Bolognesi and M Caneve Squiggles tool for the analysis of LOTOS specifications In Formal Description Techiques pages 201 216 FORTE 88 1989 A Bouali Weak and branching bisimulation in fctool Technical Report 1575 INRIA 1991 A Bouali and R de Simone Symbolic bisimulation minimisation In Fourth Workshop on Computer Aided Verification Montreal 1992 G Boudol Notes on algebraic calculi of processes In K Apt editor Logic and Models of Concurrent Systems NATO ASI Series F13 1985 G Boudol and I Castellani A non interleaving semantics for CCS based on proved transitions Fundamenta Informaticae 11 4 433 452 1988 R Cleaveland J Parrow and B Steffen The concurrency workbench In Automatic Verification Methods for Finite State Systems pages 24 37 LNCS 1989 R De Nicola A Fantechi S Gnesi and P Inverardi The JACK verification envi ronment internal note Technical report I E I C N R 1993 R De Nicola A Fantechi 5 Gnesi and G Ristori An action based framework for verifying logical and behavioural properties of concurrent systems In K G Larsen and A Skou editors Proceedings of the 3rd International Workshop on Computer Aided Verification Aalborg Denmark volume 575 of Lecture
27. engine controller can immediately answer 6 2 The JACK Methodology for Formal Specification The AuToGRAPH Approach The first step in the Jack specification development system may be a graphical one we use AUTOGRAPH to draw the automaton that characterize the desidered behaviour of the controller The Figure 0 4 shows the output of the AUTO GRAPH session Now we give some explanation about the states and edges of the pictured automaton The edge labels terminated by a represent signals that our controller will output while those ones terminated by a are controller inputs Initially the engine is stopped and its controller is in the initial state S Notice that if the controller is in the state 5 and it receives a test command it will respond by sending a stopped signal To represent this synchronisation with the control system a dummy state is needed to input test and output stopped We did not want to give a name to dummy states AUTOGRAPH fills no named states with auto generated names G1 G2 and G3 Generating states correspond to the three engine power production levels When the controller is in G1 and the control system asks for decreasing the power the controller does nothing but producing synchronisation messages as in the user re quirements it behaves in the same way when it is in G3 and receives inc H12 H21 H23 and H32 are intermediate states the controller is in the state Hxy when has received the order to
28. erformed are you talking about all paths only one path Figure 0 9 A NL2ACTL session controller could be able to send a signal about the termination of such a command In ACTL language we can express it by the following formula AG E X begintrue gt EXw gi E X okv notdonetrue The results of the model checking of the formula generated by NL2ACTL and of that one above are in Figure 0 12 both formulae are signaled to be true and they are automatically recorded in a scroll panel Using AMC it is possible to create and update files of formulae and to create formulae macros to make easier the verification job It is also possible to understand why a formula is true or false on a model clicking on the button why AMC will show the path that make the formula true or false letting the user navigate in the automaton paths We have shown a relevant part of the JACK methodology if we check that our specifica tion has not a certain property using AMC we can discover which are the paths that make such a property false and after we restart the specification cycle shown in this section by reloading AUTOGRAPH from JACK and navigating in the model graph to reach the bad paths and correct them T CONCLUSIONS AND FURTHER WORK We have presented the integration project for the JACK environment for the specification and verification of concurrent and communicating systems specified by process algebra terms and modelled by
29. finite Labelled transition Systems JACK is a set of integrated tools coming from the research teams at IEI CNR and INRIA The integration is realised with a graphical interface and communication medium between the tools this medium is based on text files describing semantical objects automata networks of automata as input output of the tools using the Fc2 syntax We have displayed the configuration of the different levels of the graphical interface and dedicated gt if start is performed then lock is performed gt In the phrase then lock is performed you must specify when soon Ji eventually Figure 0 10 NL2ACTL session continued gt if start is performed then lock is performed gt RCTL Formula e 0 if start is performed then lock is performed Farseg in 2 2827 secs start E true true U lock true f CE Figure 0 11 A NL2ACTL session continued MODEL CHECKER MODE v TOPLEVEL BUILD EVAL EC2 FILE tmp case_study MiniPower fc2 ACTL FORMULA EDITOR start E true true U lackj true CHECK TRUE WHY CLEAR HISTORY MACROS EDITOR FAIRNESS EDITOR MODEL CHECKING OUTPUT Hello World Model Checker for ACTL Version 1 11alpha 10 93 automata in fc2 version 1 1 Taking input from tmp case stucdy MiniPower fc2 FORMULAE LIST US AG EXIlbegin true gt EF EX lok Inotdone true start E true true U lock true REM
30. gamini AUTO A verification tool for distributed systems using reduction of finite automata networks In S T Vuong editor Formal Description Techniques IT pages 61 66 North Holland 1990 E Madelaine and D Vergamini Finiteness conditions and structural construction of automata for all process algebras In R Kurshan editor Proceedings of Workshop on Computer Aided Verification New Brunswick June 1990 AMS DIMACS M Marino A framework for the development of natural language grammars In International Workshop on Parsing Technologies pages 350 360 Pittsburgh 1989 R Milner Communication and Concurrency Prentice Hall International Englewood Cliffs 1989 R Paige and R Tarjan Three partition refinement algorithms SIAM Journal on Computing 16 6 973 989 1987 D M R Park Concurrency and automata on infinite sequences In P Deussen editor 5t GI Conference volume 104 of Lecture Notes in Computer Science pages 167 183 Springer Verlag 1981 G D Plotkin A structural approach to operational semantics Report DAIMI FN 19 Computer Science Department Aarhus University 1981 V Roy and R de Simone n autograph primer Rapports Techniques 112 INRIA 1989 R Tarjan Fast algorithms for solving path problems Journal of the 28 3 594 614 1981 R Tarjan A unified approach to path problems Journal of the ACM 28 3 577 598 38 39 1981 P van Eijk Proceedings of the 4th internatio
31. hen we define o 1 Moreover if gt i 1 we will denote by a i the i state in the sequence 2 2 Process Algebrae Process algebrae are syntaxes for the description of parallel and communicating processes we give a brief presentation of CCS MEIJE process algebra 1 7 which is used by the JACK system for the description of reactive systems For simplicity we describe the subset of MEIJE that corresponds to the CCS process algebra following R Milner 31 Moreover we adopt the syntax used in the AvTO Mauro tools see section 5 and restrict it to their rules to guarantee the satisfiability of some finitary conditions of the underlying semantic model namely automata 15 The MELJE Syntax The MEIJE syntax is based on set of actions that processes can perform and on a set of operators expressing process behaviors and process combinations The 5 syntax permits a two layered design of process terms the first level is related to the sequential regular process description the second to a network of parallel sub processes supporting communication and action visibility filters The syntax starts from a set of labels Act as atomic signal names ranged over by alphanu meric strings such names represent emitted signals if they are terminated by the character or received ones if they are terminated by denotes the special action not belonging to Act symb
32. his action and action a e The let construct bounds non recursive definitions of process variables The Figure 0 1 shows the structural operational semantics of some CCS MEUE oper ators previously described in terms of labelled transition systems 34 note that the CCS MEIJE parallel operator operational rules are those of the CCS parallel operator whereas the MEIJE parallel operator instead has an additional rule allowing product of actions that are not necessarily co names i e a and a pape Oen re o 0 50 pp 0 0 0 0 0 0 Figure 0 1 Operational semantics of some MEIJE operators 2 8 Bisimulation Semantics We give here the definition of the bisimulation equivalence over LTSs due to Park 33 Definition 2 1 Bisimulation Given an LTS A Q Act U R a bisimulation over Q x Q is a binary symmetric relation R such that for any p q Q x Q we have pRq iff Va Act p gt 34 4 54 pRq We note by the largest such relation that is the union of all bisimulations definable over S Observational bisimulations first introduced by Milner 31 are defined through the notion of an unobservable action 7 considered as a silent step in the system behavior To abstract unobservable moves during observation we shall use the weak transition relation defined as follows Definition 2 2 The Weak Relation def T f 5 Va def 4
33. ified Requirements can also be maintained and enhanced on the basis of the results of the verification stage on the basis of the concrete model of the system and the formalization of requirements a list of temporal logic formulae the verification of the latter on the former by means of the model checker may provide useful information Model checking for ACTL can be performed with time complexity O Q x e where is the ACTL formula to be checked on an LTS that has Q states and gt arcs CRLAB IEI CNR CRLAB is a system based on rewriting strategies 12 13 The input which is supplied to the system interactively can be LOTOS 25 or CCS 31 specifications It is possible to simulate the operational behaviour of a process as well as automatically prove the bisimulation equivalence of two finite processes The bisimulation equivalences considered are the observational trace and branching ones It is also possible lIntuitively an abstraction criterion is a collection of abstract actions which are rational expressions over the concrete set of actions this is a way to express path properties with all the expressive power of rational expressions to define user driven proof strategies although no facility for this is explicitly available However a strategy to prove the equivalence of two CCS processes by transforming one process term into the other by means of axiomatic transformation is provided Pisa Toor IEI
34. liminaries We first introduce the concept of Labelled Transition System on which reactive systems are modelled and ACTL formulae are interpreted Definition 2 1 Labelled Transition System A Labelled Transition System is a 4 tuple A Q qo Act where e Q is a finite set of states We let q r s range over states e qo is the initial state e Act is a finite set of observable actions and is the unobservable action We let a b range over Act and a range over Act U T e RC Q x ActU T x Q is the transition relation Note 2 2 For C Act we let A denote the set AU For Act we let Ra q denote the set 140 there exists a A such that q a q R We will also use the action name instead of the corresponding singleton denotation as subscript Moreover we use R s to denote R4et s For A B Act we let B denote the set A B Often we simply write q for 4 0 4 c R Definition 2 3 Given an LTS A Q qo Act U R we have that e a path in A is a finite or infinite sequence q1 q2 of states such that q 1 R q The set of paths starting from a state q is denoted by II q We let range over paths e a path Il q ts called maximal if it is infinite or if it is finite and its last state 4 has no successor states i e R q 0 e if is infinite then we define o w ifo 42 qn t
35. ly specified process is called term During the specification stage the user deals with the terms in the MAUTO environment terms are parsed and syntax errors are reported In the parsing stage it is detected whether terms represent finite state systems or not just finite state systems can be studied Sufficient syntactic conditions are studied in 29 The user can then translate a term the main specification term or another one into either the Fc2 format or the AUTOGRAPH format to graphically view the specification or into other formats suitable as inputs for various other tools to carry on with the next specification and verification phases Many translation functions from algebraic objects into automata are also available so that the user can enter the MAUTO verification framework This will be descibed in the Verification Tools section NL2ACTL an automatic translator from Natural Language to Temporal Logic IEI CNR NL2ACTL a prototype translator from Natural Language expressions to Temporal Logic formulae has been developed and integrated in JACK in order to test the use of Natural Language in a friendly interface to make the expression of properties in the logic easier for the user NL2ACTL deals with sentences expressing the occurrence of actions performed by reactive systems A precise semantic meaning in terms of ACTL formulae is associated with each sentence If this semantics is not ambiguous an immediate ACTL translation is pro
36. nal conference on formal description techniques FORTE 91 In The Lotosphere Integrated Tool Environment pages 473 476 New Brunswick 1991 North Holland R J Van Glabbeek and Weijland Branching time and abstraction in bisimulation semantics extended abstract Information processing 89 G X Ritter ed Elsevier Science pages 613 618 1984
37. olising the unobservable action to model internal process commu nications we let Act Act U to denote the full set of actions that a process perform The following syntax is related to the definition of regular sequential processes R denotes a sequential process while a matches any element of Act X is a label denoting a process variable R stop a R let rec X R X R in X Here denotes an optional and repeatable part of the syntax We now explain the CCS MEIJE sequential part semantics e stop is the process without behavior e a Ris the action prefix operator e X R bounds the process variable X to the process R e R Ris the non deterministic choice operator e The let rec construct allows recursive definitions of process variables The second level of process term definition is used to design networks of parallel sub components denoted here by P where R is a sequential regular process R axP let X P and X R in X e is the parallel operator e ais the action restriction operator meaning that a can only be performed within a communication e P a b is the substitution operator renaming b into a e ax P is the ticking operator driving process P by performing action a simultaneously with any behavior of P This means that any time that process P performs an action then process P performs in parallel both t
38. pecifications are given following the syntax of some process algebra AUTO MAUTO or by means of a graphical tool AUTOGRAPH that allows the user to draw automata that are translated into process algebra terms AUTO MAUTO can then be used for formal verification and automata analysis 3 Model checking of properties expressed in ACTL on a reactive system modelled by a finite state LTS a linear time model checker AMC for the action based logic ACTL has been defined to prove the satisfiability of ACTL formulae and consequently the properties of systems 4 Analysis of concurrent systems with respect to various concurrency semantics in terleaving partial order multiset a parametric tool the Pisa has been developed that allows the user to observe many different aspects of a distributed sys tem such as the temporal ordering of events and their causal and spatial relations The paper is organized as follows Section 2 presents an overview of the syntax and semantics of the CCS MEIJE process algebra used to describe reactive sytems in JACK and of the ACTL logic An introduction to formal verification tools is given in Section 3 Section 4 gives a description of the integration project and the graphical interface of the system In Section 5 the JACK interface is described with an overview of the components of the JACK environment Finally in Section 6 we give an example of use of the JACK environment 2 BACKGROUND 2 1 Pre
39. rs e x E t gU if x ff lt gt for E t gU 9 x for lt x gt 74 e for 5 lt gt n 3 FORMAL VERIFICATION TOOLS Formal verification for reactive systems usually consists of two important stages 1 the system design specification stage 2 the properties checking stage The tools have been built following this scheme Here below we thus describe specification tools and properties checking tools 8 1 Specification Tools These tools offer functionalities to build a process specification They are often process algebra syntax compilers and make it possible to compositionally design a process term by first specifying the sub terms separately and then putting just the sub term process names in a higher term This can be done in two ways e by allowing the designer to enter a specification in a textual form e by offering sophisticated graphical procedures to construct a process specification The tool then automatically translates the drawings into a process term At this level other functionalities can be offered such as e term rewriting e finite state conditions checking 3 2 Property Checking Tools Logics have been intensively used to check the behavioural and logical properties of pro grams In particular in the concurrent systems area temporal or modal logics have been introduced in order to be able to express properties in a logical language that per mits system b
40. tempt we have developed an environment based on the links proposed in 11 and on new links that exploit the Fc2 format 27 see Figure 0 2 We had the following objectives e to provide an environment in which a user can choose between several verification tools this environment will have a simple user friendly graphic interface e to create a general system for managing any tool that has an input or output based on Fc2 format files Such tools can be easily added to the JACK system thus extending its potentiality In this sense the Fc2 format acts as a system glue Now we briefly introduce the tools that are used in the JACK system dividing them into specification tools and verification tools 4 1 Specification Tools AUTOGRAPH INRIA This is a graphic specification tool for the design of parallel and communicating processes 35 that provides functionalities for a compositional develop ment of a specification As a general rule a window is a process specification Process construction starts from automata which represent single sequential processes Processes surrounded by boxes are said to be networks and are used to hide information on low level details of a specification and to represent parallel composition If two networks are drawn at the same level they can synchronise the signals they emit and thus representing com municating processes There is no need for a network to be fully specified it could simply be an empt
41. that can be given or generated by a verification tool in the domain of finite state concurrent systems The format is organised as follows Fc2 Objects and Labels The Fc2 objects are vertices edges and nets A net is a graph containing a finite number of vertices and edges Each object has a label Objects are presented in tables An Fc2 file is thus a table of nets each net has a table of vertice each vertice has a table of edges Each object has a label A label is a record of informations each being preceded by a field name The field names are struct behav logic hook These fields are used to assign semantical information to objects For instance the field behav of an edge stands for the action label of the underlying transition Each piece of information is a string or is composed using a set of predefined operators of various arity to express simple set constructs Fc2 Nets Nets in the Fc2 format can be 1 a single LTS the net is just a table of vertices representing the set of states of the LTS and for each state vertex the set of transitions starting from that state form the edge table The minimum information label is the action name of each transition given through the field behav 2 asynchronised vector of nets in the field struct of the net the structure of the net is given listing the set of sub nets put in parallel and composing the current net The vertex table is reduced to an unique element state from which all s
42. vided otherwise an dialog with the user is started in order to solve the ambiguity In fact in our experience in the specification and verification of properties using temporal logics we have found that imprecisions frequently occur in the passage from the informal expression of properties in natural language to their formulation in temporal logics due to the inherent ambiguities in many natural language expressions We have thus attempted to identify a solution to this problem in the current state of the art in Natural Language Processing looking for a formal method that can help to generate logic formulae which correspond as closely as possible to the interpretations an ACTL expert would give of the informal requirements NL2ACTL has been developed using a general development environment PGDE aimed at the construction testing and debugging of natural language grammars and dictionar ies which permits us to build an application recognizing natural language sentences and producing their semantics 30 4 2 Verification Tools Auto Mauto INRIA As we stated above AUTO MAuTOo can also be used in ver ification because it permits automata to br reduced in various ways Commands allow process algebra term verification of partial properties based on observations of underlying automata Further automata analysis is available such as abstraction minimisation and diagnostics on equivalence failure Using MauTo in the verification phase
43. y box It is sufficient to specify its external synchronisation signals and this permits a top down approach in the AUTOGRAPH specification process Another feature of AUTOGRAPH is the automata interactive exploration starting from an initial state an user can just unfold the paths s he is interested in AUTOGRAPH provides Equivalence Checker Properties expressed in Natural Language CRLAB Parametric Concurrency Tool NL2ACTL PISATOOL cpap eh hee ite hh Term Specifications CCS Lotos Meije ACTL Formula User Interface FC2 Specifications Automata Networks i ACTL Properties Counter Examples AMC AUTOGRAPH Graphic Specifications Figure 0 2 The integration project several output formats in which a graphical specification can be translated including Fc2 the MAUTO syntax for terms and Postscript Auto Mauto INRIA Mauro 15 a generalisation of AUTO is a tool for both the specification and the verification for concurrent systems described by process algebrae Actually MauTo can deal with Mee 1 CCS 31 LOTOS 25 and EsTEREL 3 process algebrae while AUTO was just designed for the first two MAUTO is a command interpreter manipulating two classes of objects the class of process algebrae specifications and that of specification automata Each algebraical
44. ynchronisation constraints between the sub nets are expressed as edges from this state to itself having as label the synchronisation action set 3 a transducer this is a generalisation of the synchronised vector of nets where the net has several states from each state a specific set of synchronisation constraints are given reaching other states The format is more concrete than process algebra Moreover it enables the description of different views of parallelism and synchronisation In fact all finite state systems that can be represented by process algebrae are also representable by the Fc2 format 5 THE JACK INTERFACE In order to test our integration ideas we have developed an user friendly interface Fig ure 0 3 to the different tools composing the JACK system The interface is designed in an object oriented style where objects are either term specification files or Fc2 description files This interface has been developed using the Tcl Tk language facilities for the creation and manipulation of graphical widgets linked to a interactive function calls mechanism through mouse and keyboard events The interface is basically composed by two objects area one for term files and one for Fc2 files 5 1 Term Files Manipulation Terms are given in a textual form with the syntax adopted by MaAuTO In JACK there is a term specification area management see Figure 0 3 that is a list of files containing term specifications A set of

REPORTRAPPORT

Contents

Download Pdf Manuals

Related Search

Related Contents