Home

Fourth Release of the COMPASS Tool Symphony IDE User Manual

1. a Import c saa Select Import Projects Select a directory to search for existing Eclipse projects Select an import source Select root directory type filter text A Select archive file D tmp SymphonyIDE plugins eu compas General l amp Install Projects amp Overture v AVDeviceDiscovery_MC AVDeviceDiscovery_MC a Select All BEOCoSimulation_MC BEOCoSimulation_MC rae 7 BEOStreamingSo_MC BEOStreaming_MC Deselect All L BitRegister BitRegister V BitRegister_MC BitRegister_ MC ChoiceSupportInDebugger ChoiceSupportInDebugger amp Plug in Development Run Debug 4 amp Symphony A Symphony Examples amp Team Refresh ConwayOlympian ConwayOlympian v DPhilosophers_MC Dphils_MC P Davart Awat Options Search for nested projects Copy projects into workspace Working sets Add project to working sets lt Back Nex Cancel Figure 72 Symphony Examples Simple Bit Register The BitRegister_MC project contains the model of a bit register The specification contains operations to detect overflow or underflow a state variable a value to limit the maximum value of the state variable MAX and the increment value The main behaviour is described in the process RegisterProc which uses channels to perform increments and decrement until an overflow or underflow situation is found Such a situation generates a deadlock It is straigh
2. gt EMER_ACTIVE SC EMER_ACTIVE TurnindLvr gt 0 amp amp tilOld TurnIndLvr gt TURN_IND_OVERRIDE SC Vw TURN_IND_OVERRIDE REQ 007 TurnIndLvr 0 gt EMER_ACTIVE SC Y SystemUnderTest OUTPUT_CTRL CP TA Initial true gt IDLE SC A FLASHING left right amp amp left lOld right rOld gt FLASHING SC M FLASHING voltage lt 10 voltage gt 15 left amp amp right amp amp ctr gt 3 Old amp amp rOld gt IDLE SC v Initial true gt ON SC CA OFF REQ 002 t gt 320 gt ON SC M ON t gt 340 gt OFF SC A IDLE 10 lt voltage amp amp voltage lt 15 amp amp left right gt FLASHING SC CA gt TestEnvironment TE CA Figure 95 Detailed configuration example from the turn indication project CT displays the component type that is e CP for a composite structure block or class e TE for the top level component of the test environment e SC for a state machine transition In Figure 95 for example the transitions of the state machines associated with compo nents FLASH_CTRL and OUTPUT_CTRL are displayed for the sample project 4During creation of the initial test procedure the detailed configuration has already been used see Section 12 5 1 93 D31 4a
3. E Refinement Laws X iz als 7 channels c nat Law Name v test process test begin gt E test cml state v nat 1 actions A true J amp c v gt A B val x nat Stop A B v end E CML RPO List X m Ni Re Type Source E Refinement Law Details amp m lt Refinement Laws gt E CML RPO Details X writable Insert 8 26 Figure 82 Specification excerpt selection 80 D31 4a Symphony IDE User Manual Public ris O cML Explorer X v test gt A test cml B test cml amp channels c nat process test begin state v nat 1 actions B val x nat Stop A B v end HEI E Refinement Law Details amp lt Refinement Laws gt Figure 83 Searching for applicable laws Open With gt Show In Shift Alt w Cut Ctrl X Copy Ctrl C Paste Ctrl V Quick Fix Ctrl 1 Shift Right Shift Left Open Decleration F3 Debug As Run As Validate Team Compare With Replace With Fault Tolerance Refinement Preferences Input Methods 81 gt Refine gt lla COMPASS E EYCML c Refinement O E Refinement Laws jm Law Name E CMLRPOList X m Ni Re Type Source o E CMLRPO Details m D31 4a Symphony IDE User Manual Public COMPASS The applicable laws are then loaded onto the Refinement Laws panel and a law may be selected as shown in Figure 84 In this case the details of th
4. Auto generated THY file for Dwarf cml 6 c 7 a 3 g Bi DwarfType or e 7definition LampId lt L1 gt lt L2 gt lt L3 gt v amp c a raan pi ne LonpId 8 declare LampId_def eval evalp v 10 laststate Signal oe 11 Hineeniateta Signal 10 definition Signal set of LampId a 12 desiredproperstate ProperState 11 SR oe er ene 13 inv d a saasa 5 3 Ja o 14 CCCd currentstate d turnoff union d turnon 13 definition ProperState Signal z 15 Cd turnoff inter d turnon and 14 declare ProperState def eval evalp z Bt 16 NeverShow All 15 gt Ef insh 17 d currentstate lt gt lt L1 gt lt L2 gt lt L3 gt and 16 typedef DwarfType_Tag True by auto gt SLE 18 MaxOneLampChange 17 instantiation DwarfType Tag tag gPoc 19 card d currentstate d laststate union d las 18 begin 20 ForbidStopToDrive 19 definition tagName_DwarfType_Tag x DwarfType_Tag DwarfType 21 CCd lastproperstate stop gt d desiredpropersta 20 instance 22 DarkOnlyToStop 21 by intro_classes metis full_types Abs DwarfType_Tag_cases singleton i 23 Cd lastproperstate dark gt d desiredpropersta 22 end a 24 DarkOnlyFromStop 23 mh Cd desiredproperstate dark gt d lastpropersta 24 abbreviation Lastproperstate fld MkField TYPE DwarfType Tag 1 Proper ae r 25 abbreviation turnoff_fld MkField TYPE DwarfType Tag 2 set of LampIc ae
5. OoOo New Project Project Create a new project resource M Use default location Location Users uwe Development workspace Browse Working sets _ Add project to working sets Working sets lt Back Next gt Cancel Finish Figure 92 Creating a new RTT MBT Project selecting the project location Creating RTT MBT projects as sub components of another project can be useful if the RTT MBT test projects are part of a larger project representing a complete test cam paign where several models are used to generate test procedures for different aspects or parts of a complete system Every RTT MBT project uses exactly one test model to generate test procedures from Organising RTT MBT projects as folders inside an other Symphony project provides a flexible way to integrate RTT MBT projects in your project structure If one test model is sufficient for your goals it is recommended to create a stand alone project Creating a RT T MBT sub component is also supported by a wizard in the RTT per spective Select the Symphony project in the project explorer and start the wizard using New Other from the context menu or the File menu On the first page of the wizard select RT I MBT Folder from the RT Tester category Figure 93 and click Next In the follwing dialog page use the RTT MBT project name as the folder name for the new RTT MBT sub component The wizards creates an empty RTT MBT project structure representing the RTT
6. Specification frame This cannot be interpreted instantiate a new object of class C and assign it to v Table 8 CML statements 124 D31 4a Symphony IDE User Manual Public Operator Syntax Nondeterministic if statement if el gt al e2 gt a2 If statement if el then al elseif e2 then a2 else an Cases statement Cases e pl gt al p2 gt a2 others end Nondeterministic do statement do el gt al e2 gt a2 gt an Sequence for loop for e ins doa Set for loop for all e in set S doa Index for loop for i el to e2 by e3 doa While loop while e doa COMPASS Comments evaluate all guards ei If none are true then the statement diverges If one or more guards are true one of the associated actions is executed nondeter ministically the boolean expressions ei are evaluated in order When the first ei is evaluated to true the associ ated action is executed If no ei evaluates to true the action an is executed The expression e is matched against each pat tern pi in order The result of the cases state ment is the first action ai whose associated pat tern pi matches the expression e If not pattern is matched the others clause is executed if all guards ei evaluate to false terminate Oth erwise choose nondeterministically one guard that evaluates to true execute the associated ac tion and repeat the do statement for each expressi
7. D31 4a Symphony IDE User Manual Public COMPASS 15 Conclusion This user manual provides a basic guide to the use of the Symphony IDE and where to find and activate the tool s features Section 2 illustrated how to get hold of the software whereas the following sections introduced the Eclipse terminology with perspectives projects and basic error handling The plug ins for CML model simulation Section 6 collaborative modelling using multiple instances of the Symphony IDE Section 7 automated theorem proving of proof obligations Section 8 model checking of CML models Section 9 using the Model Checker for analysis of fault tolerance Section 9 the refinement support fea tures Section 11 automated test generation Section 12 and simplified support for translating SysML to CML models Section 13 are fully integrated into the main Sym phony IDE Some of the plugins for fault tolerance verification Section 10 and re finement calculation see COMPASS Deliverable D33 4 FM14 are explained more elaborately from a theoretical perspective in their own deliverables The overall ca pabilities of the Symphony IDE are broad and have a high degree of reuse of the component functionality Some of the plug ins due to external dependencies require the use of software be yond what is distributed by the COMPASS project these cases are documented in the sections belonging to the individual plug ins and core features
8. RT Tester Plugin E RT Tester a Figure 1 The COMPASS tools On the left of is Artisan Studio which provides the ability to model SoSs using SysML It is possible to generate XMI model files and CML files from SysML models http symphonytool org D31 4a Symphony IDE User Manual Public COMPASS in Artisan Studo and those are recognised within the Symphony tool SysML models may also have static fault analyses performed on them using the external HiP HOPS tool based on work from project task 3 3 3 In the centre of Figure I is the main Symphony tool itself with many of its submod ules identified and the larger grey boxes correspond to specific plug in In particular the Symphony IDE s connection to the external RT Tester tool facilitates the use of automated test generation techniques on SoS models and the Symphony IDE acts as a control console for the RT Tester platform There are also dependencies on the Isabelle theorem prover by the theorem prover plug in and on the Microsoft FORMULA model checker by the model checker plug in The fault tolerance plugin for CML models uses the model checker plugin to analyse fault tolerance properties of CML models like the static fault analysis that is done on SysML models using HiP HOPS this is based on work from project task 3 3 3 There is support for formal refinement using the refinement plugin this is a refinement calculator that uses the external Maude tool and the use
9. Symphony IDE User Manual Public COMPASS Allocation is only relevant for hardware in the loop testing it allows to specify the allocation of TE simulations and SUT test oracles to a specific CPU core TC is used for quickly defining transition coverage TC goals marking a state machine transition in the model browser in column TC specifies the goal cover this state machine transition in the test procedure to be created In Figure 95 for example the mark in column TC for transition EMER OFF 6 EmerSwitch gt BMER_ ON of state machine FLASH CTRL will lead to the generation of a test procedure where the emergency switch EmerSwitch is set to 1 at some time during the test execution so that the SUT if implemented correctly performs the equivalent behaviour to the state machine transition from EMER_OFF to EMER_ON Observe that every transition coverage goal is also identified as a test case automatically derived from the model Transition coverage test cases have identifiers TC lt Project Name gt TR lt number gt and by selecting the test case equivalent to the state machine transition marked in the TC column and adding it to the additional goals file See for a detailed de scription how this is performed the same effect is achieved The goal identification via column TC is just a work flow abbreviation in many situations for example in case of a regression test where just a few transitions have been
10. example cml Type checking model types are ok If there are errors in the file they will be reported in a manner similar to Symphony command line CML Checker Parsing files example cml Type checking Error 3430 Non compatible type lt CONECT gt detected for communication parameter index 0 expected CoSimulationProtocol TCP_Event in example cml at line 77 27 Note that by default the interpreter is not invoked on input see Section for such usage It is also possible to input CML directly into the command line tool when invoked with the i option This is useful for quickly cutting and pasting small bits of CML for example To generate a SVG graph representation of a parsed CML model we use the dot lt file gt and dotpath lt executable path gt options The invocation cmlc dot example dotpath usr bin dot example cml will produce the same output as above but will also create the file example svg with a representation of the parsed model 113 D31 4a Symphony IDE User Manual Public COMPASS 14 3 Proof Obligation Generation Invoking the command line tool with the pog option will cause the proof obligation generator to be run over the CML model if the model passed the type checker The resulting obligations if any are printed directly in the tool s output They may then be inspected by the user though nothing else may be done with them at this point Running the POG against the
11. int Q a x gt bey gt let n y 1 in n lt MAX amp s n n gt MAX amp Skip s 1 end COMPASS Listing 1 A Reader Writer model in CML 31 D31 4a Symphony IDE User Manual Public COMPASS 7 Collaborative Modelling in the Symphony IDE An SoS will often contain constituent systems that are developed by different stake holders which are geographically distributed In order to create and develop a model of such an SoS the different stakeholders need to establish a collaboration through which interface descriptions and the system design can be examined negotiated and agreed on Symphony contains a Collaborative Modelling plugin which enables instances of Sym phony IDE running on different computers to be connected via the internet in order to exchange modelling data and establish a collaboratively developed SoS model The Collaborative Modelling plugin can be used by modellers that want to work on a joint CML model of an SoS while being geographical distributed The basic principles of the Collaborative Modelling plugin is illustrated in Figure 26 Connectivity is established between instances of the Symphony IDE via a common Collaboration Project that is shared among the collaborating modellers The collabora tion between the modellers is performed by sending and exchanging configurations as illustrated by the configurations moving in the direction of the arrows A Configuration can be seen as a snap
12. 11 Alpha sendRescueInfto 12 serviceRescue 13 logFaultl resi 14 Alpha _LFTSimple Alpha 15 Alpha NFTSimple Alpha 16 Alpha DLSimple Alpha 17 Alpha _FFTSimple Alpha ls 19 Fault tolerant limit 29 process LFTSimple 21 begin 22 actions NOMINAL LFTSimple sen processMessage S 5 sendRescuelnfoToEru F receiveMlessage resendRescuelnfoToEru wT EP processMessage gt RI gt FFTSimple NOMINAL 25 RECEIVE_LFTSimple rec t H startRecoveryl enc 26 FAULT_LFTSimple fault b P LFT Sirra ATN LA at AEAT Icimple E logFau Fault Tolerance 1 gt logi NFTSimple NOMINAL Po mE e gt NOMII 31 NOMINAL_LFTSimple 32 end 33 34 Not fault tolerant 4 Figure 76 Fault tolerance verification menu on the project navigator 71 D31 4a Symphony IDE User Manual Public A B C D sr iuiviexampies cmi cs COMPASS 19 Init unwanted lt Faulti gt gt Init 20 Init 2iend 22 23 process Limit _LFTSimple Limit 24 process Limit NFTSimple Limit 25 process Limit _DLTSimple Limit 26 process Limit FFTSimple Limit 27 28 Fault tolerant 29 process MweP elk 30 begin 31 actions 32 NOMINA 33 FAULT 34 35 NOMINAL LF 36end 37 38 Not fault toleran 39 process NFTSimple 40 begin 41 actions 42 NOMINZ 43 FAULT 44 45 NOMINAL NF 46 end 47 48 Deadlocked
13. 73 To run fault tolerance verification check channels chansets processes name Unable to verify fault tolerance property property for process system due to The verification of fault tolerance property property for process system was The system defined by process system is NOT deadlock free The current ver sion of the model checker won t enable verification of fault tolerance of dead The system defined by process system is NOT divergence free Total elapsed The system defined by process system is NOT semifair Total elapsed time The system defined by process system is NOT divergence free nor semifair The system defined by process system is NOT fault tolerant with the given limit No system should be full fault tolerant Check design of system Total elapsed The system defined by process system is fault tolerant with the given limit D31 4a Symphony IDE User Manual Public COMPASS rau Baai pee a 20 Q FFTSimple NOMINAL f oe ae H startRecovery1 enc 22 actions Q LFTSimple NOMINAL 23 NOMINAL_LFTSimple sendRescueInfoToEru gt logFaultl Q NFTSimple NOMINAL_ S processMessage 2 processMessage gt RECEIVE_LFTSimple FAULT_LFTSimple 25 RECEIVE _LFTSimple receiveMessage gt serviceRescue gt NOMINAL_LFTSimple 26 FAULT_LFTSimple fault1 gt RECOVERY_LFTSimple errorl gt failurel gt Skip Pl 27 RECOVERY
14. A _ B behave as A until B takes control then behave like B Timed interrupt A _e_ B behave as A for e time units then behave as B Untimed timeout A gt B offer A but may nondeterministically stop offering A and offer B at any time Timeout A _ e gt B offer A for e time units then offer B Start deadline A startsby e A must execute an observable event within e time units Oth erwise the process is infeasible End deadline A endsby e A must terminate within e time units Otherwise the process is infeasible Table 11 Timed process constructors Operator Syntax Comments Replicated sequential composition i in seq e A i e must be a sequence for each i in the sequence A i is executed in order Replicated external choice 1 in set e U A i offer the environment the choice of all processes A i such that i is in the set e Replicated internal choice i in set e A i nondeterministically behave as A i for any i in the set e Replicated generalised parallelism es i in see lt execute all processes A i for i in the set e in A i parallel synchronising on the events in cs Replicated alphabetised parallelism i in set e execute all processes A i in parallel syn cs i A i chronising on the intersection of all cs i Each process A i can only perform events in es i Replicated interleaving i in set e A i execute all processes A i in parallel without synchro
15. D Figure 44 Distributed Simulation requested dialog As each collaborator replies to the simulation request the status of the reply will be shown on the nitialise Distributed Simulation dialog If all collaborators that have been assigned to simulate a process agrees the simulation may be started as shown in If just one of the collaborators rejects participating in the distributed simulation the whole simulation will be cancelled The distributed simulation is started by clicking Start simulation after which the other collaborators will be notified that the simulation is starting The distributed simulation will then automatically be launched and run as described in 43 D31 4a Symphony IDE User Manual Public COMPASS Initialise Distributed Simulation Select the process that will act as the coordinator of the simulation Select external processes and attach them to a collaborator Select Coordinating process EmergencyCoordination lt Simulate Animate External Process To be simulated by Status Em ye lal Ambulance compass collab3 gmal Lc Ready Pol ce com p 4a55 col g bD a gn lal JCD Ready cancel Simulationreay Figure 45 Distributed Simulation ready for start status 44 D31 4a Symphony IDE User Manual Public COMPASS 8 Proof Support in the Symphony IDE It should be noted that it is beyond the scope of this user manual to provide detailed descrip
16. ProperState gt IntrTest turnoff set of LampId i E Copy C turnon set of LampId Paste TAN laststate Signal currentstate Signal X Delete E desiredproperstate ProperState Move Rename F2 entstate d turnoff union d turnon d de S f inter d turnon and H Import how All e Export state lt gt lt L1 gt lt L2 gt lt L3 gt and LampChange Refresh f5 currentstate d laststate union d laststa StopToDrive Validate roperstate stop gt d desiredproperstate lt lyToStop Debug As gt roperstate dark gt d desiredproperstate i Run As gt LyFromStop Team gt edproperstate dark gt d lastproperstate i Compare With gt Dwar fType Replace With P anChawhll dA _and Theorem Proving i Check TP compatibility Properties l Inspect Proof Obligations F m Automatic Proof Obligation Discharge Manual Proof Obligation Discharge Manual Proof Session Figure 54 Invoking automatic proof obligation discharge With a CML model open right click on the model filename in the Project Explorer and select Theorem Proving Manual Proof Session as shown in Figure 58 The CML model is first checked to ensure it is supported by the theorem prover If there are any parts of unsupported syntax in the CML model an error message appears which informs the user A list of unsupported syntax is reported in the warning pane of the Symphony IDE If the model is supported the theorem prover pl
17. Y gt generated Y Isabelle gt 2013 10 10 11 24 17 2013 11 26 09 55 24 E Dwarf_User thy Ja Dwarf thy gt gt model Y POG 2013 11 26 10 03 43 a Dwarf_PO thy a Dwarf thy gt gt model gt Isabelle CML launch Figure 57 Project explorer with generated thy files EJ CML Explorer X U 9 pwarf cmi X mm B m types _ LampId lt Li gt lt L2 gt lt L3 gt Y i Dwarf Sianal set of LampId 3 New gt Signal Dwarf l Open s in set dark stop warning drive gt genera p A E READM Open With gt lastproperstate ProperState gt 2 intrTest turnoff set of LampId B Copy C turnon set of LampId Paste p laststate Signal currentstate Signal X Delete E desiredproperstate ProperState Move Rename f2 entstate d turnoff union d turnon d desi alk f inter d turnon and Reg mport how All e5 Export state lt gt lt L1 gt lt L2 gt lt L3 gt and LampChange Refresh f5 currentstate d laststate union d laststate StopToDrive Validate roperstate stop gt d desiredproperstate lt gt Deb A lyToStop ebug AS gt roperstate dark gt d desiredproperstate in Run As gt lyFromStop Team gt edproperstate dark gt d lastproperstate in i gt Compare With Eaa Replace With P EanChanilIl ld and Theorem Proving b Check TP compatibility Properties gl Inspect Proof Obligations f Automatic Proof Obligation Discharge Manual Proof Obligation D
18. a test procedure can be generated according to this configuration Note that exactly one test procedure in the execution context will be generated for each test procedure generation context in the generation context of a project 101 D31 4a Symphony IDE User Manual Public COMPASS 12 8 1 Activating the Generation Process As explained in Section 12 5 3 the generation process is activated by selecting a test procedure generation context in the project explorer and giving the Generate Test com mand from the RTT MBT tool bar from the RTT MBT menu or in the Test Generation Context context menu of the project explorer right click on the selected item When a test generation is started all progress bars are cleared and the following console message is displayed generating test procedure lt name gt please wait for the task to be finished During the test generation the progress for the different coverage goals and for the overall test generation is indicated in the progress view Successful test procedure generation is indicated through the following console message lt name gt PASS generate test procedure If the generation was aborted or did fail error messages are given in the console view 12 8 2 Results of Test Procedure Generation Validation Aspects Before running a generated test procedure against the SUT it may be desirable to vali date it with respect to the original test objectives you had in mind w
19. also see Figure 12 BR Problems 4 Tasks EJ Console 1 error 0 warnings 0 others Description Resource Path Location Type v Errors 1 item Function returns unexpected type Actual int Expected bool Error cml TypeError line 4 Problem Figure 13 User Interface problems view with type errors To give the complete picture for all errors in a given model the problem view shows the list of all generated errors see Figure 13 18 D31 4a Symphony IDE User Manual Public COMPASS Type error markers will be updated whenever a CML Source file is saved with changes To force a re check of all source files again click the Project Clean item from the menu bar 19 D31 4a Symphony IDE User Manual Public COMPASS 6 The Symphony Simulator This chapter explains how to simulate animate a CML model with the Symphony IDE This includes how to add and configure launch configurations and how the interpreter is launched and used Information on which CML constructs are supported by the Simulator can be found in Appendix A First the basic modes of operation are explained The interpreter operates in two modes Run and Debug and within these modes there are three options Animate Sim ulate and Remote Control These options control the level of user interaction and are described below 1 Simulate This option will interpret the model without any user interaction When faced with a choice of several observ
20. and MaxOneLampChange d and ForbidStopToDrive d and DarkOnlyToStop d and DarkOnlyFromStop d 14 4 CML Simulation The command line tool enables simulation of CML models when invoked with the e option Since the CML model may have more than one process defined the e lt procId gt option must be supplied where lt procId gt is the name of the process that is to be simulated As an example of how this works consider the following CML model in a file called example cml channels init a b process A begin init gt a gt Skip 114 D31 4a Symphony IDE User Manual Public COMPASS end process B begin init gt b gt Skip end process C A B The following command will simulate the process identified by C cmlc e C example cml This results in the following truncated output being printed to the console Symphony command line CML Checker Parsing files example cml Type checking model types are ok Simulator status event INITIALIZED Simulator status event RUNNING Simulator status event WAITING_FOR_ENVIRONMENT The system picked tau A gt begin class SactionClass0 7 C Next A Simulator status event RUNNING Simulator status event WAITING _FOR_ENVIRONMENT The system picked tau begin class SactionClass0O gt init gt a gt Skip C A l Next begin class SactionClass0 end SactionClass0 init gt a gt Skip
21. ing point input voltage has typical value 12V in today s cars and the model defines 10 lt voltage lt 15 as the admissible range As a consequence the lower bound 0 0V and upper bound 16 0V are suitable values to be inserted for voltage in the signal map Observe that the test data generator will only create inputs to the SUT which are consistent with the data ranges defined in signalmap csv This fact may be used to influence the generation process in the following ways if an input to the SUT is 91 D31 4a Symphony IDE User Manual Public COMPASS specified with identical lower and upper bounds in the signal map the generator will leave this value constant over the complete test execution time and try to reach the test objectives by manipulating the other inputs only A more detailed explanation of all columns in the signal map is given in Section 12 7 2 12 5 3 Generate the First Test Procedure To generate a test procedure from the initial generation context P 1 select the context P1 in the project browser Then select RTT MBT command Generate Test Procedure in the context menu of the project browser right click on P 1 or from the RTT Plugin command bar see Figure 94 D olw Oooo Generate Simulation Generate Test Procedure Clean Test Procedure Generation Context Generate and Execute Test Procedure Figure 94 Model based test commands in the RTT Plugin command bar As a result of this first generat
22. no state A csl cs2 B Not implemented Generalised parallelism A lnsl cs ns2 N implemented Generalised parallelism no state execute A and B in parallel synchronising on the events in cs Neither A nor B change the state Table 14 Parallel action constructors 132 D31 4a Symphony IDE User Manual Public COMPASS Operator Syntax Comments Replicated sequential composition i in seq e A i Execute A for parameter i in sequence over e Replicated external choice 2 in set e A 1 External choice indexed by i in set e Replicated internal choice Imi 2 in set e A i Internal choice indexed by 1 in set e Replicated interleaving i in set e Not implemented ns 1 Ali Replicated generalised parallelism lces i in set e Not implemented ns i 26a Replicated alphabetised parallelism i in set e Not implemented ns 1 cs 1 Ali Replicated synchronous parallelism 2 in set Not implemented ns 1 A i Table 15 Replicated action constructors 133 D31 4a Symphony IDE User Manual Public COMPASS Operator Syntax Comments Let let p e ina Local constant declaration declare the local variable v of type T optionally ini tialised to e and evaluate action a in this context Assignment vi e assign e to v Multiple assignment atomic vl el assignments are executed atomically with respect to en the state invariant execute operation op of the current
23. nor receiveMessage Figure 77 B shows the corresponding red marker process NFTSimple begin actions NOMINAL sendRescueInfoTokEru gt processMessage gt RECEIVE FAULT RECEIVE receiveMessage gt serviceRescue gt NOMINAL 6The plugin always runs both fault tolerance verification versions with and without the limiting condi tion 76 D31 4a Symphony IDE User Manual Public COMPASS FAULT unwanted lt Faultl gt gt RECOVERY unwanted lt Errorl gt gt unwanted lt Failurel gt gt Skip RECOVERY StartRecoveryl gt endRecoveryl gt serviceRescue gt NOMINAL NOMINAL end Listing 5 Not Fault Tolerance example 10 2 4 Example DL The current version of the Fault Tolerance Plugin is unable to check fault tolerance on systems that are deadlocked shows this example and Figure 77 C its warning mark The difference to a non deadlocked system can be subtle compar ing Listing 6 to Listing 4 where both instances of Stop replace a recursive call to NOMINAL _DLSimple Both Stop action instances cause a deadlock in this sys tem process DLSimple begin actions NOMINAL sendRescuelInfoToEru gt processMessage gt RECEIVE FAULT RECEIVE receiveMessage gt serviceRescue gt Stop FAULT unwanted lt Faultl gt gt RECOVERY unwanted lt Errorl gt gt unwanted lt Failurel gt gt Skip RECOVERY StartRecoveryl gt logFaultl gt
24. simp del atLeastAtMost_ iff add atLeastAtMost_unfold apply unfold numberMonth_def apply unfold months def apply unfold atLeastAtMost_def apply auto done record raw_date day day month 10 definition isLeapYear nat bool wh Lemma month list simp lemma isLeapYear 2000 UNIV set months apply simp add months def apply unfold set_eq iff apply clarify apply case tac x Mina simp_all longleftarrow rightarrow Prover record raw date longrightarrow Progress Symbol over Output ES ob Conso proof prove step 6 Viewer goal 1 subgoal gt leftrightarrow 1 UNTY a longleftrightarrow P gt Leftrightarrow rover Output lt gt Longleftrightarrow mapsto gt longmapsto midarrow Midarrow Figure 50 Overview of Isabelle perspective in Symphony Theory File Editor A text editor which enables the user to interact with the theory script and prove theorems add additional definitions lemmas and theorems Theory Outline This pane provides an outline to the contents of the selected theory file including definitions functions lemmas and theorems and may be used to navigate the theory file Prover Progress A collection of status bars for the currently open theory files shows the progress made by Isabelle in proving the scripts in the theory file Prover Output A window to report error messages and the status of the goals of selected
25. test_model cml line 3 Y o Action cs test test_model cml line 4 pal CML Debugger E test_model cml 2 p outline 5 CML Event X E channels tock init a b rar process A begin end init process B begin end process test A init B console X Tasks Error Log C amp Mlele Bvriv a Quick Launch CML Model CML Debugger Waiting for environment on init tock WAITING FOR ENVIRONMENT Figure 19 A CML model animated in the debug perspective Debug test test_model cml Symphony IDE File Edit Navigate Search Project Run Window Help ri v ae a t BS wer O Q By ee Q ei EVM Debug Debug X x A Variables Breakpoints Observable Event History X m v BY Quick Launch CML Model tock gt i CML Debug Target init CML Debugger E test_model cml X A 2 Outline CML Event X 7 2 channels tock init a b process A begin init gt SESISkip end process B begin init gt b gt Skip end b process test A init B console X Tasks 9 Error Log a E Mlee Bvive BG Quick Launch CML Model CML Debugger Waiting for environment on a b tock WAITING FOR ENVIRONMENT writable Insert 3 29 Figure 20 The init event has just occurred and it is now currently offering a b and tock where a is currently selected 6 3 3 Run Debug In addition to the two modes of operation Animate and Simulate the standard modes Run and Debug als
26. 3 The typical application of this feature is for the generation of robustness tests where certain inputs to the SUT are to be produced only in exceptional behaviour situations These inputs are written in test environment TE simulations and the associated state machine transitions have been marked in the ROB column of the detailed configuration Then these transitions will only be taken in test procedures generated with RB 1 RP 1 100 in their advanced configuration Test environment state machines can have transitions marked by the stereotype lt lt Robustness gt gt These transitions are always processed as robustness transitions regardless of their status in column ROB in the detailed configuration With column ROB it is possible to mark additional transitions of TE state machines as robustness transitions Finally observe that marking SUT state machine transitions in column ROB has no effect 12 7 2 Detailed Configuration of the Signal Map The signalmap editor is opened by double clicking the file TestProcedures lt Test Proc Gen Context gt conf signalmap csv The signal map has already been introduced in Section 12 5 2 in the context of test project creation We will now describe the detailed configuration options provided by the signal map To this end consider an example of a signal map from the turn indication sample project as displayed in Figurelodt3 The editor for signalmap csv files contains more c
27. 87 D31 4a Symphony IDE User Manual Public COMPASS ProjectExplorer X 8 os Y SampleProject Vv Turnindication Y gt TestExecution Execution Context gt _P1 Test Procedure Y TestGeneration Generation Context gt _P1 Test Procedure Generation Context Figure 90 Test procedure generation and execution context Test Procedure Generation Context The test procedure generation context is the place in the project where the generation of a single test procedure is prepared Here the test engineers configure the generation by e specifying the model portions to be evaluated during the generation e specifying the test cases to be covered in the test procedure to be generated Execution Context The execution context is the place where the actual test proce dures which can be compiled and executed against the SUT reside in This context is contained in directory TestExecution When RTT MBT creates a new test proce dure based on the information provided in the respective test procedure generation con text the resulting test procedure files are placed in a sub directory of TestExecution carrying the same name as the respective generation context There it can be compiled executed evaluated and documented The execution context can contain both automat ically generated and manually created test procedures The manual development of test procedures is described in Ver13al Figure 90 shows the test procedu
28. An account is used to identify the connected user on the XMPP server The Collaborative Modelling plug in has been tested against Google Talk servers for which Google accounts can be used Connecting A connection is established by using the Account Information dialog that can be opened by clicking the Collaborative Modelling view s dropdown menu and clicking Connect to IM Provider as shown in Figure 28 In the dialog XMPP can be selected as con Jhttp www eclipse org ecf 33 D31 4a Symphony IDE User Manual Public COMPASS Error Log Problems Tasks E Console Messages Contacts Collaborative Modelling X Test attached to project EmergencyMgm e6ced7a0 2801 4aeb 9012 9d57e143b5b1 Expand All Y D Test attached to project EmergencyMgm e6ced7a0 2801 4aeb 9012 9d57e143b5b1 gt D Configurations 8 Collapse All Add new collaboration project v Collaborators 2 Connect to IM Provider mm compass collab gmail com mm compass collab2 gmail com Ctrl Contrib Bottom Figure 28 Screenshot of the Connect menu nection protocol or alternatively XMPPS in order to use an encrypted connection via Secure Sockets Layer In the Account Information dialog the user account information and server address need to be provided to establish a connection as show in Figure 29 Once connected the active view will change to Contacts Only accounts listed in the contacts list can become part of a collabo
29. Dwarf Signal example bundled with the Symphony IDE results in the following truncated output Symphony command line CML Checker Parsing files Dwarf cml Type checking Warning 5001 Instance variable dw is not initialized in Users jwc Documents compass Common PublicLiveCMLCaseStudies Dwarf Dwarf cml at line 68 2 type invariant satisfiable obligation in Users jwc Documents compass Common PublicLiveCMLCaseStudies Dwarf Dwarf cml at line 4 2 exists ps ProperState amp ps in set dark stop warning drive type invariant satisfiable obligation in Users jwc Documents compass Common PublicLiveCMLCaseStudies Dwarf Dwarf cml at line 1t2 exists d DwarfType amp d currentstate d turnoff union d turnon d desiredproperstate and d turnoff inter d turnon and d currentstate lt gt lt L1 gt lt L2 gt lt L3 gt and card d currentstate d laststate union d laststate d currentstate lt 1 and d lastproperstate stop gt d desiredproperstate lt gt drive and d lastproperstate dark gt d desiredproperstate in set dark stop and d desiredproperstate dark gt d lastproperstate in set dark stop type invariant satisfiable obligation in Users jwc Documents compass Common PublicLiveCMLCaseStudies Dwarf Dwarf cml at line Ce ee exists d DwarfSignal amp NeverShowAll d
30. E Preferences Install gt E Overture amp Plug in Development gt amp Run Debug gt amp Symphony gt amp Team Cancel Figure 106 Selecting File System as import source 109 D31 4a Symphony IDE User Manual Public File system Import resources from the local file system From directory C Users Alvaro Documents XMI COMPASS m amp XMI Filter Types Select All Deselect All Into folder HSUV Options _ Overwrite existing resources without warning _ Create top level folder Advanced gt gt Finish Cancel Figure 107 Selecting the XMI file 13 3 Generating CML and Inspecting the Result Finally to generate the CML model right click the XMI file and select the menu item SysML Import SysML state machine as shown in Figure IE CML Explorer 33 Bane a ES HSUV E_HSUV xmil New gt Open Open With gt E Copy Ctrl C Paste Ctrl V 3 Delete Delete Move Rename F2 g Import e5 Export E Refresh F5 Debug As Run As Team Compare With Replace With mc Model check CML PoG SysML Y Y v v v v v v bd f CML THY Properties Alt Enter Import SysML State Machine Figure 108 Menu selection for model generation A number of CML files will be created in the CML project as shown in Figure In order to inspect the model of the state
31. Figure 41 A Configuration is approved or rejected by right clicking the specific Configuration and selecting either the Approve or Reject menu item as can be seen in In case a Configuration is rejected a dialog will open in which the reason for the reject decision can be entered 40 D31 4a Symphony IDE User Manual Public COMPASS Error Log i Problems 4 Tasks Console A Messages Contacts s Collaborative Modelling X compass collab2 gmail com v D Configurations 8 gt E c7cad687 Wed Aug 06 15 48 47 CEST 2014 Not shared local configuration v 5 3a316fb1 Thu Jul 31 15 45 03 CEST 2014 Received gt E Files 4 v sg Sent To 1 s compass collab gmail com Rejected Figure 41 Configuration rejected by collaborator Evolving and Agreeing on Model Design Instead of merely approving or rejecting a suggested model design the collaborator can make adjustments to the files received in a Configuration When a file is changed a new Configuration will automatically be created This new Configuration can then be signed and shared in the exact same way as described above Sending updated Configurations back and forward will establish a type of collaboration where the design of the SoS can be evaluated and negotiated by the collaborators via continuous adjustments of the CML specifications Each time a new Configuration is received the new version will be added to a Configuration list thereby creating a h
32. MBT project As stated before each RTT MBT project uses exactly one test model An XMI file containing your test model has to be imported into the project see Ver13b for an explanation how test models are exported to XMI Typically this XMI file resides 89 D31 4a Symphony IDE User Manual Public COMPASS 0 0O09 New Select a wizard 1 Wizards type filter text gt Java gt Overture gt Plug in Development Y Symphony CML Class Ecm File Q CML Process Ecm Project t aRTT MBT Folder Y RTT MBT Project lt Back Next gt Cancel Finish Figure 93 Creating a new RTT MBT Project creating a Sub Directory Project on your PC where also the test model elaboration took place Selecting RTT MBT gt Import Model opens a file browser that can be used to navigate to the directory where your XMI file with extension XML or XMI is located Select the file and start the import As a result of the import the XMI file is stored as model_dump xm1 in the model directory of the RTT MBT project together with a LivelockReport log file Please check the livelock report for problems in the model After a successful model import a first test generation context P1 has been created in the generation context directory Test Generation which will be used to generate the first test procedure along with an initial project configuration and signal map as explained in Section 12 5 The ini
33. Symphony model checking support Number of instances handled by FORMULA 1 Help Install Update Isabelle Java Model Checker Setup Plug in Development RT Tester Run Debug Symphony Team Theorem Prover Setup VDM Restore Defaults Apply Cancel Figure 61 CML Model Checker Preferences 9 4 Using the CML model checker The model checker functionalities are available through the CML Model Checker per spective see Figure 62 which is composed by the CML Explorer 1 the CML Editor 59 D31 4a Symphony IDE User Manual Public COMPASS 2 the Outline view 3 the internal Web browser to show the counterexample when invoked and two further specific views the CML Model Checker List view 4 to show the overall result of the analysis and the Model Checker Progress view 5 to show the execution progress of the analysis a File Edit Navigate Search Project TheoremProver Isabelle Run Window Help ri R Z a A Gy amp arb yoy e Quick Access E E CML me Model Checker E CML Explorer 53 G i 6 outline X p i Examples An outline is not available me CML Model Checker List 22 m File Property SAT E Model Checker Progress View 53 A fD ErorLlog X F Problems Tasks EJ Console HY Workspace Log type filter text No operations to display at this time Figure 62 CML Model Checker Perspective The analysis of a CML model is
34. Tasks E Console A Contacts Collaborative Modelling X a Messages amp Console c4e45d71 Fri Aug 08 16 32 25 CEST 2014 Not shared local configuration gt 0 hj attached to project Collab2 e8162005 bf55 4083 a0b6 c42e75981370 gt Test attached to project EmergencyManagement e6ced7a0 2801 4aeb 9012 9d57e143b5b1 v TaBa Systems Collaboration attached to project TaBa Sys efd93ad9 3829 4c70 b9e5 9b5fac8d8226 D Configurations 1 Y c4e45d71 Fri Aug 08 16 32 25 CEST 2014 Not shared local configuration v E Files 1 Sign and Share Configuration gt fll System cml Fri Aug 08 16 32 25 CES 2014 New file Diff with previous configuration 3 Sent To 0 gt Collaborators 2 Figure 39 Signing and Sharing configuration When a Configuration is selected for sharing it is signed with the Collaborator s name a snap shot is taken of the current contents of the files in the Configuration and the Configuration is locked from further changes The signed and locked Configuration is then pushed to the other collaborators in the Collaboration Group and as such new changes in the collaboration will appear instantly for all collaborators This is done in order to show the current development and changes as they occur as the aim is to support a collaborative work process and not to function as a versioning system When a Configuration is received it will appear in the Collaboration View as a Con figur
35. collaboration project Connect to IM Provider Figure 30 Screenshot of the new project menu This will open the New collaboration project dialog as seen in Figure 31 in which the title and description of the project is to be entered The collaboration project must be attached to a CML project in order for the plugin to know in which workspace directory it should operate Only one Collaboration Project can be attached to a CML project at a time The plugin will track the files in the workspace directory in order to determine changes to the model New collaboration project Create new collaboration and attach it to a project in the workspace Collaboration Title Title Message Description Collab1 Attach collaborative work to this project wet mie abas TaBa System Figure 31 Screenshot of the new project dialog The creator of the Collaboration Project will initiate the collaboration by adding col laborators to the Collaboration Group The Collaboration Group is created on the basis of the user s contacts buddy list from which the wanted collaborators can be selected 35 D31 4a Symphony IDE User Manual Public COMPASS Once other collaborators have joined a collaboration project the initiator has no more control of the project than the other collaborators This means that the Collaboration Project is decentralized and is therefore not exclusively managed by any collaborator All collaborators that are in the Collaboration
36. end Simulator status event RUNNING Top CML behavior WAITING_CHILD Waiting for environment on init tock Simulator status event WAITING_FOR_ENVIRONMENT OJinit 1 tock 0 The environment picked init Executing init Simulator status event RUNNING Top CML behavior RUNNING Top CML behavior WAITING_CHILD Waiting for environment on a tock Simulator status event WAITING _FOR_ENVIRONMENT Ola 1 tock 0 Note that the two zeros on lines by themselves are user input the simulator will run until the environment must choose an observable event to synchronise on then present the choice of synchronisable events to the user The user must then enter the number of the chosen event then the simulator will continue 115 D31 4a Symphony IDE User Manual Public COMPASS 14 5 SysML to CML translation Given an example SysML model that has been exported to an XMI file from Artisan Studio it is possible to use the command line tool to convert the model into CML If the XMI file is named example xmi and it contains a state machine called Exam pleModel then the output of the translation will be placed in a subdirectory called ExampleModel Note that the output path is based on the name of the model not the XMI filename Details on how the translation is used within the Symphony IDE may be found in and details on the translation process itself may be found in COMPASS Deliverable D31 4d ML14 116
37. fault tolerant limit process name Total elapsed time elapsed time If all required definitions are modelled see Section 10 2 several operations will start running The first two check the prerequisites explained in APR 13 i divergence freedom and 11 semifairness and a third will check for deadlock freedom If these prerequisites are met then two further operations are started one to check if the CML process is fully fault tolerant and another if the process is fault tolerant with respect to the limiting conditions if not limiting conditions are defined the default considers that the model is able to tolerate all faults All operations use Symphony s model checker tool and can be cancelled while they are running or before they run The possible messages for errors warnings and successes are shown as markers be side the top level CML process as shown in Figure 77 and are described in Table 2 The elements in square brackets are replaced by actual values For example replace property with Semifairness and system with the process P Fault Tolerance Plu gin messages are also shown in the Markers pane If this view is not shown select the menu Window Show View Other then select General Markers To clear any resultant fault tolerance messages right click on the relevant CML process or the message itself on the Markers view see Figure 78 and select Clear fault tolerant markers
38. finished If this switch is deactivated all the required files are downloaded If active additional log files and other generated files are downloaded that can be useful for debugging The Settings for Test Generation Context and Test Execution Context can be over ridden by project properties the settings for the client mode verbose logging and extra file retrieval can only be defined in the global Eclipse preferences of the RTT Plugin 12 2 The RTT MBT Perspective RTT MBT test generation is performed using the RT Tester perspective RttPerspec tive This perspective is designed to allow model based test generation and execu tion of generated test procedures The perspective shown in Figure 89 consists of a Project Explorer a Console View a Progress View an Outline and a central area for all Editors The RTT MBT Toolbar provides quick access to all RTT MBT com mands The Project Explorer lets you create select and delete projects and navigate between the files in these projects as well as adding new files to existing projects It is a cen tral element of the perspective RTT MBT commands are normally performed on the selected item in the Project Explorer The icons in the Toolbar are enabled or disabled with respect to the selected item If multiple items are selected only the commands that can be performed for all selected items are enabled If a command 1s activated for mul tiple selected objects the command is performed fo
39. from SUT inputs and outputs also local variable values are selectable as for example the tilOld variable storing the last state of the turn indica tion lever Additionally it is possible to display simple state machine states such as EMER_OFF of state machine FLASH CTRL in the sample project Simple states are displayed like Boolean variables over time value 1 meaning that the machine resides in this state Hierarchic composite states such as EMER_ON in Figure 98 can be unfolded to show their subordinate states Signals of FLASH_CTRL EJ Figure 99 Display of the signal viewer for a test procedure covering all transitions of state machine FLASH_CTRL in the sample project Figure 99 shows a typical display of the signal viewer it is associated with a test proce dure generated with the objective to cover all transitions of state machine FLASH_CTRL in the sample project The signal values are displayed over timd for the following sig nals e EmerSwitch emergency switch on off 1 0 input to the SUT e LampsLeft indication lights left hand side on off 1 0 output of the SUT e LampsRight indication lights right hand side on off 1 0 output of the SUT TurnindLvr turn indication lever off left right 0 1 2 input to the SUT e voltage input to the SUT 6This presentation style is called y t diagram 103 D31 4a Symphony IDE User Manua
40. from using the visibility functionality to hide interfaces that has already been negotiated or approved by others Once a file is added to a Collaboration Project it will become part of a Configuration as shown in Figure 38 The contents of the files added to the Collaboration Project can freely be adjusted locally within a Configuration until the collaborator wants to share the model with 38 D31 4a Symphony IDE User Manual Public COMPASS Error Log B Problems Tasks E Console Contacts Collaborative Modelling X A Messages TaBa Systems Collaboration attached to project TaBa Sys efd93ad9 3829 4c70 b9e5 9b5fac8d8226 gt D hj attached to project Collab2 e8162005 bF55 4083 a0b6 c42e75981370 gt Test attached to project EmergencyManagement e6ced7a0 2801 4aeb 9012 9d57e143b5b1 TaBa Systems Collaboration attached to project TaBa Sys efd93ad9 3829 4c70 b9e5 9b5fac8d8226 v D Configurations 1 c4e45d71 Fri Aug 08 16 32 25 CEST 2014 Not shared local configuration v E Files 1 gt M System cml Fri Aug 08 16 32 25 CEST 2014 New file Sent To 0 gt x Collaborators 2 Figure 38 New non shared configuration the other collaborators Once shared the particular Configuration will become read only Sharing Model Data A model is shared by right clicking on the Configuration and clicking Sign and Share Configuration as shown in Figure 39 Error Log Problems 4
41. fully supported by the POG Obligations will be generated for any value initialization that requires them B 10 State State both in processes and classes is supported by the POG POs will be generated for any state initializations and invariants that require them 129 D31 4a Symphony IDE User Manual Public COMPASS C CML Support in the Theorem Prover This section gives an overview of the CML constructs that are implemented We present the constructs using tables where the first column of each table gives the name of the operator the second gives an informal syntax and the last is a short description that gives the operator s status If a construct is not supported entirely then the name of operator will be highlighted in red whilst partially supported operators are written in blue 130 D31 4a Symphony IDE User Manual Public COMPASS C 1 Actions The following tables describe all of the supported and partially supported actions Where A and B are actions e is an expression P x is a predicate expression with x free c is a channel name cs is a channel set expression ns is a nameset expres sion Operator Syntax Termination SK1p Deadlock SLOP Chaos Chaos Divergence Div Delay Wait e Prefixing c e x P x gt Guarded action le amp A Sequential composition A B External choice A B Internal choice A B Interrupt A _ B Timed interrupt A _e_ B Untimed timeout A gt B
42. hn pag abort Al poe 26 abbreviation turnon_fld MkField TYPE DwarfType Tag 3 set of LampId oa p MaxOneLampChange d and 27 abbreviation laststate fld MkField TYPE DwarfType Tag 4l Signal 30 ForbidStopToDrive d and 28 abbreviation currentstate_fld MkField TYPE DwarfType Tag 5 Signal 31 DarkOnlyToStop d and 29 abbreviation desiredproperstate fld MkField TYPE DwarfType Tag 6 Prc 32 DarkOnlyFromStop d 30 33 3l abbreviation lastproperstate SelectRec lastproperstate_fld 34 values 32 abbreviation turnoff SelectRec turnoff_fld 35 dark Signal 33 abbreviation turnon SelectRec turnon_fld 36 stop Signal lt L1 gt lt L2 gt 34 abbreviation laststate SelectRec laststate fld a 37 warning Signal lt L1 gt lt L3 gt 35 abbreviation currentstate SelectRec currentstate_fld 38 drive Signal lt L2 gt lt L3 gt 36 abbreviation desiredproperstate SelectRec desiredproperstate fld a 39 37 40 functions 38 definition Error Log X fart Problems Tasks EJ Console PO CML PO List BO CML PO Details 5 7 Ex x 2 A ead Workspace Log i Figure 59 Example Dwarf CML model and generated thy file The theorems are all simply proved using the cml_tac proof tactic The tactic is applied by using the line by cml_auto_tac on the line below the theorem This applies rules and tactics defined in the isabelle utp UTP and CML theories imported during the initial setup of the the
43. invoked through the context menu when the CML or the MC perspectives are active see Figure 63 E Model Checker The Symphony IDE ga S a a File Edit Navigate Search Project Theorem Prover Isabelle Run Window Help rhe Sas Pr QrF FPreoro le Quick Access E E CML me Model Checker E CML Explorer 5 m A G Outline O we An outline is not available ES AVDeviceDiscovery_ MC BEOCE New 7 E BEOSt Go Into 2 cusSSd F Copy Ctrl C 2 DPhilc Paste Ctrl V E InfCor 3 Delete Delete Move me CML Model Checker List 33 m Rename F2 Process Property SAT s Import e Export I 2 Refresh F5 Close Project Close Unrelated Projects E Model Che Debug As Tasks El Console Run As gt Team gt No operation Compare With gt Plug in Restore from Local History Configure gt Create External System Template E BitRegister mc Model check gt Check MC compatibility E cm PoG A Check deadlock Saia k Check livelock ites Properties Alt Enter Check Nondeterminism Figure 63 The Model Checker Context Menu Right click on the CML project or file to be analysed and select Model check Property to be checked The option Check MC Compatibility allows a previous check if the constructs used in the model are supported by the model checker If some con structor is not supported by the model checker the Symphony IDE shows a warning 60 D31 4a Sympho
44. is slower than FDR and PAT Regarding manipulation of infinite types the CML model checker is able to directly handle infinite data types in communication and in predicates whereas FDR and PAT are not This is a result of using SMT solving to instantiate and use values based on constraints Thus the CML model checker is able to provide answers for cases where FDR and PAT are not 9 3 Model checker Preferences The way the model checker instantiates data from infinite domains is configurable in Symphony through the menu Window gt Preferences There is a section Model Checker Setup see Figure 61 that provides a field containing the number of instances that the model checker will use for all infinite types used in any CML model The default value is 1 The suitable value depends on the specification For example 1f the piece of CML code ch x gt Stop is used only and ch is a channel supporting an infinite type only one instance is enough to detect the deadlock However 1f the CML code a x gt b y gt if a lt gt b then a and b support infinite type is used the model checker needs two instances at least to perform the correct analysis In general guidelines the number of instances can be determined by looking at the necessary values to explore all branches of the analysed process a C E Preferences type filter text Model Checker Setup Py General Ant Communications Setup values for using the
45. name to be used by the TE when writing to an interface variable of the SUT into column Concrete Signal Identifier only filled in if TE may WRITE this signal 97 D31 4a Symphony IDE User Manual Public COMPASS Admissible Error may contain 0 or a positive integer or floating point value It is used to introduce tolerances into test oracles to be applied when checking SUT outputs against expected results If for some SUT output variable x an admissible error has been specified in the signal map and an output value 7 is expected at a certain stage of the test execution outputs x in range EZ E lt SL lt E E are still accepted by the oracles and lead to PASS verdicts Values outside this range lead to a FAIL Latency complements the Admissible Error in the time domain A latency value gt O time unit milli seconds affects the test oracles in such a way that they still accept an output expected at time tg according to the model if it is produced within the range of the admissible error at some point in time interval to to l 12 7 3 Test Generation Properties The test generation properties can be adjusted by editing the configuration files max_steps txt and advanced conf Both files contain properties that control the RT T MBT test generation The files are text files with semicolon separated values These values are described in this chapter so that they can be adjusted using an editor or any other CSV file editing to
46. or process 1 with the parameters p 2 execute action A with parame ters p Execute operation op assign result to v Return return eorreturn Return value e in an operation Specification VDM specification statement frame wie Vie TI rda ys T2 pre Pl vl v2 post P2tvilevi vVzZev2 New y i new C Not implemented Table 16 CML statements 134 D31 4a Symphony IDE User Manual Public COMPASS Operator Syntax Comments Nondeterministic if statement Not implemented Lit el gt al e2 gt a2 end If statement The condition el is used to enable the statement al or if el then al an The optional elseif are not allowed elseif e2 then a2 x else an Cases statement Not implemented cases e pl gt al p2 gt a2 others gt an end Nondeterministic do statement Not implemented do el gt al e2 gt a2 end Sequence for loop for e ins doa Not implemented Set for loop for all e in set S do a Notimplemented Index for loop for i el to e2 by e3 dg Not implemented While loop while e do a repeat a while e evaluates to false Table 17 Control statements 135 D31 4a Symphony IDE User Manual Public COMPASS C 2 Declarations Operator Syntax Comments Value Declaration values Definitions of values to be used in a cml model value definitions Value Definition N nat It declares the value N as a natural number and assigns the value 2 to it Channe
47. processes This is shown in Figure 18 To launch a simulation a process must be chosen This is done by double clicking one of the process names in the list or selecting it and pressing OK This will launch a simulation with that process as the top level process If you launch via a shortcut then a launch configuration named Quick Launch or Quick Launch lt number gt if more exist will be created and launched 22 D31 4a Symphony IDE User Manual Public COMPASS File Edit Navigate Search Project Run Window mi v a Br Ov Qe gry v E CML Explorer X AlS Y OG test_model cml X gt BitRegister process testProcessl p rocess testProcess2 gt E bO P i gt 1 3 Dwarf gt RingBuffer v test gt test madal enl New gt begin Skip end begin Skip end Open Open With gt Copy Delete Delete Move Rename F2 Import Export Refresh F5 Validate Debug As Run As r 1 Ch model Team Run Configurations Compare With gt Replace With Properties Alt Entei Figure 17 The quick launcher 6 3 Interpretation As mentioned at the start of there are four possible ways to interpret a model each of them will be described 6 3 1 Animation Animating a model is achieved by choosing the Animate radio button in the launch configuration as described in the last section this is also the default behavior In this mode of operation the user has to pick every observab
48. section Edit Conclusion Merge Cosim section into Simulation WC 0 21 10 08 2014 Added section on Collaborative Modelling 023 5082014 ACF Eating roe 25 08 2014 ON Eaim o2 95 08 2014 US Eime p 036 95 08 2014 ALRD Ede 0 _ NO OO O N OI Olo oO ol O SN OY A D31 4a Symphony IDE User Manual Public COMPASS Contents U9 3 1 Eclipse Terminology ooa aa 0000008 4 Managing Symphony Projects 4 1 Creating new CML projects oaoa a a 2 00002 eee 5 The CML Type Checker 5 1 Output 25 stobeece hb ete een eee as 5 2 Representation ce whe Sew we Hee RE OS 6 The Symphony Simulator 6 1 Creating a Launch Configuration 6 2 Launch Via Shortcut 6 3 Interpretation 2 04 6 4 Co simulation 0 2 7 Collaborative Modelling in the Symphony IDE 7 1 Connectivity between Symphony IDE instances 7 2 Creation of a Collaboration Environment 7 3 Exchange and negotiation of model data 7 4 Distributed Simulation 8 Proof Support in the Symphony IDE 8 1 Obtaining the Software 8 2 Configuration Instructions for Isabelle UTP 8 3 Using the Isabelle perspective with the Symphony IDE 8 4 Proving CML Theorems 9 The Model Checker Plug In 9 1 Installing Auxiliary Software 9 2 Differences from other tools 2 9 3 Mod
49. systern 849 process DLSimple 50 begin 51 actions 52 NOMINA 53 FAULT 54 55 NOMINAL DLS 56 end 57 58 Full fault tolera 859 process FFTSimple 60 begin 61 actions E MOMTAT Undo Revert File Save Open With Show In Cut Copy Paste Quick Fix Shift Right Shift Left ff Add to Snippets Open Decleration Profile As Debug As Run As Validate Replace With Forward search Team Compare With Preferences Remove from Context Ctrl Z Ctrl S Alt Shift W gt Ctrl X Ctrl C Ctrl V Ctrl 1 Ctrl Alt Shift Down ple FAULT LI rrori gt gt Skip ea le FAULT_N gt Skip Tet fl RFATITT FI Figure 77 Fault tolerance verification menu on the CML model 72 D31 4a Symphony IDE User Manual Public COMPASS Table 2 Messages of fault tolerance verification plugin Description Icon Message Missing definition sets The tool will show only those missing Exception occurred an internal error exception message Canceled by user canceled by user Deadlock locked systems Not divergence free time time elapsed Not semifair time elapsed Not semifair and not diver gence fr ee Total elapsed time time elapsed Not limited fault tolerant limit process name Total elapsed time elapsed time Full fault tolerant time time elapsed Limited but not full
50. test procedure executable Tby default the folder Test Execution within the project 8The menu command Execute Test from the RTT MBT menu or the toolbar can be used to perform the test procedure actions Clean Test Compile Test Run Test Replay Test Result and Generate Documen tation in the correct order without further user interaction as long as no errors occur 104 D31 4a Symphony IDE User Manual Public COMPASS 12 9 3 Compile Test Procedure A test procedure is always executed together with the system under test The stim ulations of the test procedure must be connected to the respective input interfaces of the SUT and the output interfaces of the SUT that are relevant for the test must be connected to the test procedure This is a task for the test environment A generic test environment is created together with the test procedures during the test generation Connecting an SUT to this generic interface is part of the duties of a test engineer RTT MBT provides functionality to create a simulation for the SUT or components of the SUT in case that test procedures should be designed generated and evaluated before the SUT implementation is complete and an actual SUT exists that can take part in the test Simulations generated with RTT MBT already contain a connection to the test environment so that a generated test procedure can be compiled together with a simulated SUT without any further implementation The integration of a SUT i
51. the home directory of the chosen Overture project Then a new file with the appropriate file extension texttt cml will be created in the directory 4 5 Adding Standard Libraries In addition to adding new empty files it is possible to add existing standard libraries This can be done by right clicking on the project where the library is to be added and then selecting New Add CML Library That will make a new window as shown in Figure 11 Here the different standard libraries provide different standard function alities In the body of many of these functions operations are declared as is not yet specified but the actual functionality for all of these are hard coded into Symphony so the user can get access to this when the respective standard libraries are included This can be summarised as IO This library provides functionality for input and output from to files and the stan dard console Math This library provides functionality for standard mathematical functions such as sine and cosine Add Library Wizard Add Library Select the libraries to include Libraries V 10 Library v 1 0 0 V Math Library v 1 0 0 Configuration Used linked libraries Cancel Finish Figure 11 Adding New Libraries 17 D31 4a Symphony IDE User Manual Public COMPASS 5 The CML Type Checker The Symphony IDE ships with the CML Type Checker The Type Checker checks type consistency and referential integrity of your mo
52. the theorem prover Symphony supports both fully automated and manual discharge of proof obli gations Automatic discharge is the preferred method and should be attempted first To perform automatic discharge right click the model in the project explorer and select Theorem Proving Automatic Proof Obligation Discharge This is shown in Figure 54 This process checks that the CML model is supported by the theorem prover If there are any parts of unsupported syntax in the CML model an error message appears which informs the user A list of unsupported syntax is reported in the warning pane of the Symphony IDE The individual POs are also checked to ensure they use syntax sup ported by the theorem prover If the model is supported the POG perspective will be shown as per Figure 55 From here users may submit individual POs to the theorem prover by right clicking them and selecting Submit PO to Theorem Prover Alternatively all POs can be submitted at once by clicking Submit All POs the button labeled a in Figure 55 Finally it is possible to terminate the Isabelle session by clicking Terminate Session the button labeled b in However this functionality is still experimental and once a session is terminated Isabelle may not start up again correctly If this happens please restart Symphony Automatic discharge is capable of handling a significant number of POs However it may be unable to discharge particularly complex obligati
53. up the test generation process Suppose for example that the functionality of FLASH_ CTRL and OUTPUT_CTRL has been implemented in two different control components of the SUT If a complete regression test achieving transition coverage should be performed for FLASH_CTRL and the coverage thereby obtained for OUTPUT_CTRL is without relevance it suffices to mark all FLASH_CTRL transitions in the TC column while 95 D31 4a Symphony IDE User Manual Public COMPASS leaving the same column unmarked for OUTPUT_CTRL The RTT MBT tool analyses the coverage goals configured for the test procedure generation process and performs a so called cone of influence reduction on the model all model components that do not contribute to the coverage goals defined are automatically de activated during the generation process so that the constraint solver operates on a simpler transition re lation in this example the local relation specifying the behaviour of FLASH_ CTRL alone ROB marks transitions of the test environment as robustness transitions This means that they will only be executed if e the associated TE component has been activated for the test procedure genera tion e parameter RB robustness test generation ON OFF has been set to 1 in the ad vanced configuration see Section 12 7 3 and e parameter RP percentage of robustness transitions has been set to an integer value in range 100 in the advanced configuration see Section 12 7
54. value is set to 2 the analysis becomes more longer Expressions and predicates The use of expressions and predicates in constructs like guarded actions conditional statements etc is restricted to simple expressions We recommend that only ex pressions involving the operators x lt gt lt gt lt gt and or The use of complex expressions can make the STM solving activity slower as more constraints are manipulated internally Furthermore boolean expressions involving variables whose disjunctive normal form have more than two disjuncts are not allowed This is due to FORMULA limitations on manipulating disjunction For example the expressions value gt 5 and value lt 10anda lt 5o rb care allowed whereasa lt 5erb corb lt 3isnot Synchronisation values At the moment the model checker accepts only generic parallelism and only channel names or set of events in the synchronisation set Thus synchronisation in events with a specific values for example P chan 1 Qis not allowed l4Importable directly from the Symphony examples 69 D31 4a Symphony IDE User Manual Public COMPASS 10 The Symphony Fault Tolerance Tool In this section we present instructions for running the Fault Tolerance plugin via small examples Section 10 1 shows how to run the Fault Tolerance Plugin shows small CML models extracted and modified from Insiel s Emergency Response System ERS case study Th
55. zip and the contents are pure Java and inherently cross platform as a result All that is required to run the tool is a Java runtime environment version 1 7 Java 7 or later After downloading cmlc 0 4 0 zip decompress it into a folder In that folder will be the files cmlc cmlc bat and cmlc 0 4 0 jar Invoke the command line tool using either cml c Linux Mac OS X or cmlc bat Windows 14 1 Available Functionality The command line tool provides access to the following features in the core libraries e CML model parsing and typechecking e Proof Obligation Generation POG for CML models see Section 14 3 e CML model simulation see Section 14 4 e SysML to CML translation see Section 14 5 e Generation of graph representations of parsed CML models The CML parser is the primary element of the command line tool as nothing can happen without using it Generally the tool will read in a sequence of CML file s and then perform a typecheck on the abstract syntax tree AST At this point the data is ready to be used by the rest of the core libraries and plugins It is possible to run the core libraries on an AST that has not been typechecked but doing so is not recommended except to test error reporting or if the user only wishes to generate a graph representation of the AST The graph representation generator will output a SVG file containing a representation of the AST generated from the input CML files This depends on th
56. 1 Inspecting Proof Obligations This section provides brief instructions on how to use the POG plug in to inspect Proof Obligations POs Information on which CML constructs are supported by the POG can be found in Appendix B In order to inspect the POs for a given CML model the the user must select a CML project or a CML file right click and select Theorem Proving Inspect Proof Obli gations from the context menu This is shown in Figure 51 Once the POG has run successfully the generated POs are displayed in a view to the right of the editor if the default POG perspective is enabled If you click on any PO in this list its predicate can be seen in a frame below the PO list This is shown in Figure 52 Any PO can be double clicked and the editor will highlight the relevant portion of the CML model that yielded that PO which is also illustrated in Figure 52 POs can be displayed in one of two ways full obligation the default setting or de finedness predicate only The full obligation shows all contextual information for each PO whereas the definedness predicate only shows the portion of the PO that enforces definedness with no contextual information This version can sometime be more in tuitive to comprehend To switch between settings click Window Preferences Symphony POG see Figure 53 0Tt is beyond the scope of this document to describe the Isabelle syntax interested readers are directed to the Isa
57. 15 All of the existing CML launch configurations will appear under the CML Model To create a new launch configuration you may double click on the CML Model or on the New launch configuration button then an empty launch configuration will appear as shown in Figure 15 with the name New Configuration possibly followed by a number if this name is already used To edit an existing configuration click on the desired launch configuration name and the details will appear on the right hand side of the dialogue As seen in Figure 15 a project name and a process name need to be associated with a launch configuration along with the mode of operation as discussed in When choosing a project you can either write the name or click on the Browse button which 20 D31 4a Symphony IDE User Manual Public COMPASS CML Dwarf Dwarf cml Symphony IDE File Edit Navigate Search Project Run Window Help rie x i o aa bOr E CML Explorer X AlS Y o BDwarfcem X gt BitRegister types gt bO LampId lt Ll gt lt L2 gt lt L3 gt Signal set of LampId Y Dwarf ProperState Signal Dwarf launch DwarfType lastproperstate Properst gt RingBuffer turnoff set of L turnon set of L laststate Signal currentstate Signal desiredproperstate ProperSt inv d d currentstate d turnoff union d t fa turnatftt intar dA turnan l and Figure 14 Screenshot of the toolbar of the Symphony IDE showing the debug butto
58. 4 it differs both in scope only covers blocks as types and individual state machines and in the semantics which takes a synchronous view of events The distinctive feature of the semantics implemented in this plug in have been described in COMPASS Deliverable D31 4d ML14 Finally since XMI files produced by different tools are not in general compatible this tool assumes the file has been generated using Artisan Studio version 7 4 13 1 Exporting SysML models In order to export a SysML models into an XMI file we must first open the model on Artisan Studio Figure shows the Hybrid SUV HSUV example model in Artisan Studio it Te b Fs Se eee 4 D gt am eee ise baad 3 Properties of HSUVModel 5 HSUV ay E z a ModelingDomain HybridSUV I ext Options Changes Style tems Access Permissions O 1SuVMoce i Profiles B Annex C E ReadMe Type Package jed 19 2009 17 3 nybi Protectes ck a f y v Gree RAe e O O O a pe For Help press F1 Tornen Figure 101 HSUV model in Artisan Studio With the model open we must select the menu item Tools XMI Export as shown in Figure If the XMI menu is not available then the tool may not have been installed In this case re run the installation of Artisan Studio and select the XMI feature to be installed Next the destination XMI fi
59. Animate Simulate Co Simulation Mode External System Host localhost 8882 External Processes Apply Revert Filter matched 6 of 6 items Figure 24 Coordinator launch configuration with the Reader process as external 29 D31 4a Symphony IDE User Manual Public COMPASS r Debug Configurations Create manage and run configurations Debugs a CML Model GEax er Name RW Main gt Develop Common 4 be CML Co Simulation Model Project EJ RW CML Model Project ReaderWriter VDM PP Model E VDM RT Model P E VDM SL Model Process Reader Execution Mode Animate Simulate Co Simulation Mode Host localhost 8882 External Processes Select Configure External System A Revert Filter matched 6 of 6 items pply Figure 25 External system launch configuration for the Reader process co simulation engine the configuration must have at least one of either Reader or Writer designated as external In Figure 24 a launch configuration is shown for the coordinator and Figure 25 shows the Reader external system 30 D31 4a Symphony IDE User Manual Public channels a b int values MAX 10 process Main Writer a b Reader process Reader begin actions S a x gt x lt MAX amp b x gt s x MAX amp b x gt Skip s end process Writer begin actions s val x
60. E specifies with entry values 1 that the variable is an output of the SUT which may be observed in the testing environment If this variable cannot be observed by the TE its SUT writes to TE value has to be set to 0 TE writes to SUT specifies with entry values 1 that the variable is an input to the SUT which may be written to by the testing environment If the TE cannot write to a variable its TE writes to SUT value has to be set to 0 In some hardware in the loop testing environments the TE may write outputs in place of the SUT for example to override erroneous outputs of SUT components that might affect other parts e g a different controller in an SUT network of the SUT In these situations both the SUT writes to TE and the TE writes to SUT entries are marked by 1 and further definitions must be provided in columns Concrete Signal Identifier explained next Concrete Signal Identifier is only relevant if the testing environment uses different names for SUT inputs and outputs from the ones occurring in the model This is fre quently necessary in hardware in the loop testing environments where abstract model signals have to be mapped to concrete hardware interfaces with names depending on the HW drivers used In these situations the concrete name of an interface variable as it should be read by the TE during test execution is inserted in column Concrete Signal Identifier only filled in if TE may READ this signal Insert the variable
61. Group can send requests for new collab orators to join the Collaboration Project This ensures that no one has the control of the group and the authority is distributed Adding Collaborators The collaborators are selected by right clicking on the Collaborators node for the rele vant Collaboration Project in the Collaborative Modelling view and choosing the Add Collaborator menu item This will list the online contacts of the account that was used to create the connection in Section 7 1 as shown in Figure 32 Error Log Problems 4 Tasks Console 2a Messages Contacts lt Collaborative Modelling X eee a Collaborators gt hj attached to project Collab1 e 8162005 bF55 4083 a0b6 c42e75981370 gt O Test attached to project EmergencyMam e6ced7a0 2801 4aeb 9012 9d57e143b5b1 TaBa Systems Collaboration attached to project TaBa System efd93ad9 3829 4c70 b9e5 9b 5Fac8d8226 Configurations Collaborators Add Collaborator compass collab2 gmail com Figure 32 Add collaborator to project screenshot The Collaboration Request dialog will open in which a message to the recipient of the request can be entered as shown in Figure 33 Send collaboration request Send to compass collab2 gmail com Collaboration Title Lets collaborate Message Figure 33 Collaboration Request dialog The selected collaborator will then receive a join request with the name of the sender the title of the coll
62. L formalism Thus if you are not familiar with this we suggest the tutorial for CML before proceed ing with this user manual BGW12 However users broadly familiar with CML may find the Tool Grammar reference COMPASS Deliverable D31 4c Col14 useful to ensure that the they are using the exact syntax accepted by the tool Previous versions of the WP31 deliverables included an Examples Compendium doc ument that has been omitted from the overall Deliverable D31 4 package The relevant material however is available on the Symphony Tool ea and is also bundled with the Symphony IDE itself see Section 4 2 This version of the document supports version 0 4 0 of the Symphony IDE The intent is to introduce readers to how this version of the tool interacts with CML models The main tool is the Symphony IDE which integrates all of the available CML analy sis functionality and provides editing abilities The architectural relationship between Symphony and the rest of the tools used in the COMPASS project is shown in Fig Refinement Plugin Maude gt NY P Isabelle UTP CML Theorem Prover Plugin Proof Obligation Generator SysML to CML Translation J artisanStudio Static Fault Analysis Plugin Symbolic Model Checking Model Checker Plugin Microsoft FORMULA Distributed Simulation Fault Tolerance Verification Simulator Plugin
63. Lampid dw desiredproperstate stop SetNewProperState ProperState gt SetNewProperState st S setPs ProperState dw mk_DwarfTypeC dw currentstate Gshine Signal dw currentstate st SG thunk st dw currentstate v Q Dwarf init gt Init DWARF_TEST3 dw laststate a dw DwarfType dw currentstate p st a pie 0 E 7 Error Log Problems X 4 Tasks El Console 0 errors 1 warning O others Description Resource Path Location Type v amp Warnings 1 item amp Instance variable dw is not initialized Dwarf cml Dwarf line 68 Problem y Dwarf Figure 3 Outline of the Symphony Workbench o gt F ors i CML Process i _ i Q ak b a GA a w f int int ve gt b Fv Figure 4 The Outline view showing a CML process and its actions on the left On the right the Outline view shows a CML class The higher level elements of the outline can be collapsed or expanded to respectively hide or show their child nodes For example a process can be expanded in order to see its actions operations and so forth Clicking on the name of a definition will move the cursor in the editor to the definition The outline will also automatically highlight whichever node corresponds to the cursor position as it changes Finally it s important to note that the Outline view when displayed is only updated for source files that parse correctly Thus files that have pars
64. Modelling that provides a graphical overview of the current collaboration projects that this Symphony IDE instance is related to This graphical view makes it possible to see other collaborators view the exchanged configurations and files see the history of exchanged configurations and see which collaborators have approved or proposed adjustments to the shared model data A screenshot of the Collaboration view is shown in Figure 27 Error Log i Problems 4 Tasks E Console a Messages A Contactsi Collaborative Modelling X Test attached to project EmergencyMgm e6ced7a0 2801 4aeb 9012 9d57e143b5b1 Test attached to project EmergencyMgm e6ced7a0 2801 4aeb 9012 9d57e143b5b1 gt D Configurations 8 v Collaborators 2 mn compass collab gmail com mn compass collab2 gmail com Figure 27 Screenshot of the Collaborative modelling view 7 1 Connectivity between Symphony IDE instances The connectivity between the Symphony IDE instances is established using the open source Eclipse Communication Framework ECF The connectivity between all the participating collaborators is used to push notifications to all connected Symphony IDE instances in order to ensure that collaboration activity is shared rapidly The current version of the Collaborative Modelling plug in makes use of the open standard XMPF formerly Jabber protocol This makes use of a centralized server for relaying data between the different participants
65. SEVENTH FRAMEWORK PROGRAMME Grant Agreement 287829 Comprehensive Modelling for Advanced Systems of Systems COMPASS Fourth Release of the COMPASS Tool Symphony IDE User Manual Deliverable Number D31 4a Version 1 1 Date September 2014 Public Document http www compass research eu D31 4a Symphony IDE User Manual Public Contributors Joey W Coleman Aarhus Luis Diogo Couto Aarhus Kenneth Lausdahl Aarhus Claus Ballegaard Nielsen Aarhus Anders Kaels Malmos Aarhus Peter Gorm Larsen Aarhus Richard Payne Newcastle Simon Foster York Alvaro Miyazawa York Uwe Schulze Bremen Adalberto Cajueiro UFPE Andr Didier UFPE Editors Joey W Coleman Aarhus Reviewers Uwe Schulze Bremen Richard Payne Newcastle Adrian Larkham Atego COMPASS D31 4a Symphony IDE User Manual Public COMPASS Document History 0 1 02 12 2013 IWC 02 03 03 2014 15 07 2014 IWC Structure check SSS 0 5 22 07 2014 JWC Update Cosim amp Commandline sections tidy simulator support 0 6 22 07 2014 Added screenshots for S2C lite 0 7 23 07 2014 ALRD Unified document formatting Up Ver dated the examples and the required definitions to run the FT verification 23 07 2014 HM Added text to the instruction on how to use S2C lite 3 07 A 23 07 2014 LDC Check and clean up sections 3 6 and 8 updated section 9 with new POG TP interaction A T Di T 14 28 07 2014 Edit Theorem Proving
66. The information of each state has the format vars proc where vars contains the manipulated variables bindings and proc is a process frag ment Furthermore the generated files can be viewed by refreshing the project The user can see the content of all files 4m1 gv and svg as they are text files Fur thermore a trace provided by the model checker can be exercised directly in the CML animator to provide an interactive way to reach the deadlock When the analysed process is unsatisfiable the property checked is not valid in the model and the user tries to see the graph the model checker plug in returns a message indicating that the graph is available only for satisfiable models Figure 74 Thus if the user checks a process for deadlock and it is unsatisfiable there is no trace leading to deadlock and hence does not make sense to build such a trace Symphony Oo Counterexample construction available only for satisfiable models Figure 74 Message when the graph is not available Models from B amp O There are three models from B amp O analysable in the model checker Streaming CoSimulation and Device discovery Concerning the third model there are constructs like Wait Timed timeout interruptions etc and there is a a process called 65 D31 4a Symphony IDE User Manual Public COMPASS TargetProduct_DD_SD_InterfaceProtocolView that performs an input on channel TPMulticastChannel which supports t
67. Timeout A ee gt B Abstraction A es Comments terminate immediately It yields a state with no outgoing transition can always choose to communicate or reject any event It yields a livelock Wait for e time units offers the environment a choice of events if e is true behave like A otherwise behave like St op behave like A until A terminates then behave like B offer the environment the choice between A and B nondeterministically behave either like A or B Interrupt A by B Interrupt A by B for e time units Timeout to B Timeout to B after e time units behave as A with the events in cs hidden Table 13 Action constructors 131 D31 4a Symphony IDE User Manual Public COMPASS Operator Syntax Comments Start deadline A startsby e Not implemented End deadline A endsby e Not implemented Channel renaming A c lt nc Not implemented Recursion mu X F X Definition of a recursive action Mutual Recursion A in the mu form full support when using mu mu X Y r X Y Gt X Y tual equations Interleaving A nsi ns2 Net implemented Interleaving no state A B execute A and B in parallel without synchronising Neither A nor B change the state Synchronous parallelism A nsl ns2 B Notimplemented Synchronous parallelism no state A B Not implemented Alphabetised parallelism A nsl csl1 cs2 nsP N implemented Alphabetised parallelism
68. _LFTSimple gt receiveMessage 2 startRecoveryl gt logFault1 gt resendRescueInfoToEru gt resendRescuelnfoToEru 29 processMessage gt receiveMessage gt endRecoveryl gt sendRescuelnfoToEru 30 serviceRescue gt NOMINAL LFTSimple i 4 m b lt 4 j 9 Error Log E Problems 4 Tasks E Console Sig Progress E Markers 53 g g error 2 warnings 1 other A Description Resource Path Location Type 4 Fault tolerance problem 4 items O The system defined by process NETSimole is NOT fault toleran_insiel ft werif ___ InsielSimpleFtVerification NFTSimple line 35 Fault tolerance problem amp No system should be full fa Clear fault tolerance markers jelSimpleFtVerification FFTSimple line 64 Fault tolerance problem amp The system defined by proc Goto ielSimpleFtVerification DLSimple line 49 Fault tolerance problem The system defined by proc jelSimpleFtVerification LFTSimple line 20 Fault tolerance problem 3 Copy Ctrl C ao Malaia Malaia Figure 78 Clear fault tolerance verification messages on the Markers view 10 1 1 Known issues The Fault Tolerance Plugin has been tested only with small examples as those shown in and may therefore contain bugs The only currently known issue is on the first execution of the plugin when Symphony is started The model checker preparation phase returns an error when generating the FORMULA files for the CML model Subsequent executions of the plugin should run normall
69. able events one will be chosen in an arbitrary but deterministic manner In other words the simulation will always make the same choices for every run of the same model 2 Animate This option will interpret the model with user interaction All observ able events are selected by the user 3 Remote Control This option enables the interpreter to be remote controlled by an external Java class implementing the RemoteControl interface and located in the lib folder of the project The interpreter also supports breakpoints Breakpoints can be set at any line in the model Once the line with the breakpoint is reached the execution is suspended and the current state of the model including variable values may be inspected The modes of operation controls the interpreter s behaviour with respect to breakpoints are 1 Run This will simulate animate the model ignoring any breakpoints 2 Debug This will simulate animate the model and suspend execution at all en abled breakpoints 6 1 Creating a Launch Configuration To create a launch configuration first click on the small arrow next to either the debug button or the run button depending on the desired mode as shown in Figure 14 Once clicked a drop down menu will appear with either Debug configurations or Run configurations depending on which button you clicked select the appropriate config urations option This will open a configurations dialog like the one shown in Figure
70. aboration project and the message entered in the Collaboration Re 36 D31 4a Symphony IDE User Manual Public COMPASS quest dialog Figure 34 shows the Join request dialog in which the collaborator can choose to join or decline the collaboration request Collaboration request received Collaboration request received From compass collab gmail com Title TaBa Systems Collaboration Message from Lets collaborate sender Collab2 Attach collaborative work to this project EmergencyManagement TaBa Sys Figure 34 Collaboration Request Received dialog When the collaborator joins the collaboration the sender of the request will be notified by a small pop up box as shown in Figure 35 Error Log L Problems Tasks Console Contacts X Collaborative Modelling 4 Messages Console el compass collab2 gmail com o clausbn123 A compass collab Collaborative Modelling plugin compass collab2 gmail com Joined Collaboration Figure 35 Joined notification Deleting Leaving a Collaboration Project A collaborator can leave a collaboration project by deleting it from the Collabora tion View Deleting a project will remove the project from the list of Collaboration Projects and it will also notify the other collaborators that this collaborator has left the collaboration and therefore no further data exchanges will be made with this particular collaborator Deleting a project will n
71. al is allowed for parameter Table 26 Declarations 145 D31 4a Symphony IDE User Manual Public COMPASS D 3 Types Operator Syntax Comments Type Declaration The type Index is defined as a natural number whose values are limited by the invariant expression That Cypes is the value of Index can be from 1 to 10 Only basic Index nat inv a types are allowed to be used as types of user defined i in set l 10 types Field types are not allowed Table 27 Types 146 D31 4a Symphony IDE User Manual Public COMPASS D 4 Operations Operator Syntax Comments Operation Declaration It defines a new operation Credit which receives a operations natural number and does not return values The se Credit nat gt mantics of Credit is to change the value of balance Credit n which should had been defined in the state Pre and post conditions are nor allowed The constructs frame rd and wr are not allowed balance balance n Table 28 Operations 147
72. alification for model based testing tools In Brian Nielsen and Carsten Weise editors Testing Software and Systems Proceedings of the 24th IFIP WG 6 1 International Conference ICTSS 2012 Aalborg Denmark November 2012 number 7641 in Lecture Notes in Computer Science pages 8 23 Heidelberg Dordrecht London New York 2012 Springer Joey W Coleman Fourth release of the COMPASS tool CML grammar reference Technical report COMPASS Deliverable D31 4c September 2014 John Fitzgerald Peter Gorm Larsen and Jim Woodcock Modelling and Analysis Technology for Systems of Systems Engineering Research Challenges In INCOSE Rome Italy July 2012 Simon Foster and Alvaro Miyazawa Formal refinement support Techni cal report COMPASS Deliverable D33 4 September 2014 Simon Foster and Richard J Payne Theorem proving support developers manual Technical report COMPASS Deliverable D33 2b September 2013 M Leuschel and M J Butler ProB an automated analysis toolset for the B method STTT 10 2 185 203 2008 Kenneth Lausdahl Anders Kaels Malmos Claus Ballegaard Nielsen Joey W Coleman and Klaus Kristensen Co simulation engine Tech nical report COMPASS Deliverable D32 4 June 2014 Alvaro Miyazawa and Peter Gorm Larsen Fourth release of the COM PASS tool sysml to cml translation mitigation effort Technical report COMPASS Deliverable D31 4d September 2014 Jan Peleska Elena Vorobev Florian Lapschie
73. altered in the test model testers just need a test procedure verifying these transitions Moreover state machine transition coverage is regarded as the typical test coverage criterion to be applied when ever the SUT has to be tested in a reasonably thorough way but is not safety critical or business critical so that the more sophisticated coverage criteria described in Ver13b should be applied SC is used for quickly defining modified condition decision MC DC coverage goals SC stands for safety critical because MC DC coverage is the most common cover age criterion to be applied in the context of safety critical systems testing see the avionic standard WG 11 and for explanations about this coverage crite rion As shown in Figure transitions have to be marked in both the TC and the SC columns if MC DC coverage should be realised by the test procedure to be cre ated As for transition coverage marking MC DC coverage goals in columns TC and SC is just a short cut for selecting the MC DC coverage test cases associated with this transition Note however that in contrast to transition coverage several test cases are associated with the goal to cover one transition according to the MC DC criterion the transition has to be exercised with differing valuations of the atomic conditions contributing to the guard condition and several stability conditions where the state machine remains stable in its current control state have to
74. aspects of the tool such as parametrised laws and proviso management is provided in D33 4 82 D31 4a Symphony IDE User Manual Public COMPASS 12 RT Tester Plug In This chapter describes the RT Tester Model Based Testing RTT MBT functionality provided by Symphony using the RT Tester plug in RTT Plugin The user interface is explained together with the basic information about model based testing with RT Tester It covers the areas from creating a test project selecting and using a specific UML SysML model to generate test procedures from as well as defining and control ling the test procedure generation process and finally executing and evaluating concrete test procedures Model Based Testing is a complex task and RTT MBT provides a lot of functional ity that can be configured to generate test procedures reaching the desired test goals The focus of this user manual is to describe the RTT Plugin and how it can be used as a front end to RTT MBT Additional information about RTT MBT can be found in a separate manual that also describes model based testing with RT Tester but describes the usage of the RT Tester graphical user interface from Verified Systems which is not integrated in Symphony Note that in Ver13b you will find additional chapters about generating test models defining test goals using the model checking capabilities of RTT MBT as well as different test strategies and the supported UML and SysML model elements and LTL s
75. at will act as the coordinator of the simulation Select external processes and attach them to a collaborator Select Coordinating process EmergencyCoordination Simulate Animate External Process To be simulated by Status EmergencyCoordination Ambulance compass collab3 gmail cor Police _compass collab2 gmail cor Figure 43 Initiate Distributed Simulation dialog Once the distributed simulation has been configured a request can be sent to the se lected collaborators prompting them to participate in the distributed simulation and to simulate specific processes The collaborators will be presented with the name of the simulations coordinator the name of collaboration project and the name of the process that needs to be simulated as illustrated in Figure 44 When receiving a simulation 42 D31 4a Symphony IDE User Manual Public COMPASS request the request can either be declined or accepted If the request is declined the dialog will close and nothing more will happen with regards to the simulation If the request is accepted the dialog will remain open pending the coordinator starting the distributed simulation Distributed Simulation requested compass collab gmail com requested this symphony instance to collaborate ina distributed simulation Participate Collaboration Project Collaboration Project TaBa Systems Collaboration Simulation of process Police Status Approve _no decire
76. ation Generator POG 128 B I Processes adn Bx ARKHDR ED ORR DR RRR EE 128 Pe Classe 5 eee OSES OE AeA ERE eee 128 B 3 Actions o 1 sinus bh Oo ho Re eee GS KD REO eS 128 B 4 Channels and Chansets 0 0 0 0 0 0 000 128 B 5 Namesets 0 0 000 000 eee ee 128 Doe eee ee eee eee epee e eee nee ee ee en 128 ae ee ee ee ee 128 B S Functions se ox lt 4 4k we amp ORG a RGR De a 129 BO Vil s s neh bak eee eh eee eee eee 129 ee ee E E 129 130 C l Actions oe es eee ee a 131 C 2 Declarations 0 0 0 0 0 0000 2 ee eee 136 ee ee ee ae ee ee ee ee 137 a ee ee ee 137 ooo ee ee eee ee eee Bae ee ee eS 138 D31 4a Symphony IDE User Manual Public COMPASS 139 Deoa e eee eee ee a ee eee a 140 D 2 Declarations 0 0 0 0 L 145 ee ee ee ee 146 EE i D31 4a Symphony IDE User Manual Public COMPASS 1 Introduction This document is a user manual for the Symphony IDE produced in the COMPASS project an open source tool supporting systematic engineering of System of Systems SoSs using the COMPASS Modelling Language CML The ultimate target is a tool that is built on top of the Eclipse platform that integrates with the RT Tester tool and also integrates with Artisan Studio This document is targeted at users with limited experience working with Eclipse based tools Directions are given as to where to obtain the software This user manual does not provide details regarding the underlying CM
77. ation postfixed with Received Received model data will not become part of the overall model before the receiver has approved of it Meaning that the tool will not include the received model data into the project workspace until the receiver manually includes it into the workspace As a result all the files received via Configurations are 39 D31 4a Symphony IDE User Manual Public COMPASS stored within the project but do not become visible in the project explorer and thereby for analysis in the tool until requested Activating Received Model Data A received Configuration is made active in the workspace by right clicking the Config uration and selecting the Activate Configuration menu as show in Figure 40 Error Log Problems 4 Tasks Console 2a Messages Contacts amp Collaborative Modelling c4e45d71 Fri Aug 08 16 32 25 CEST 2014 Received gt hj attached to project Collab1 e8162005 bF55 4083 a0b6 c42e75981370 gt D Test attached to project EmergencyMgm e6ced7a0 2801 4aeb 9012 9d57e143b5b1 v TaBa Systems Collaboration attached to project TaBa System efd93ad9 3829 4c70 b9e5 9b 5fac8d8226 Y D Configurations 1 Y _ c4e45d71 Fri Aug 08 16 32 25 CEST 2014 Received v E Files 1 gt fll System cml Fri Aug 08 16 32 25 CEST 2014 gt 3 Sent To 1 gt Collaborators 2 Activate configuration introduce files into workspace Approve Reject Diff with previous configurati
78. automatically be derived from this model in form of LTL formulas These test cases define the precondition and input values but not the expected outputs because these are already defined in the model describing the expected behaviour of the system under test The expected outputs are calculated by test oracles that are executed together with a test procedures covering the test cases Test Procedure Detailed instructions for the set up and execution of a given set of test cases and instructions for the evaluation of results of executing the test cases RTCA DOI78B In RTT MBT test procedures can automatically be generated from a test model for a given set of goals test cases specified as LTL formulas These test procedures are separated into a stimulation component that performs a timed sequence of SUT inputs and number of test oracles that observe the stimulations and check for the expected output of the different system components Test Oracle A source to determine expected results to compare with the actual re sult of the system under test With RTTI MBT oracles are generated as parts of test procedures For each component of the SUT in a test model a test oracle is generated checking for the expected behaviour of the respective component Test Generation In this document test generation describes the process of calculat ing concrete system under test inputs and expected outputs for a given number of test cases goals in the form of LTL f
79. be explored This is il lustrated for example by the MC DC test cases related to control state IDLE in state machine OUTPUT_CTRL of the sample project Finally observe that some MC DC conditions and their associated test cases may be infeasible The stability condition 94 D31 4a Symphony IDE User Manual Public COMPASS IMR TurnindLvr 0O lt 0 amp amp IMR SystemUnderTest FLASH_CTRL tilOld O IMR TurnIndLvr 0 amp amp IMR SystemUnderTest FLASH_CTRL FLASH_ CTRL EMER_ON EMER_ACTIVE O amp amp IMR EmerSwitch 0 amp amp IMR TurniIndLvr 0 0 IMR SystemUnderTest FLASH_CTRL tilOld 0O IMR TurnIndLvr 0 for example cannot be fulfilled due to the contradictory atomic conditions IMR TurnindLvr 0 lt 0 amp amp IMR TurnindLvr 0 0 and IMR SystemUnderTest FLASH_CTRL tilOld O IMR TurnIndLvr 0 amp amp IMR SystemUnderTest FLASH_CTRL tilOld 0O IMR TurnIndLvr 0 because IMR TurnIndLvr always carries non negative values Note however that RTT MBT can identify most infeasible test cases This is performed when creating the test case database from the test model and the infeasible test cases are recorded in directory model unreachable testcases csv where you will find the infeasible MC DC test case discussed above so that these do not have to be covered in test campaigns SIM marks test model components as simulations For components residing in the test environment this is mandatory so un
80. belle tutorials as in footnote 8 50 D31 4a Symphony IDE User Manual Public COMPASS E cm Explorer 2 O A pwarf cmi 38 elite Y types vow f v LampId lt Ll gt lt L2 gt lt L3 gt nal Signal set of LampId Dwa ate Signal E Dw New gt ps in set dark stop warning drive gt get Open B RE Open With gt e lastproperstate ProperState gt E intrTe turnoff set of LampId B Copy C turnon set of LampId Pas laststate Signal aste currentstate Signal Delete gt desiredproperstate ProperState Move R urrentstate d turnoff union d turnon d menama F2 hoff inter d turnon and ej Import erShow All A Export entstate lt gt lt L1 gt lt L2 gt lt L3 gt and aap OneLampChange Refresh F5 d currentstate d laststate union d lasts amp bidStopToDrive a stproperstate stop gt d desiredproperstate Validate kOnlyToStop Debug As gt stproperstate dark gt d desiredproperstate Run As p kOnlyFromStop Team gt siredproperstate dark gt d lastproperstate Compare With gt hal DwarfType Replace With gt NeverShowAll d and Theorem Proving gt Check TP compatibility Properties 381 Inspect Proof Obligations Ty Automatic Proof Obligation Discharge Manual Proof Obligation Discharge Manual Proof Session Figure 51 Invoking the Symphony POG 8 4 2 Discharging Proof Obligations POs are automatically generated by the POG and can be discharged by
81. c COMPASS Select Export resources to an archive file on the local file system Select an export destination type filter text Y amp General File System Preferences gt Install gt amp Run Debug gt Team a finish Figure 9 Select an output format for the exported process o Export Archive file Please enter a destination archive File B project g amp ConstituentA g amp ConstituentB g amp Constituentc Filter Types Select All Deselect All To archive file Options Save in zip format Create directory structure for files Save in tar format Create only selected directories Compress the contents of the file Figure 10 Project ready to be exported 16 D31 4a Symphony IDE User Manual Public COMPASS 4 4 Creating Files Switching to the CML perspective will change the layout of the user interface to focus on CML development To change perspective go to the menu Window Open per spective Other and choose the CML perspective From this perspective you can create files using one of the following methods 1 Choose File New CML File or CML Class or CML process or 2 Right click on the Overture project where you would like to add a new file and then choose New CML file or CML Class or CML process In both cases you need to choose a file name and optionally choose a directory if you do not want to place the file in
82. c COMPASS 00090 Properties for TP 001 type filter text RT Tester iv vY gt Resource Project Database Name uwe_verified_de_TurnindicationDemoProject Run Debug Settings Test Execution Context TestExecution Test Generation Context TestGeneration Make tool for SUT code make Ignore Pattern for File Transfer svn git 0 Max Solver Steps 100 Max Simulator Steps 0 Max Number of simultaneous Input Changes 1 Min Duration between Input Changes 10 Min Duration between Input Changes 10000 Use Abstract Interpreter 1 Robustness Testing 0 Robustess Percentage 0 Model Checking 0 Restore Defaults Apply Cancel oK 4 Figure 97 Properties page of a test procedure generation context decremented The following simulation steps continue to decrement this value until a new model element is covered or the value becomes zero In the former case the value is set back to MAX SIMULATION STEPS In the latter case the simulation is stopped and the constraint solver tries to reach one of the remaining test goals from the model state reached by the simulation The default value is O no simulation with random data generation Default configuration Ifthe default values are suitable for a new test procedure to be generated it is not necessary to edit the basic configuration The initial test procedure generation context Test Procedures _P1 is created with such a default configura tion Observe however that
83. cal output generated in several formats to be presented Graph Viz is available at http www graphviz org and can be installed on several platforms The CML model checker uses specifically the dot exe program which provides compilation from a textual description to several formats We use the SVG format that is vectorial and accepted by most of Web browsers 9 2 Differences from other tools The main differences of the CML model checker from other popular tools ike FDR or PAT include the way these tools are developed performance and the capability of handling infinite types FDR and PAT have been implemented following the usual model checker implementa tion approach where search based algorithms are implemented to provide the desired functionality The CML model checker on the other hand uses the strict relation be tween the formal semantics of the language and its analysis Indeed the CML model checker was created by following the structured operational semantics of CML and is therefore semantically well founded Furthermore the development cycle of the back end of the model checker is about a few weeks assuming knowledge of FOR MULA Mnttp www microsoft com visualstudio 58 D31 4a Symphony IDE User Manual Public COMPASS Concerning performance FDR and PAT have many internal optimizations that make these tools faster than the CML model checker Furthermore as the CML uses SMT solving it is reasonably expected that it
84. cation of the Isabelle application for example Applications Isabelle2013 2 app For Mac and Linux in the second text box labelled b in Figure 46 navigate to the location of the utp isabelle folder extracted in Section Use the Browse button to navigate to the correct location if required This step is not required for Windows Click the Ok button to save the configuration and to finish the setup procedure Once setup from the menu bar select Theorem Prover Launch Theorem Prover to run Isabelle NOTE the first time Isabelle is invoked several min utes are needed to initialise and build the theories Subsequent uses of Isabelle will not require this long wait To monitor progress click on the button on the bottom right of the tool as highlighted in Figure 47 Troubleshooting More detailed instructions are provided at the Isabelle Eclipse web site which may be of use 47 D31 4a Symphony IDE User Manual Public COMPASS Insert 9 15 Launching Isabelle CML 57 Figure 47 Isabelle configuration in Symphony initialisation progress http andriusvelykis github io isabelle eclipse getting started If errors persist please report them using the Symphony bug tracking facility https github com symphonytool symphony issues new 8 3 Using the Isabelle perspective with the Symphony IDE The steps in this section should be followed to begin proving theorems using the Is abelle th
85. ces as shown in Fi gure 79 You must provide the path to the Maude binary and the path to the Maude encoding cml refine maude provided with the Symphony IDE For example if the Symphony IDE was installed into home user SymphonyIDE then the path in Maude CML location should be home user SymphonyIDE refinement cml refine maude Preferences lE Maude Setup Ov v gt General gt Ant gt Help gt Install Update Maude CML location home user cml refine maudel Browse gt Isabelle Setup values for using Maude for refinement Maude binary location usr bin maude Browse gt Java gt JavaScript Maude Setup gt Maven Model Checker Setup gt Play gt Plug in Development gt RT Tester gt Run Debug gt Scala gt Scala Worksheet gt Symphony gt Team Theorem Prover Setup Validation gt VDM gt Web gt XML Restore Defaults Cancel Figure 79 Maude configuration 78 D31 4a Symphony IDE User Manual Public COMPASS 11 2 The Refinement Perspective Next the refinement perspective must be selected as shown in Figure 80 Open Perspective Java Browsing fe Java Type Hierarchy JavaScript me Model Checker Plug in Development E POG PO Proof Obligation Resource W RttPerspective amp scala 5 Team Synchronizing VDM x XML Figure 80 Selection of refinement perspective The refinement perspective consists of six areas as shown in Figure 8 1 CML Expl
86. d elseif e2 then a2 x else an Cases statement Not implemented cases e pl gt al p2 gt aZ others gt an end Nondeterministic do statement Not implemented do el gt al e2 gt a2 end Sequence for loop for e ins doa Not implemented Set for loop for all e in set S do a Notimplemented Index for loop for i el to e2 by e3 dg Not implemented While loop while e do a Not implemented Table 25 Control statements 144 D31 4a Symphony IDE User Manual Public COMPASS D 2 Declarations Operator Syntax Comments Value Declaration values Definitions of values to be used in a cml model value definitions Value Definition N nat It declares the value N as a natural number and assigns the value 2 to it Channel Name Declarations channels It declares the channels a and b supporting a specific ay D 3 Type type Chanset Declarations chansets It declares sets of events at once chanset definition Nameset Declarations namesets Not implemented nameset definition State Declarations state It defines the state structure containing the variable value nat value Qualifiers and invariants are not allowed in in stance variable definitions Process Declaration process P val x nat It declares the process P with a parameter Only the process_body qualifier val is allowed Action Declarations actions It declares the action A with the parameter 1 Only the A val i int action qualifier v
87. d 5 d w rer Cis TE B Outline 3 B CML Explorer 23 Lampld Sianal Ba east Roete a Figure 49 Running Isabelle and selecting Isabelle perspective ace 2 s ES Ccm poc dh isabelle D theory Dates imports Main begin type_synonym day nat datatype month Jan Feb Mar Apr type_synonym year nat primrec monthNumber month nat definition months month list where CML_PO_Example D Sortie ie monthNumber Nov gt Ef Examples k W S isabelleTestProj monthNumber Dec S Dates thy definition months month list where definition numberMonth nat month months Jan Feb Mar Apr May June July Aug Sep Oct Nov Dec Y H lemma monthNumber_inv simp numb Ui Travel Agent S apply definition numberMonth nat gt month where S apply numberMonth n months n 1 S apply S apply Project an lemma monthNumber_inv simp numberMonth monthNumber m m Explorer apply unfold numberMonth def Theory apply unfold months_def apply case_tac m apply simp_all s Outline done S apply S apply lemma atLeastAtMost_unfold m lt n Theory File Suc m n S apply v don by auto e lemma month_list simp UNIV set ma S apply S apply S apply S apply lemma numberMonth_inv simp n 4 nat i2 gt montnnumoer numoermonth n n apply
88. d theorems in Isabelle perspective 57 D31 4a Symphony IDE User Manual Public COMPASS 9 The Model Checker Plug In The CML Model Checker MC is part of the Symphony IDE concerned with support for analysing models in terms of classical properties deadlock livelock and nondeter minism and in the case of a property that is valid it also provides a useful information about model s behaviour a trace that validates the analysed property Furthermore the model checker provides support for the Fault Tolerance Plugin detailed in Section 10 in the sense that fault tolerance analysis relies on model checking 9 1 Installing Auxiliary Software The CML model checker is developed on top of the Microsoft FORMULA tool and GraphViz The first is used as the main engine to analyse CML specifications whereas the second is used to show any counterexamples found by the analysis The steps to install the CML model checker to work are listed as follows 1 Download and install the Microsoft FORMULA tool It is available at cesearch microsoft com en us um redmond projects formula Although the tool is free it requires Microsoft Visual Studid This makes the current version of the CML model checker platform dependent as the underlying framework is from Microsoft 2 Download and install the GraphViz software GraphViz is open source graph vi sualization software It allows several kinds of graphs to be written in a text file and graphi
89. d turnoff union d turnon d de f inter d turnon and ey Import how All t Export state lt gt lt L1 gt lt L2 gt lt L3 gt and LampChange Refresh f5 currentstate d laststate union d laststal i StopToDrive Validate roperstate stop gt d desiredproperstate lt Deki A gt LyToStop ebug AS roperstate dark gt d desiredproperstate ir Run As gt LyFromStop Team gt edproperstate dark gt d lastproperstate ir Compare With A oe fType Replace With Poi LanChawAl1 land Theorem Proving gt Check TP compatibility Inspect Proof Obligations Automatic Proof Obligation Discharge L Manual Proof Obligation Discharge Manual Proof Session Properties l rm Figure 56 Invoking automatic proof obligation discharge thy file extension a model specific read only file for the CML model lt modelname gt thy and a user editable file lt modelname gt _User thy These files along with a read only version of the CML model are added to a timestamped folder in the PROJECT generated Isabelle folder of the CML project see Figure 57 As with PO discharging this file is specific to the current state of the model Any changes made to the CML model will not be reflected in the thy file and thus the process must be restarted 54 D31 4a Symphony IDE User Manual Public COMPASS rA vw m CML Explorer 33 Fs m T CML Project Dwarf a A Dwarf cml d Dwarf v0 zip B Dwarf xml
90. del Type consistency includes check ing that operator and variable types are respected Referential integrity includes check ing that named references exists and have an appropriate type for their context 5 1 Output The type checker produces two kinds of artifacts Type Errors and Type Warnings Both carry a reference to the offending part of the model a description of what is ill formed and an exact location of where the issue occurred 5 2 Representation In the Symphony IDE user interface type errors show up in three places To point the user at the exact piece of CML source causing an error an error marker will be shown in the left margin of its Editor Additionally the problematic piece of syntax will be underlined with red as seen in Figure 12 kef CML Explorer 24 O Error cml 23 HI T class ErrorClass begin gt 8 Airport b2 AVDeviceDiscovery Fun ction gt 124 BitRegister f i U0t 2 bool b ChoiceSupportinDebugger veoh OFA Atal b 1 Dwarf end a y3 IncubatorMonitor b ya RingBuffer b w Stack i TypeError P Fam Error cmil Figure 12 User Interface showing type error markers Type errors are also made visible in the user interface through the CML Project Ex plorer The CML Project Explorer offers a tree view of CML model file structure If an error occurs in a CML source file then all of folders containing that file up through the hierarchy to the project level will have a red error marker
91. dentified and the PASS FAIL results are validated during the replay process The reason for performing replays is twofold e Some test cases refer to internal model states that cannot be observed during test execution against the SUT but can be identified by the model interpreter when running the test execution log against the model e Replay is a redundant procedure operating orthogonally to the automated test procedure generation An error that may have been produced by the genera tor will be uncovered during replay with high probability Therefore replay is 105 D31 4a Symphony IDE User Manual Public COMPASS mandatory to be performed when RTT MBT is applied for the test of safety relevant software replay is an essential pre requisite to RTT MBT tool qual ification this is described in more detail in BPS12 For application of test automation tools in a safety critical context only qualified tools may be used More details about tool qualification are presented in Ver13b To replay a test procedure executed before select the test procedure in the execution context using the Project Explorer and issue the Replay command in the tool bar the RTT MBT menu or the Test Execution context menu As a result of the replay com mand execution a log file is stored in the log directory of the test procedure generation context of the selected test procedure TestGeneration lt TestProcName gt log covered_testcases csv listin
92. e Fault Tolerance Plugin works together with the CML model checker as described in Chapter 9 In D24 2 we extended the SysML to CML mapping rules to allow the verification of fault tolerance in a SysML model If these mapping rules are not used the CML model to be verified must be annotated manually with faults errors and failures as is done in the examples in Section 10 2 When annotating a CML model several definitions must be provided The plugin is able to create some automatically but the following definitions must be provided unwanted lt any type gt The unwanted events channel It can be of any CML type for example unwanted int H The set of events chanset that should be hidden These events are those related to the recovery mechanisms activation and its internal actions It can be empty if there is no channel to be hidden Alpha_ lt name of the system process gt The alphabet of the process chanset It does not include the unwanted events Limit_ lt name of the system process gt This process limits the behaviour of the system avoiding execution of failures which are those unwanted events that the system is not expected to tolerate This definition is only used on the Limited Fault Tolerance verification In some cases the plugin tries to provide missing definitions as outlined in Table 1 Table 1 Cases where the plugin tries to provide missing items If not provided Tries to create it with H Chanse
93. e Figure 25 for illustration Note that the options above are specific to a remote simulator configuration an alterna tive configuration for external systems based on native code is described in Deliverable D32 4 LMN 14 A co simulation requires the coordinator to be started first so that it is listening for clients before the external systems are started This allows any external system to connect and register by informing the coordinator which process the external system implements Note that current constraints mean that only one instance of a given pro cess may be externalised neither processes in a replicated operator nor parametrised processes may be externalised A Reader Writer example CML model is provided in The screenshots in Figure 24 and Figure 25 assume this example as a basis for the values in the dialogs The example itself is a CML specification of a reader writer system where the top SoS process is Main The top process constructs the SoS using a single Writer and Reader process in parallel synchronizing on the channels a and b To use the r OEE Sa Debug Configurations m Create manage and run configurations Debugs a CML Model SBx e Pr Name RW type filter text Main gt Develop Common 4 CML Co Simulation Model A Rw See A CML Model Project ReaderWriter Browsen EJ VDM PP Model i VDM RT Model _ i VDM SL Model Process Main Search Project Top Process Execution Mode
94. e Graphviz suite of graph visualization utilities P The output is useful for producing a visual representa tion of the data used internally by the COMPASS tool to represent the static structure of a model of a system of systems This allows a developer to quickly verify whether the input CML files result in the expected internal data structures General user use 1s not recommended Found athttp www graphviz org 112 D31 4a Symphony IDE User Manual Public COMPASS 14 2 Basic Invocation After obtaining the command line tool package decompress it into a folder In that folder will be among others the files cmlc and cmlc bat Invocation of the cm1 c Linux Mac OS X or cmlc bat Windows script with no parameters will produce the following output Symphony command line CML Checker Usage cmlc switches lt filel gt lt fileN gt Switches dot Enable dot graph output to file lt out gt dot lt out gt dotpath The path to the dot binary dotpath lt path gt Enable simulation of process lt procID gt e lt procID gt Interactive mode read input from stdin Disable typechecking Enable Proof Obligation Generator output Enable state machine to CML tranlation s2c lt xmiFile gt Assuming some CML model in a file example cm1 loading it into the command line interface is accomplished by typing cmlc example cml If run in this manner the output will be Symphony command line CML Checker Parsing files
95. e errors will not have their Outline view updated 12 D31 4a Symphony IDE User Manual Public COMPASS 4 Managing Symphony Projects This section explains how to use the tool to manage CML projects Step by step in structions for importing exporting and creating projects will be given 4 1 Creating new CML projects Follow these steps in order to create a new CML project 1 Create a new project by choosing File New Project Symphony project see Figure 5 2 Type in a project name see Figure 6 3 Click the button Finish 8 0 8 New Project Select a wizard lt gt Wizards type filter text PB CML Project EJ vom PP Project A VDM RT Project P VDM SL Project gt General gt Overture Y amp Symphony E CML Project lt Back Next gt Cancel Finish Figure 5 Create Project Wizard 4 2 Importing Symphony projects 4 2 1 Symphony example projects The Symphony IDE comes bundled with a package of examples that users may exper iment with To import them into the workspace use the following procedure 1 Right click the explorer view and select Import then choose Symphony Sym phony Examples See for more details Click Next to proceed 2 The available example projects will be presented in the next dialog as shown in Choose the desired examples then click Finish and they will be automatically imported into your workspace An overview of all the CML projects tha
96. e expression types are implemented no detailed overview of them is given here The overview is divided into two subsections actions and statements which is a sub group of actions and processes Each subsection contains a series of tables that group similar categories The first column of each table gives the name of the operator the second gives an informal syntax and the last is a short description that gives the oper ator s status If a construct is not supported entirely no or partial implementation of the semantics then the name of operator will be highlighted in red and a description of the issue will appear in the third column 120 D31 4a Symphony IDE User Manual Public COMPASS A 1 Actions This section describes all of the supported and partially supported actions Where A and B are actions e is an expression P x is a predicate expression with x free c is a channel name cs is a channel set expression ns is a nameset expression Operator Syntax Comments Termination Skip terminate immediately Deadlock Stop only allows time to pass Divergence Diverge runs without ever interacting in any observable event Delay Wait e does nothing for e time units and then terminates Prefixing cle x P x gt A offers the environment a choice of events of the form c e p wherep in set x x T P x Guarded action e amp A if e is true behave like A otherwise behave like STOP Sequential compositio
97. e law are presented in the bottom panel and the law can be applied by double clicking it ry v FE Br Ar v ow Q FY AML EC Refinement E cML Explorer X 6 test cml X 6 C RefinementLaws X als 7 channels c nat Law Name v test process test begin Implicit to Explicit Recursion gt A test cml state Dummy Law v nat 1 actions A true amp c v gt A B val x nat Stop A B v end E CMLRPOList X m Ne Re Type Source E Refinement Law Details X fm N A N mu X A X EC CML RPO Details X m Figure 84 Selection of refinement law The refined CML specification is shown in the CML Editor and further refinement laws can be applied Figure 85 In this example a refinement law is applied to make the implicit recursion in A explicit using the mu operator n HGG A A m O7 Q7 we D Ov Q E BML EC Refinement E cML Explorer X G test cml X A C Refinement Laws X jm als channels c nat Law Name Y test process test begin gt E test cml ce fai ai actions A mu XX true amp c v gt XX B val x nat Stop A B v end E CMLRPOList X m Ne Re Type Source E Refinement Law Details X m N A N mu X A X E CML RPO Details X gt jm writable Insert 13 4 Figure 85 Application of refinement law As previously mentioned the details of how the tool can be extended with new refine ment laws as well as the description of other
98. e model state remained stable In hardware in the loop tests it may be desirable to change only a bounded number of inputs at a time since the SUT reaction may become non deterministic in presence of too many nearly simultaneous input changes Therefore parameter CI is set to 1 by default meaning that after a delay at most one input to the SUT is allowed to be changed For software testing it is often allowed and even necessary to change several input variables to the SUT at the same time If this is the case CI should be set to a bound which is sufficiently high DI Minimal duration between two input changes In hardware in the loop test ing the interface latency of the SUT has to be taken into account if changes to the SUT occur with too high a frequency the SUT will not be able to process them be cause consecutive changes get lost already on input interface boards or in buffers of the SUT runtime system Therefore the minimal duration between input changes to the SUT should be respected by the testing environment To this end parameter DI du ration between input changes can be set to a natural number indicating the minimal duration between two input changes in the time unit milliseconds LI Upper limit for the duration between two input changes Changes to the SUT should not occur with too high a frequency Thus it can be useful if the tester can limit the maximum duration between two input changes to prevent the solve
99. e rest of this chapter and in the RTT MBT setting Model based testing The behaviour of the system under test SUT is specified by a model elaborated in the same style as a model serving for development purposes Optionally the SUT model can be paired with an environment model restricting the possible interactions of the environment with the SUT Test Model Specifies the expected behaviour of a system under test This is an im portant step in model based testing Note that a test model can be different from a design model It might only describe a part of a system under test that is to be tested and it can describe the system at a different level of abstraction underlying API that is used for these file operations uses java I O functions so that the Eclipse resources are not updated automatically You can use Refresh using native hooks or polling setting from the Workspace section of the General preferences of Eclipse to perform these updates automatically 86 D31 4a Symphony IDE User Manual Public COMPASS Test Case A test case is a set of input values execution preconditions expected re sults and execution postconditions developed for a particular objective or test condi tion such as to exercise a particular program path or to verify compliance with a spe cific requirement For RTT MBT model based testing with RT Tester a test model is used that describes the behaviour of the system that should be tested Test cases can
100. eferences El Model Checkers c terexample The Symphony ID S Eo m Edit Navigate Search Project Theorem Prover Isabelle Run Window Help ri A A Pv Qa Qr 7 7 ey ce Quick Access fy EX cM mc Model Checker E CML Explorer 53 O Symphony X A G Outline 2 m aal Y An outline is not available a aes G al tau tau b3 tau E AVDeviceDiscovery_MC E BEOCoSimulation_MC E BEOStreamingSo_MC E BitRegister_MC E CUSSoS_MC i E DPhilosophers_MC I a E InfComm_Mc amp generated 5 nt cml me CML Model Checke InfComm launch Process Property SAT PRec Deadlock 4 mm b E Model Checker 8 7 O P ErrorLog 2 fi Problems 4 Tasks E Console 5 v Ek aiu oa X Y Workspace Log i No operations to display at this tim YPE filter text Message Plug in Date Concluido Figure 75 Analysis result with infinite communications 66 D31 4a Symphony IDE User Manual Public COMPASS 9 6 Syntax Limitations This section provides tips for users in terms of CML syntax limitations for model checking purposes Most of these limitations are due to the the embedding of CML in FORMULA and performance Some of these limitations can also be avoided by the dependency inclusion performed by the model checker when analysing CML pro cesses That is even a CML project has many files and processes defined the model checker includes only the selected process and all other processes it d
101. el checker Preferences 9 4 Using the CML model checker 9 5 Examples 2664554446 ao GHG bw bs wo eG 9 6 Syntax Limitations 10 The Symphony Fault Tolerance Tool 10 1 Performing Fault Tolerance Verification 10 2 Fault Tolerance Verification Plugin Example 11 The Refinement Tool 10 11 11 13 13 13 14 17 17 18 18 18 20 20 22 23 28 32 33 35 37 4 45 45 47 48 50 58 58 58 59 59 64 67 70 70 74 78 D31 4a Symphony IDE User Manual Public COMPASS 11 1 Using the Maude Tool on n aaa 78 EE E E ee ee 79 E ee ee ee ee eae 79 12 RT Tester Plug In 83 12 1 RTI MBT Preferences 0 0 000 83 pee ene ee een ee eee eee 85 Ce koe eee eee eee hae eee 86 12 4 Creating a Project 2 2 2 2 2 00 eee ee ee eee 88 re ee 90 ee ee ee ee 92 ease nee e bees een eas 93 TETERE TEUER EEEE TEREE 101 a 104 107 ea oe ee ee eae a eX 107 a ee ee ee ee ee ee ee ee 109 13 3 Generating CML and Inspecting the Result 110 14 The Command line Tool 112 14 1 Available Functionality a aoa 112 JR bee eee deeae eee ea ee ae ee 113 soe e ea eee ewe ee eee ee 114 ne Reo ee eee ee ee eee ee eee es 114 Leese nee eee een ee eee ee 116 15 Conclusion 117 120 A l Actions aaaea L 121 ee T 126 B CML Support in the Proof Oblig
102. elism les i in set e execute all actions A i for i in the set e ns i ACY in parallel synchronising on the events in cs Each action A i can only modify the state components in ns i Replicated alphabetised parallelism i in set e execute all processes A i in parallel syn ns i cs i A i chronising on the intersection of all cs i Each process A i can only perform events in cs i and can only modify the state com ponents inns i Table 7 Replicated action constructors 123 D31 4a Symphony IDE User Manual Public COMPASS Operator Syntax Comments Let let p e in a evaluate the action a in the environment where p is associated to e declare the local variable v of type T option ally initialised to e and evaluate action a in this context Assignment vi e assign e to v Multiple assignment atomic vl i assignments are executed atomically with re spect to the state invariant Call 1 obj 0p p execute operation op of an object obj 1 or 2 op p of the current object or process 2 with the 3 A p parameters p 3 execute action A with pa rameters p Assignment call 1 1 execute operation op of an object obj or v ob 0p p 2 execute operation op the current object or process with the parameters p and assign the op p value returned by op to a variable Return return or terminates the evaluation of an operation pos return e sibly yielding a value e
103. emma ForbidStopToDrive mk_DwarfType amp stop 11 Lemma SimpleGoal2 V by 12 forall x nat amp gt 5 gt amp gt 1 true v amp lemma DarkOnlyToStop mk_DwarfType amp stop amp 13 by cml_auto_tac V by 14 Y H lemma DarkOnlyFromStop mk_DwarfType amp stop amp 15 lemma NeverShowAll mk_DwarfType amp stop amp stop amp stop amp stop true v by 16 by cml_auto_tac end 17 18 Lemma MaxOneLampChange mk_DwarfType amp stop amp stop amp stop amp stop true 19 by cml_auto_tac 20 21 Lemma ForbidStopToDrive mk_DwarfType amp stop amp stop amp stop amp stop true Theo X O A22 by cml_auto tac gt a 2 papas ae 24 Lemma DarkOnlyToStop mk_DwarfType amp stop amp stop amp stop amp stop true amp 25 by cml_auto_tac type filter text a Rn eT ATT It VA Symbols X Observable Event Hist 2 emma DarkOnlyFromStop mk_DwarfType op amp stop amp stop amp stop true o rial 28 by cml_auto_tac _ Ctype filter text 29 Y Arrow 30 leftarrow 31end longleftarrow Prover Output 23 E Problems EJ Console 9 Error Log Sg Progress B B im i ana O lt Leftarrow o lt Longleftarrow Rightarrow g Longrightarrow leftrightarrow 0 longleftrightarrow T lt lt Leftrightarrow lt gt Longleftrightarrow 0 mansto Writable Insert 28 20 Figure 60 Discharge
104. en as input to 62 D31 4a Symphony IDE User Manual Public COMPASS Could not analyse the specification Internal error when accessing some null object during FORMULA script generation Figure 69 Conversion error Could not analyse the specification Internal error in FORMULA Figure 70 Internal error in FORMULA the FORMULA tool to be analysed The graph construction is performed internally producing a file with extension gv and using the GraphViz software actually the dot exe command to compile the gv file to a graph file with extension svg Then Symphony automatically shows the graph file in its internal browser see Fig ure 71 All these steps are performed automatically r a a Model Checker Model checker counterexample The Symphony IDE s eore To File Edit Navigate Search Project Theorem Prover Isabelle Run Window Help ri A A Pv amp rQr v Qr r Quick Access E A cmt 5 CML Explorer 3 inf cml Symphony amp DE Outline BB 7 E AVDeviceDiscovery MC E BEOCoSimulation_MC E BEOStreamingSo_MC E BitRegister MC E CUSSoS_MC E DPhilosophers_MC 4 E InfComm_MC amp generated me CML Model Checke 5 E inf cmi B InfComm launch An outline is not available Process Property SAT 1 Deadlock i E Model Checker 23 Error Log X E Problems 4 Tasks E
105. enerate an external choice of as many actions as the size of values in the set alive Names Names of variables local state communication must be different because FOR MULA does not allow definition of variables with scope directly Some of these constraints are already checked by the parser for instance processes using the same names are not allowed Concerning state variables it is not possible only for model checking purposes that distinct processes declare state variables with the same name or it is not possible that two communication or parameter variables in any process or action have the same name This was a design decision when implementing the embedding to improve the performance Manipulation of scope in FORMULA would certainly affect the one to one description from the operational semantics as well as performance It is worth mentioning that if variables with same names are used in different and independent processed do not represent a problem because only the analysed process will be considered Dealing with infinite types The manipulation of infinite types are implemented in the model checker allows only their use in communication variables Furthermore the use of an infinite type is al lowed only in input events channe1l var with one parameter The number of in stances of infinite types to be manipulated by FORMULA must be specified in the model checker preferences see Section for details We recomme
106. ent Options X E begin operations dummyOp gt amkan dummyOp v v 1 post ENG state v int 0 init gt dummyOp a gt Skip end process B begin init gt b gt Skip end process test A init B E console X 4 Tasks Error Log E B aBn 0 lt terminated gt Debug Console Quick Launch CML Model CML Debugger Waiting for environment on b tau ACallStm gt ACallStm test cs WAITING FOR_ENVIRONMENT RUNNING FAILED Error 4072 Postcondition failure post _dummyOp in home akm phd runtime COMPASS ny test test_model cml at line 8 5 at in ani i aa ak writable Insert 12 21 Figure 23 The interpreter has stopped because a post condition has been violated 27 D31 4a Symphony IDE User Manual Public COMPASS 6 3 5 Interpreting implicit model elements There are cases where it is useful to be able to simulate models that have a degree of looseness to them such as functions or operations that are intended to select and return an arbitrary element from a set To support this the functionality of the simulator was extended to use the ProB constraint solver LBO8 When the Overture VDM simulator encounters an implicit function or operation it now translates the pre and post conditions into a form suitable for the ProB constraint solver and then uses the result of running ProB on it For example consider the following example of a select function select ns set of
107. eorem proving support plug in for the Symphony IDE The steps enable the user to prove theorems for a specific CML model 1 If Isabelle is not already running from the menu bar select Theorem Prover Launch Theorem Prover This will run the Isabelle configuration defined in Section 8 2 If there is already an instance of Isabelle running an error message will appear as in Figure 48 This can be safely dismissed 6600 Problem Occurred K Launching Isabelle CML has encountered a problem Only a single prover can be running at any time stop the running prover before launching a new one Details gt gt om 4 Figure 48 Error messages from Isabelle in Symphony 2 When proving in the Symphony IDE the Isabelle perspective is used To open the perspective manually select the icon labelled a in Figure 49 and then select Isabelle and then ok If the perspective has been used previously then select the Isabelle perspective using the button labelled b in Figure 49 3 Once open the Isabelle perspective will look like Figure 50 There are various panes in the perspective as follows Project Explorer Similar to the CML perspective this pane shows the projects created in the user s workspace and their contents Please note that a GitHub account is necessary for filing bug reports 48 D31 4a Symphony IDE User Manual Public COMPASS E 4 NAQA HOQ gt 0 B Dwarf cml 2 es 7 1 kypes 2 LamnT
108. epends on Parameters in processes and actions Processes and actions must have only one parameter to be analysed by the model checker However extra parameters can be emulated by using local variables dc1l var type or as state variables so that their values can be changed and used along the specification Furthermore parameters must have primitive type such as int nat or strings Replicated constructs Replicated constructs can be accepted by the model checker as long as the values used in the indexes can be determined before the translation to FORMULA This means that sets whose values are dynamically determined when executing the CML model cannot be used as indexes of replicated constructs To overcome this limitation one can declare the sets of all possible indexes as values or types in the CML model For example the code process Spec begin state this state variable is modified by some actions alive set of NODE_ID 0 1 2 actions Alive Ji alive is not allowed as the values in the set alive are determined dynamically On the other hand if it is possible to use fixed values the same piece of code can be written as follow values alive set of NODE_ID 0 1 2 process Spec begin actions Alive Ji alive 12The set alive could also be declared as a type in the model 67 D31 4a Symphony IDE User Manual Public COMPASS This causes the conversion to FORMULA to g
109. every involved construct will be marked gray in the editor window Editor This shows the CML model source code with a twist As seen in Figure 19 parts of the model is marked with a gray background This marking is determined by the selected event in the CML Event Options view To understand how the views work together a two step animation is shown in Figure 19 and In tock has happened once and a tock event is currently selected Since process A and B both offer tock they are both marked with gray in the Editor view In Figure 20 the init event has been double clicked Thus A and B has synchronized on init and they both wait for the next event to occur 6 3 2 Simulation Simulating without user interaction is achieved by choosing the Simulate option in the launch configuration This mode of operation will interpret the model by taking random decisions when faced with a choice of events However the same choices will always be taken if the model is interpreted multiple times this can be controlled by a seed value In Figure 21 a simulate interpretation has completed 24 D31 4a Symphony IDE User Manual Public COMPASS Debug test test_model cml Symphony IDE File Edit Navigate Search Project Run Window Help ri v o gt as Z weer OvrQavraAawvr ey Q E AcM Debug Debug X x A W Variables Breakpoints Observable Event History X m v BY Quick Launch CML Model tock n CML Debug Target of Action test cs
110. ferences together with the respective HTTP server port If the HTTP Server requires authentication the credentials must be added in the Username and Password fields of the Server section see Figure 87 how this is done 0 O80 Preferences type filter text Server x v gt General gt Ant Server settings C C note Username and Password are used for HTTP s authentication if the server name is an URL gt Help gt Install Update Server algieba informatik uni bremen de gt Java Port 9116 gt JavaScript i Library Hover Name Uwe Schulze gt Maven gt Plug in Development User ID uwe verified de WRT Tester Project Server gt Run Debug Username Password Cancel t ok Figure 87 The RT T MBT Server Settings Page The RI Tester core components the Test Management System TMS and the RTT MBT test generator are executed on the server The RTT MBT project files are created and maintained on the client side For every RTT MBT task that is to be executed the client synchronises all required files with the server workspace It is recommended that you use your real name as the user name and your email address as your user identification The Server connection can be tested using the main page of the RT Tester section in the Eclipse preferences The Project page shown in Figure 88 of the RT Tester preferences contains global set tings that are used as default values for all RTT MBT projects as long as the
111. g all test cases covered during the test execution together with the PASS FAIL in formation obtained for this test case during replay These test case verdicts are added to the test documentation in the next step Generate Documentation If replay is not per formed test cases that are assigned to internal test model states might not get a verdict from the test execution and will occur as inconclusive in the test documentation 12 9 6 Generate Documentation After a test run automatic generation of the test result should be triggered To this end select the procedure in the test execution context and issue the Document Test command in the context menu in the toolbar or in the RTT MBT menu This has the following effects e A test procedure description document in PDF format is created in the testdata directory of the test procedure e A test results description document in PDF format is created in the same direc tory 106 D31 4a Symphony IDE User Manual Public COMPASS 13 SysML to CML Translation This section describes the use of the SysML to CML translation plug in S2C lite that is available in the Symphony IDE This plug in takes an XML representation of the SysML model in the form of an XMI file exported from Atego s Artisan Studio and produces a number of CML files one for each block and state machine It is worth mentioning that this tool is different from the implementation in Artisan Studio of the semantics in D22
112. generation fails users may attempt manual proofs To attempt a manual proof right click the model in the project explorer and select CML THY Manual Proof Obligation Discharge This is shown in Figure 56 This process checks that the CML model is supported by the theorem prover If there are any parts of unsupported syntax in the CML model an error message appears which informs the user A list of unsupported syntax is reported in the warning pane of the Symphony IDE The individual POs are also checked to ensure they use syntax sup ported by the theorem prover If the model is supported the theorem prover plug in creates two theory files with the thy file extension a model specific read only file for the CML model lt modelname gt thy and a user editable file lt modelname gt _PO thy These files along with a read only version of the CML model are added to a timestamped folder in the PROJECT generated POG folder of the CML project see Figure 57 Note this file is specific to the current state of the model Any changes made to the CML model will not be reflected in the thy file and thus the process must be restarted The generated model thy file uses a combination of regular Isabelle syntax and the Isabelle syntax defined for CML described in more detail in FP 13 In the lt modelname gt _PO thy file each supported PO is represented as an Isabelle lemma with the proof goal being the PO expression Each lemma init
113. guration csv to open the configuration editor e Mark the entry in column DEACT Deactivate model component during the generation process for every model component that should not be considered during the generation e Mark at least one state machine transition of the SUT in column TC Transition Coverage This is a directive to the generator that the model coverage test case visit this transition during test execution will be covered by the test procedure to be created The other columns of the configuration file are explained in more detail in Section 12 7 1 For the initial generation there is nothing more to do 12 5 2 Check and Edit the Signal Map The signal map specifies the input output direction of each interface variable as well as the data ranges admissible for these signals During project initialisation an initial version of the signal map is created based on the type information of the interface signals specified in the model The resulting signal map is placed into the test procedure generation context as file TestGeneration _Pl conf signalmap csv Since the generator can only guess the appropriate signal ranges and since it may be useful to change the ranges for specific test purposes it is advisable to open this file by double clicking it in the project browser Then adapt the pre defined data ranges where appropriate In the turn indication sample project described in Ver13b for example the float
114. he type Device_Record Event the invariant of such a type is removed the process can be analysed and does not presents a deadlock Furthermore as these models use timed constructs the model checker will show tock events in the graph representa tion Model from Insiel There is one example from Insiel called CUSSOS It contains constructs involving par allelism and interleaving of smaller components processes The synchronisation be tween processes is defined by general parallelism where the synchronisation set is de fined by specific chansets An Example with Infinite Communications The InfComm_MC project is a simple example containing a process that reads data values in a channel and uses them to update the state variable and to deadlock as long as a predicate involving their values is satisfied Clearly this example deals with features not handled by usual tools like FDR and PAT a corresponding CSP specification 1s almost the same as the CML file input events involving values form an infinite domain and predicates involving such values The values are put in two variables x and y such that there is a deadlock when their values satisfy the expressionn y and y gt 2 where n 2x Furthermore note that there must be at least two different values manipulated by FORMULA to validate the deadlock these values are shown in the graph and can be used in the animator to see the deadlock This property must be set in the Model checker Pr
115. hen configuring the test procedure generation context Therefore RT T MBT produces additional informa tion during the generation process that will be useful for checking whether your are test ing the right thing This information is described in the following paragraphs anoe Outline 24 gt go Y Model Signals SystemUnderTest F FLASH_CTRL FLASH_CTRL EMER_ON EMER_OFF Initial tilOld gt OUTPUT_CTRL left right b TestEnvironment Emerswitch LampsLeft LampsRight TurnindLyr voltage wi i Z Z Z Figure 98 Signal viewer outline showing all signals selectable for display Signal flow over time While generating a test procedure RTT MBT records all changes of interface and internal model variables as well as simple state changes within state machines as they should arise during test procedure execution against the model These variable changes over time can be visualised using the signal viewer 102 D31 4a Symphony IDE User Manual Public COMPASS which is built into the graphical user interface RTT GUI After having generated a test procedure the signal viewer can be opened by double clicking on the generated file signals json in the model directory of the respective test procedure generation con text To select the signals variables and simple states to be displayed an outline view is applied In Figure 98 some of the signals selectable for the turn indication sample project are shown apart
116. her system and as a result simulate the whole System of Systems SoS in co operation with that system Co simulation is accomplished through the use of the co simulation configuration avail able under debug configurations in the Symphony IDE A co simulation is a distributed simulation that consists of at least one coordinator and some non zero number of ex ternal systems A coordinator is the simulator that simulates the toplevel CML model of the SoS This means that it conducts its simulation at the process level and that the 28 D31 4a Symphony IDE User Manual Public COMPASS simulation starts with the top or entry process which is the process at the highest level that composes the SoS from its constituent systems The co simulation launch configuration shown in Figure 24 and Figure 25 allow the user to select the project co simulation URL and one of two modes Coordinator To run the simulator as a coordinator the user selects the Coordinator option and selects the processes that will be handled by an external system It is important to note that the process named in the Top Process section must be the top process at the SoS level An example of such a configuration is given in Figure 24 External System To run the simulator as one of the constituent systems of the SoS the user selects the External System option and in this case chooses the specific process that this simulator represents for the Top Process section Se
117. i in set e Not implemented ns i A i Replicated generalised parallelism lesi i in set e execute all actions A i for i in the set e in parallel ns i A i synchronising on the events in cs Each action A i can only modify the state components in ns i Replicated alphabetised parallelism i in set Not implemented ns i cs i A i Replicated synchronous parallelism i in set e Not implemented ns i A 1 Table 23 Replicated action constructors 142 D31 4a Symphony IDE User Manual Public COMPASS Operator Syntax Comments Let let p e ina Not implemented declare the local variable v of type T optionally ini tialised to e and evaluate action a in this context Assignment vi e assign e to v Multiple assignment atomic vl el Not implemented en execute operation op of the current or process 1 with the parameters p 2 execute action A with parame ters p Not implemented Return return eorreturn Not implemented Specification Not implemented frame we Vile T1 td Wee Iz pre Pl vl v2 POs P2 vl vl v2 v2 New v new C Not implemented Table 24 CML statements 143 D31 4a Symphony IDE User Manual Public COMPASS Operator Syntax Comments Nondeterministic if statement Not implemented if el gt al e2 gt a2 If statement The condition el is used to enable the statement al or if el then al an The optional elseif are not allowe
118. ially uses the by cml_auto_tac proof tactic to attempt to discharge the PO automatically If this is not successful indicated by red error symbols next to a lemma the user should either use the keyword oops to skip that PO or attempt to prove the lemma manually In the next section we introduce the steps for a more manual approach to theorem proving in the Symphony IDE including more details on the different thy files generated by the Symphony theorem prover 8 4 3 Discharging Model Specific Validation Conjectures To illustrate the process of proving model specific conjectures we use an example introduced in Part B of deliverable D33 2 FP13 the Dwarf signal controller 52 D31 4a Symphony IDE User Manual Public COMPASS Preferences General Ant Communications Help Full Predicate with Context Proof Obligation Detail Level Definedness Predicate Only Install Update Isabelle Java Maude Setup Model Checker Setup Plug in Development Rl Tester Run Debug Symphony Simulator Team Theorem Prover Setup 4 Restore Defaults Apply D Cancel aia Figure 53 POG preference page EJ CML Explorer X O E Dwarf cmi X aKa Y types 2 Dwarf ae LampId lt Li gt lt L2 gt lt L3 gt Sianal set of LampId New p Signal Dwarf l O s in set dark stop warning drive gt genera pen E READM Open With gt lastproperstate
119. ion the execution context Test Execution is created and the first test procedure is stored there in directory _P1 It is explained in Sec tion 12 9 how the generated procedures can be compiled and executed against a SUT or a simulation As a side effect of this initial generation the model related test cases have been identified 12 6 Creating Additional Test Procedures Additional test procedures can be generated by copying the initial or any other suit able test procedure generation context P1 in the generation context A test procedure generation context can be copied and pasted into the generation context like any other folder in the project Rename the new test procedure generation context and e inspect the signal map conf signalmap csv whether the input signals need adaptations for the new test procedure to be generated see Section 12 7 2 e adapt the configuration conf configuration csv as far as needed see Section and or e allocate new test cases to be covered by the new procedure that will be generated form this context e remove previously generated files in the subdirectories log model and testdata 92 D31 4a Symphony IDE User Manual Public COMPASS 12 7 Test Generation Configuration Model based test procedure generation with RTT MBT can be influenced in many ways allowing a user to specify different test goals to be reached and different test procedure and solver behaviour This adds complexity to the c
120. is unable to detect a failure will occur process LFTSimple begin actions NOMINAL sendRescuelInfoTokru gt processMessage gt RECEIVE FAULT RECEIVE receiveMessage gt serviceRescue gt NOMINAL FAULT unwanted lt Faultl gt gt RECOVERY unwanted lt Errorl gt gt unwanted lt Failurel gt gt Skip RECOVERY StartRecoveryl gt logFaultl gt resendRescueInfoToEru gt processMessage gt receiveMessage gt endRecoveryl gt serviceRescue gt NOMINAL NOMINAL end Listing 4 Limited Fault Tolerance example When the process chooses the FAULT action that communicates the events lt Faultl gt lt Errorl gt and lt Failurel gt the RECOVERY action can be chosen If it does then it handles lt Fault1 gt communicating both processMessage and receiveMessage Otherwise the system will eventually communicate the event unwanted lt Failurel1 gt so the process is not fault tolerant in general When a limiting condition is imposed by putting LFTSimple in parallel with the Limit process shown in Listing 2 then the verification passeq The plugin shows a green marker as depicted in Figure 77A 10 2 3 Example Listing 5 shows a system that is not fault tolerant even when considering the limiting conditions Note that the recovery mechanism does not provide the same events that the nominal behaviour provides When the RECOVERY action is chosen it will not communicate processMessage
121. ischarge Manual Proof Session Figure 58 Initiate production of a theory file for a CML model In the original CML model Dwarf cm1 and the generated thy file Dwarf thy are shown in Symphony The generated thy file uses a combination of regular Isabelle syntax which is described in various Isabelle manuals and tutorials and the Isabelle syntax defined for CML This Isabelle CML syntax is described in detail in FP13 In the corresponding generated timestamped Isabelle directory a user editable thy file is produced in this example that file is named Dwarf_User thy This file imports the utp_cm1 theory and the generated Dwarf model theory We use the Is abelle perspective to start stating and proving theorems and lemmas and can begin to prove some of those theorems introduced in FP13 These theorems named nsa molc and fstd are added to the user editable theory file Dwarf_User thy 55 D31 4a Symphony IDE User Manual Public COMPASS eoo CML Dwarf Dwarf cml The Symphony IDE Users nrjp6 Dropbox University Eclipse Workspaces CMLWorkspace Ma re 2 HAN Oa r Q Qa Ae 2 Xo Oy s Q Quick Access E E cm dh Isabelle BG Poc ao E Dwarf cmi 2 S Dwarf_User thy m lm B Dwarf thy 8 Sih 1 types 1l theory Dwarf 2 LampId lt L1 gt lt L2 gt lt L3 gt 2 imports utp cml 3 Signal set of LampId 3 begin cmt 4 ProperState Signal 4 P 5 inv ps ps in set dark stop warning drive 5text
122. ising in the in tersection of X and Y A in only allowed to commu nicate on X and B is only allowed to communicate on Y Neither A nor B change the state Alphabetised parallelism with state as with the without state version but modifications from A to the state components in ns1 and modifi cations from B to the state components in ns2 are preserved at the completion of the operator Generalised parallelism without state A cs B execute A and B in parallel synchronising on the events in cs Neither A nor B change the state Generalised parallelism with state execute A and B in parallel synchronising on the events in cs A can modify the state components in ns1 and B can modify the state components in ns2 Table 6 Parallel action constructors 122 D31 4a Symphony IDE User Manual Public COMPASS Operator Syntax Comments Replicated sequential composition i in seq e A i e must be a sequence for each i in the se quence A i is executed in order Replicated external choice i in set e A i offer the environment the choice of all actions A i such that i is in the set e Replicated internal choice 3 in set e A i nondeterministically behave as A i for any i in the set e Replicated interleaving 2 in set e execute all actions A i in parallel without ns i A i synchronising on any events Each action A i can only modify the state components inns i Replicated generalised parall
123. istory The plugin keeps track of the development and evolution of the SoS model by storing the results of the different modelling sessions performed by the collaboration group Thereby the modelling efforts can be resumed and design decisions can be renegotiated and developed as the modelled SoS evolves 7 4 Distributed Simulation The Collaborative Modelling plugin also makes use of the co simulation capabilities described in The connectivity that is already established between the col laborators in the Collaboration Group can be used to configure and perform distributed simulation of the collaboratively developed CML models While the simulation itself makes use of the co simulation capabilities described in Section 6 4 the configuration of the simulation is performed without having to manually create co simulation launch configurations on each of the involved collaborators One collaborator will act as the coordinator of the distributed simulation while other collaborators will act as clients The collaborator that initiates the distributed simulator will act as the coordinator and gets to determine which process should be the coor dinating process as well as selecting which processes should be simulated by which collaborator The distributed simulation is initiated by right clicking on the Collaboration Project node and clicking Initiate Distributed Simulation as shown in Figure 42 Please note that if the Collaborative Modelling pl
124. ists of several panels known as views such as the CML Explorer view at the top left of A collection of panels is called a perspective for example Figure 3 shows the standard CML perspective used in the Symphony IDE This consists of a set of views for managing CML projects and viewing and editing files in a project Different perspectives are available in the Symphony IDE as will be described later but for the moment think of a perspective as a useful composition of views for conducting a particular task The Symphony Explorer view lets you create select and delete Symphony projects and navigate between the files in these projects as well as adding new files to existing projects The Outline view on the right hand side of Figure 3 presents an outline of the file selected in the editor This view displays any declared CML definitions such as their state components values types functions operations and processes The type of the definitions are also shown in the Outline view The Outline view is at the moment only available for the CML models of the system In the case another type of file is selected the message An outline is not available will be displayed The outline will have an appropriate structure based on the type of CML construct found in the source file that is displayed in the visible CML editor In a CML the left Figure 4 class is outlined on the right reflecting the structure of a class On depicts a CML process and li
125. itions have been marked as robustness transitions see Section 12 7 1 but also ordinary transitions exist The test generator will fire approximately RP robustness transitions from this state and 100 RP normal behaviour transi tions For achieving an adequate distribution of normal behaviour and robustness transitions in TE simulations it is advisable to configure the test procedure generation context as a combination of constraint solving and random simulation Recall that this is achieved by setting parameters Max Solver Steps and Max Simulation Steps to positive val ues as described in the basic configuration The constraint solver alone no simu lation active always looks for the most direct model trace leading to coverage of a given test goal Therefore it ignores the percentage of normal behaviour or robustness transitions taken so far and always chooses the one which is most suitable for the test objective The other configuration parameters are currently experimental and should only be used with their default values as indicated in Table When the initial test proce dure generation context is created in Test Procedures _P1 see Section 12 4h the advanced conf file associates all parameters with their default values so that it will be unnecessary in most situations to edit this file unless CI and DI should be adapted 12 8 Test Procedure Generation If a test procedure generation context is configured completely
126. l Public COMPASS The test procedure that is visualized in Figure 99 stimulates different turn indication and emergency flashing conditions The stimulations as well as the expected SUT indications are visible 12 9 Test Procedure Execution The generated RT Tester test procedures reside in the test execution contex of the RTT MBT project Recall that a generated test procedure has the same name as the test procedure generation context used to generate this test procedure These RT Tester tasks can be selected through the toolbar the RTT MBT menu or the Test Execution Context section of the context menu for a selected test procedure Note that a test procedure has to be selected in the Project Explorer of the RttPerspective for the RT Tester actions to be enabled OVS kw E A Test result Generate Documentation Run Test Procedure Compile Test Procedure Cleanup Test Procedure Execute Test Procedure Figure 100 The RT Tester commands in the toolbar 12 9 1 Execute Test Procedure A complete test execution consists of the steps e Clean Test Procedure e Compile Test Procedure e Run Test Procedure Replay Test Result Generate Documentation 12 9 2 Clean Test Procedure A test procedure can contain outdated test results from previous test runs or the test pro cedure executable itself is outdated In both cases the Clean Test Procedure command can be used to remove all test data and the
127. l Console RY Workspace Log type filter text I No operations to display at this tim Message Plug in Figure 71 Graph Viewer The initial state of the graph is two circles intermediate states are single circles and the deadlocked state or other special states related to properties verification has a different colour a red tone Each state has a number and information hint about the bindings from variables to values the name of the owner process and the current context process fragment To see the internal information of each state just put the cursor over the state number Similarly transitions are labelled with the corresponding event and also have a hint 63 D31 4a Symphony IDE User Manual Public COMPASS showing the source and the target states This feature is useful to provide information about which rule of the structured operational semantics was applied The internal graph builder of the model checker considers the shortest path that makes the analysed file satisfiable Thus although there might be other counterexamples it shows the shortest one 9 5 Examples The Symphony IDE provides some examples that can be imported This is achieved by a right click on the CML Explorer component and choosing the Import option Then select the option Symphony Symphony Examples see Figure 72 The examples accepted by the model checker contain the suffix MC in their names
128. l Name Declarations channels it declares the channels a and b of a specific type a b type Chanset Declarations chansets it declares a set of channels chanset definition Nameset Declarations namesets Not implemented nameset definition State Declarations state It defines the state structure containing the variable value nat value Invariants implemented as UTP designs Process Declaration process P val x nat parametrised processes fully supported process_body Action Declarations actions Full support including parametrised actions A val i int action Table 18 Declarations 136 D31 4a Symphony IDE User Manual Public COMPASS C 3 C 4 Types all basic types including nat string token etc are supported quote types exist as a single type in Isabelle such that union types over them can be constructed compound types set map seq seq1 and products are supported record types are supported through tagged product types similar to HOL records union types are currently partially supported for types with a common subtype e g nat and real Expressions boolean expressions with three values full support numeric expressions full support token expressions full support set expressions partial support all operators other than set comprehension sequence expressions partial support seg comprehension missing map expressions partial support map comprehension missing range rest
129. l checking plug in described in Section 9 The fault tolerance analysis plugin described in Section 10 uses the model checking plug in to perform its analysis The Refinement Tool is described in which allows CML models to be transformed via refinement laws CML mod els can also be used to drive test generation through the RT Tester plug in as described in Section 12 It is possible to generate CML models from XMI files exported from a subset of SysML as described in Section 137 Many of the basic functions of the Symphony Please note that the translation described here only works for a small subset of the SysML notation but with a simplified semantics A more elaborate translation has been defined in D33 4 and this has been implemented directly from Artisan Studio but since it follows the OMG semantics it produces larger and more complex CML models D31 4a Symphony IDE User Manual Public COMPASS platform are available through a command line tool described in including basic typechecking interactive simulation proof obligation generation and the SysML to CML generation plugin Section 15 provides a few concluding remarks and a perspective on possible future development after the end of the COMPASS project Finally Appendices and D list the supported CML language constructs for the interpreter proof obligation generator theorem prover and model checker respectively D31 4a Symphony IDE User Manual Public COMPASS 2 Obtaini
130. le event before they can occur through the GUI In Figure 19 a small CML model is being animated in the debug perspective The following windows are depicted Observable Event History This window is located in the top right corner and shows the observable events that have been selected so far In Figure 19 only a tock event has occurred so far CML Event Options This shows the possible events that can occur in the current state 23 D31 4a Symphony IDE User Manual Public COMPASS File Edit Navigate Search Project Run Window Help E E cmL Debug A cml ex X 7 OG A test model cml X A outline X i alel process testProcessl begin Skip end a ora process testProcess2 begin Skip end Loe o gt W BitRegister O testProcess1 Skip gt bo cki s Process Selection Procesz2 Skip gt i Dwar gt RingBuffer Select a process v Stest testProcess1 Skip gt E test_model cml testProcess2 Skip Error Log Problems Tasks Console mjo m cot ED No consoles to display at this time Figure 18 Right after Run As CML Model has been clicked the context menu of the test cml file appears Since the file defines more than one process the process selection dialog is shown of the model To make a particular event occur you must double click it Fur thermore to see the origin of a particular offered event you must click it and the location of
131. le must be selected in the XMI Export dialog box and the button Export pressed as shown in Figures and 107 D31 4a Symphony IDE User Manual Public COMPASS Data Type Converter Report Writer Straic Floating License Status Template Editor Add Profile Options Customize Configuration Management Options ocs Object Animator Assembly Importer Component Wizard gt Repository Administrator Storage Mapper Publisher Rose Import SQL Generator Import Figure 102 XMI Exporter menu lon E Figure 104 File selection 108 D31 4a Symphony IDE User Manual Public COMPASS 13 2 Importing the XMI file Once the model has been successfully exported it is necessary to import the XMI file into Symphony For that create a new CML project in Symphony right click on the project and select Import Figure 105 choose File System as the import source Fig ure 106 navigate to the XMI file Figure 107 and click Finish E CML Explorer 53 ja IL New gt Go Into 12 Copy Ctrl C Paste Ctrl V X Delete Delete Move Rename F2 eA Export Refresh F5 e EA Figure 105 Importing a new file into the CML project Select Import resources from the local file system into an existing project Select an import source type filter text 4 amp General Archive File Existing Projects into Workspace
132. machine select the appropriate file in this case State Machine_HybridSUV as shown in Figure 109 110 D31 4a Symphony IDE User Manual Public gt File Edit Navigate Search Project TheoremProver Isabelle Run Window Help n HBG Fas CML Explorer 23 ElectricMotorGenerator cm Environment cml ExternalObject cml FrontWheel cml Fuel cml Fuellnjector cml FuelPump cml E FuelRail cmi E FuelRegulator cml 29 FuelTankAssembly cml aQ By OvrQarxsrt vy alw amp E StateMachine HybridSUV cm 23 COMPASS o a channels releaseBrake stopped shutoff keyOff engageBrake startVehicle accelerate Outline X RAW e Wm Quick Access E AY Oo S releaseBrake A S stopped shutoff S keyOff S engageBrake startVehicle accelerate 4 HybridSUV act_Initial a VIN ID process HybridSUV begin a PayloadCapacity Weight GlobalTime cml state a FuelEconomy Economy global types cml VME O o QuarterMileTime Time HybridSUV cml RayloadCapacity Weight aiaeag a Zero60Time Time InteriorSubsystem cml QuarterMileTime Time a UnitCost Price InternalCombustionEngine oy Zero6e Time Time a CostEffectiveness CostEffec LightingSubsystem cml w UnitCost Price a bk BrakeSubsystem 2 MeasuresOfeffectiveness ct CostEffectiveness CostEffec a p PowerSubsystem PowerControlUnit cml bkz Brakesubsysten a b BodySubs
133. marking this column for any TE entry will have unpredictable effects during test procedure generation In contrast to this SUT components are normally unmarked in the SIM column unless e a simulation of the SUT should be generated in this case all SUT components have to be marked in the SIM column before the simulation generation command is given or asub component of the SUT has not yet been implemented and should therefore be simulated by the testing environment In this situation only the unavailable sub components are marked in the SIM column and during the test procedure generation process simulation components are created for just these SUT parts DEACT allows you to deactivate test model components during the test procedure generation process This option is practical for incomplete models where some parts are still under construction De activating incomplete components will avoid error mes sages referring to missing model elements or erroneous syntax Moreover sometimes several variants of a model component have been created and for every test procedure generation a specific variant should be applied This applies particularly for the test ing environment where several alternative simulations operating on the same interface variables may be developed and each test procedure requires its specific simulation variant or no simulation at all Observe that it is unnecessary to deactivate test model components in order to speed
134. n left and run button right highlighted Debug Configurations x Create manage and run configurations Project not set B Bo Beso Name New_configuration a amp Main Develop Common Project EJ CML Co Simulation Model Bees m roject rowse EY CML Model E daia E BitRegister Top Process B Dwarf Process Search New_configuration z rna Execution Mode E RingBuffer A Animate Simulate Remote Control Filter matched 6 of 16 items Close Figure 15 The launch configuration dialog showing a newly created launch configura tion shows a list of all the available projects and choose one from there The selection of the process name is identical The selected project must exist in the workspace and the process named must exist within it It will not be possible to launch if they do not In the left corner of a small red icon with an X and a message will indicate what is wrong In the figure it indicates that no project has been set so this should be the first thing to do After setting the project name and process name the Apply button must be clicked to save the changes to the launch configuration If the project exists is open and a process 21 D31 4a Symphony IDE User Manual Public COMPASS with the specified name exists in the project then the Run or Debug button will be active and it is possible to launch the simulati
135. n External choice Internal choice A B nondeterministically behave either like A or B Abstraction A es behave as A with the events in cs hidden Channel renaming AII ec lt ne behaves as A with event c renamed to nc Mutual Recursion explicit definition of mutually recursive actions Table 4 Action constructors 121 D31 4a Symphony IDE User Manual Public COMPASS Operator Syntax Comments Interrupt A _ B behave as A until B takes control then behave like B Timed interrupt A _e_ B behave as A for e time units then behave as B Untimed timeout A gt B behave as A but nondeterministically change behaviour to B at any time Timeout A _ e gt B offer A for e time units then offer B Start deadline A startsby e A must execute an observable event within e time units Oth erwise the process is infeasible End deadline A endsby e A must terminate within e time units Otherwise the process is infeasible Table 5 Timed action constructors Operator Syntax Comments Interleaving without state A B execute A and B in parallel without synchronising Neither A nor B change the state Interleaving with state A Asi execute A and B in parallel without synchronising A ns2 B can modify the state components in ns1 and B can modify the state components in ns2 Alphabetised parallelism without state A csl cs2 B execute A and B in parallel synchron
136. n you a ROOTS file already exists This is ok choose to replace the existing file 4 Copy the utp isabelle folder from the extracted folder to the src folder in the Isabelle2013 application folder e g C ProgramFiles Isabelle2013 src As the CML and UTP theories are improved new versions will be made available As new versions are uploaded follow the above steps to obtain and unpack the up dates 46 D31 4a Symphony IDE User Manual Public COMPASS 8 2 Configuration Instructions for Isabelle UTP This section provides the steps required to use Isabelle in the Symphony IDE This setup procedure is only required on the first use of the theorem prover However if a new version of Symphony is installed then the procedure must be repeated Instruc tions for installation with the Symphony IDE are given below 1 a0 a n Preferences Navigate to the contrib z3 3 2 etc folder in the Isabelle application folder Open the settings file and uncomment remove the character the line Z3_NON_COMMERCIAL yes At present the theorem prover plug in for Symphony may only be used for non commercial use Open the Symphony IDE From the menu bar select Theorem Prover Setup Theorem Prover Configura tion A Preferences window as in Figure 46 will appear Restore Defaults Apply Figure 46 Isabelle configuration setup In the first text box labelled a in Figure 46 supply to the lo
137. nat n nat pre card ns gt 0 post n in set ns This function given a set of natural numbers arbitrarily returns one of the numbers in that set Strictly this is not a function but rather a relation but it could be seen as something that will be a function but is has an incomplete specification It can still be useful to simulate this and it is possible to do this in the Symphony IDE It is also possible to implicitly invoke the ProB solver in for all loops that use type bindings such as for all n in set x x nat do c n gt Skip where the statement in this example would synchronise on each natural precisely once in some arbitrary order There are two major limitations with this feature however The first is that union types cannot yet be translated into a form that can be used with the ProB solver and so will not interpret correctly at this point The second is that type invariants are not translated so care must be taken when solving with types that have invariants 6 4 Co simulation It is possible to split the simulation of a model across several instances of the Symphony CML simulator or even in a mix of CML simulators and other external mechanisms We call this co simulation During co simulation a portion of the modelled system is actually being simulated by other tools or systems that are external to the CML simulator This means that a simulator running in one instance of the Symphony IDE may be connected to anot
138. nd to use the the minimum but sufficient number of instances For example consider a process containing the following example channels a nat process P begin state n NATA 0 operations Double nat gt Double k n 2xk actions MAIN a x gt Double x a y gt if n y and y gt 2 then Stop else Skip MAIN end The analysis of the process P can be efficiently analysed considering 2 as the number of instances in the model checker preferences A brief look at the action MAIN shows that the state value changed by the input value red by event a x is compared with 3That is processes that are not reachable from each other 68 D31 4a Symphony IDE User Manual Public COMPASS the second input value red by the event a y which must be greater than 2 With only one instance x and y would be the same and the condition n y andy gt 2 would never be valid disabling therefore the then branch the deadlock Another tip is concerned with the use of many input communications in a same channel in recursive processes This is not recommended because this degrades the performance of SMT solving when choosing them Instead one can use different channels to ob tain input values so the number of instances in the model checker preferences can be smaller For example the process PRec defined in the example Inf Comm md 4 can be efficiently analysed considering 1 as the number of instances However if such a
139. ng the Software This section explains how to obtain the Symphony IDE described in this user man ual The Symphony tool suite is an open source tool developed by the universities and industrial partners involved in the COMPASS EU FP7 project FLW12 The tool is developed on top of the Eclipse platform The source code and pre built releases for the Symphony IDE are hosted on Source Forge net as this has been selected as our primary mechanism for supporting the com munity of users of CML and the developers building tools for the Symphony platform It has facilities for file distribution source code hosting and bug reporting The simplest way to run the Symphony IDE is to download it from the Symhpony download page at http symphonytool org This download is a specially built version of the Eclipse platform that only includes the components that are neccessary to run the Symphony IDE it does not include the Java development tools usually associated with the Eclipse platform Once the tool has been downloaded in order to run it simply unzip the archive into the directory of your choice and run the Symphony executable The tool is self contained so no further installation is necessary The Symphony IDE requires the Java SE Runtime Environment JRE version 7 or later On Windows environments either the 32 bit or 64 bit versions may be used on Mac OS X and Linux the 64 bit version is required Artisan Studio and the RT Tes
140. nising on any events Table 12 Replicated process constructors 127 D31 4a Symphony IDE User Manual Public COMPASS B CML Support in the POG This section gives a brief overview of the CML constructs that are supported by the POG If a construct is supported then any relevant POs will be generated for said construct If a construct is not supported the POG will simply ignore it and generate POs for other constructs In practice this means that the POG will run on any CML model regardless of its contents B 1 Processes No process specific POs are generated However POs are generated for the various constructs inside a process definition B 2 Classes There are no POs specific to classes However POs are generated for the various constructs inside a class definition B 3 Actions Actions are not supported by the POG No POs are generated for actions B 4 Channels and Chansets No POs exist for channels or chansets B 5 Namesets No POs exist for namesets B 6 Operations Operations are fully supported by the POG Obligations will be generated for any op eration that requires them B 7 Types Types are fully supported by the POG Obligations will be generated for any type that requires them 128 D31 4a Symphony IDE User Manual Public COMPASS B 8 Functions Functions are fully supported by the POG Obligations will be generated for any func tion that requires them B 9 Values Values are
141. nto a test environment can be a simple task but can also be very complex depending on the SUT the test integration level It can vary from linking the SUT object code for unit level tests to providing a function stub interface or shared memory communication for software integration tests to implementing hardware inter faces and communication protocols for hardware in the loop tests Independent of the test configuration every RT Tester test procedure has to be com piled into a test procedure executable This task can be started by selecting the test procedure in the Project Explorer in the test procedure execution context and using the Compile Test command in the context menu or in the RTT MBT toolbar 12 9 4 Run Test Procedure After successful compilation a test procedure is executed by giving the Run Test com mand in the context menu or in the RT Tester toolbar The results of the test execution are stored in log files in the testdata sub directory of the test procedure 12 9 5 Replay Test Result After a generated test procedure has been executed and documentation has been gen erated the test execution log has to be replayed against the test model During replay the RTT MBT interpreter processes the test execution log resulting from the test exe cution against the SUT and checks whether the SUT reactions observed conform to the reactions expected according to the model Moreover the test cases covered during the test execution are i
142. ny IDE User Manual Public COMPASS This model contains unsupported CML elements Check the warnings for more information r tell Model Checker Examples action externalchoice nostate cml Symphony IDE ee x ile Edit Navigate Search Project Theorem Prover Isabelle Run Window Help lt a A OQ Ae RER eer v al Quick Access E A cmt mc Model Checker E CML Explorer 22 i cS jm E action externalchoice nostate cm 2 B Outline 33 JF Bwrevw F 4 j Examples amp channels Saco z amp b B gt gt action externalchoice nostate cm asi 4 b ExttChoiceExamplel process ExtChoiceExamplel begin a gt Skip b gt Stop end me CML Model Checker List 52 File Property SAT 4 Error Log fa Problems 2 2 Tasks Console 0 errors 2 warnings 0 others A m Description Resource Path Location Type 4 amp Warnings 2 items amp AChannelType nodes are not supported by the Model Checker action extern Examples line 2 Problem amp AChannelType nodes are not supported by the Model Checker action extern Examples line 2 Problem E Model Checker Progress View 53 m No operations to display at this time A Examples action externalchoice nostate cml Figure 65 Details about the unsupported constructs When invoking the analysis there are several options as result e If FORMULA 1s not installed the Sym
143. o exist The Run mode will interpret the model without ever breaking on any breakpoints The Debug however will stop on any enabled breakpoint in the model When a Debug configuration is launched the perspective changes to the Eclipse Debug 23 D31 4a Symphony IDE User Manual Public COMPASS Debug test test_model cml Symphony IDE File Edit Navigate Search Project Run Window Help ci v B N P 0 Q aggy v Q eS AcM Debug Debug X Y A Variables Breakpoints Observable Event History jm v E lt terminated gt Quick Launch CML Model tock amp lt terminated gt CML Debug Target tock ai lt terminated exit value 0 gt CML Debugger init a b E test_model cml 6 outline O CML Event X OG channels init a b process A begin init gt a gt Skip end process B begin init gt b gt Skip end process test A init B Console X 4 Tasks Error Log x R Sle Brn CG lt terminated gt Quick Launch CML Model CML Debugger WAITING FOR ENVIRONMENT RUNNING observable step by test Observable trace of test tock tock tock tock tock tock init a b Eval Status Skip NA Skip Waiting for environment on tau AGeneralisedParallelismProcess End gt ASkipAction test WAITING FOR ENVIRONMENT RUNNING FINISHED writable Insert 3 42 Figure 21 The model has just been simulated Perspective however R
144. o share Adding a File to the Collaboration Project A file is added to the Collaboration Project by right clicking the cm1 file in the project explorer and selecting either Include file in collaboration or Include file in col laboration with limited visibility as shown in Figure 37 v TaBa Sys X project gt E System cml Refresh Validate Debug As Run As Team Compare With Replace With Synchronize With Collaborative Modelling Include file in collaboration project Error Log Problen Model check p Include file in collaboration project with limited visibility CML POG Configurations 3 Properties w Sa Be vie 8 Mn Figure 37 Adding a file to a collaboration project Adding a file with limited visibility gives each collaborator the option of selecting which collaborators in the Collaboration Group will receive the file This functionality is included for two reasons 1 some collaborators may not be willing to show their in terfaces and model designs to all collaborators but only to select few 2 Given that it is possible for any member of a collaboration group to expand the group by inviting other collaborators visibility gives the individual collaborators the option of selecting if new members can see their shared models A constraint of using the visibility functionality is that once the visibility of a model has been granted to a collaborator it cannot be revoked This is done to avoid collaborators
145. of the Symphony IDE remain wholly usable without the plug in functionality The Symphony IDE is still not an industrial strength product but the focus of the third and last year of the COMPASS project has been dedicated to providing both engineering improvements of the features It is worthwhile noting that all the features of the Symphony IDE tool are properly integrated and represent a clear progress beyond state of the art of the baseline technology It is now possible to analyse the same CML models both from simulation test automation model checking and theorem proving perspectives Many external tools have been integrated and the installation of these has been made as easy as possible for users However because of licensing concerns it is not possible to make the installation of the external tools fully automated 117 D31 4a Symphony IDE User Manual Public COMPASS References APR 13 BGW 12 BPS12 Col14 FLW 12 FM 14 FP13 LB08 LMN 14 ML14 PVLZ11 Ros10 Ver13a Ver13b Z H Andrews R Payne A Romanovsky A L R Didier and A Mota Model based development of fault tolerant systems of systems In 7th International Systems Conference IEEE SysCon IEEE April 2013 Jeremy Bryans Andy Galloway and Jim Woodcock CML definition 1 Technical report COMPASS Deliverable D23 2 September 2012 Jorg Brauer Jan Peleska and Uwe Schulze Efficient and trustworthy tool qu
146. of the plugin is documented in EM14 The simulator plugin is capable of simulating CML models within the Symphony IDE with no need for external components but it is also capable of co simulating a model that does have external components This is done via a set of libraries that are embed ded into the external component and which allow for communication with the simula tor plugin Section 2 describes how to obtain the software and install it on your own computer explains the different views in the Symphony Eclipse perspective This is followed by Section 4 which explains how to manage different projects in the Sym phony IDE Section 5 describes what output the CML typechecker will produce and where it may be found in the Symphony IDE For the situation where a user wishes to simulate a CML model Section 6 describes the interface to the CML simulator as included in the Symphony IDE An alternative way of simulating a complete SoS with some processes external to the Symphony CML simulator is described in Section 6 4 This external simulation is extended to allow the whole SoS model to be split so that no single constituent owner has the whole model while still allowing simulation of the complete SoS as described in Section 7 describes how to use the proof obligation generation and theorem prover plug ins that can be used together to prove properties about a CML model CML mod els may also be model checked through use of the mode
147. ol In addition to this possibility RTT Plugin provides the possibility to adjust these settings in the RT Tester section of the project properties Because these settings are specific for each test procedure generation context they are only part of the RT Tester properties page if a test procedure generation context direc tory is selected Figure 97 shows the properties page for a test procedure generation context Generation Steps Configuration File The configuration file TestProcedures lt Generation Context gt conf max_steps txt contains the settings for MAX SOLVER STEPS The maximal number of model execution steps from the current model state that the constraint solver will perform to look for a solution of the test objective to be fulfilled A value between 20 and 100 is suitable for most projects Default value is 100 MAX SIMULATION STEPS The maximal number of simulation steps to be per formed by the generator without covering any new model transitions if this number is greater than 0 the generator will try to find test data for a test objective also by means of random walks through the model if the constraint solver could not solve the goal within the given number of steps from the current state A random walk is continued as long as new portions of the model are covered by this walk If a simulation step fails to cover anew model element the initial value of MAX SIMULATION STEPS is 98 D31 4a Symphony IDE User Manual Publi
148. ol at this point http isabelle in tum de documentation html 45 D31 4a Symphony IDE User Manual Public COMPASS Linux Instructions for installation of Isabelle for Linux are as follows 1 Download Isabelle version Isabelle 2013 2 for Linux distributed as a tar bun dled archive 2 Unpack the archive into the suggested target directory 3 NOTE Do not launch the tool at this point 8 1 2 UTP CML Theories To prove theorems and lemmas for CML models Isabelle must have access to the UTP and CML Theories Instructions for obtaining these theories are given below for different platforms Linux Mac OS X 1 Download the latest version of the utp isabelle x archive from https sf net projects compassresearch files HOL UTP CML Linux Mac can choose either zip or tar bz2 2 Extract the downloaded theory package and save the utp isabelle directory to your machine e g home me Isabelle utp isabelle 0 x As the CML and UTP theories are improved new versions will be made available As new versions are uploaded follow the above steps to obtain and unpack the up dates Windows 1 Download the latest version of the utp isabelle x windows zip archive from https sf net projects compassresearch files HOL UTP CML 2 Extract the downloaded theory package 3 Copy the ROOTS file from the extracted folder to the Tsabe1l1e2013 applica tion folder e g C ProgramFiles Isabelle2013 2 Windows will war
149. olumns than are displayed in this figure Here only the columns that are relevant for this manual are displayed 96 D31 4a Symphony IDE User Manual Public COMPASS Abstract Signal Lower Bound Upper Bound SUT writes to TE TE writes to SUT Concrete Signal Admissible Error Latency EmerSwitch 0 1 oO 1 EmerSwitch 0 100 LampsLeft g l l 0 LampsLeft o 100 LampsRight i l l i LampsRight 0 100 TurnindLyr 0 2 0 1 TurnindLyr 0 100 voltage 0 0 16 0 1 voltage 0 100 Figure 96 Signal map example from the turn indication sample project Abstract Signal specifies each observable variable of the SUT with its name as de clared in the test model Model variables not occurring in the signal map are auto matically unobservable that is internal variables of the model without any observable counter part at the SUT interface Lower Bound and Upper Bound specify the lower and upper bounds respectively of input variables to the SUT as they should be observed in the test procedure generation configured in the current context If no TE simulations have been defined for an input interface variable only values within the specified range will be generated If however specific input values are generated by a TE simulation this overrides the lower and upper bound specification in the signal map For SUT outputs the specification of lower and upper bounds only has informative value it does not affect the test procedure generation process SUT writes to T
150. on Figure 40 Received Configuration When activating a Configuration the files it contains will be introduced in the workspace If a file does not exist in the workspace it will be created If the files already exist a dialog will appear that lists the files that will be overwritten and prompt the user to ap prove that new versions of these files will be created Please be aware that overwritten files in the workspace cannot be undone by the Collaborative Modelling plugin As the plugin is not a versioning system the user should use other technologies for ensuring versioning of the files in the workspace Approving Rejecting and Evolving Model When a new Configuration is received its contained model data is to be considered as a proposal as to how a particular part of the SoS could be designed The collaborators that receive the Configuration have the option of either Approving Reject or to evolve the model further Approval indicates that the collaborator accepts the entire proposed model Reject indicates that the collaborator will not use any parts of the proposal and it is discarded When a collaborator approves or rejects a Configuration the other collaborators in the collaboration group will be notified of the decision The status of a Configuration can be seen under the Sent To node of the specific Configuration An approval by a collaborator is indicated by green while a rejection is indicated with red as illustrated in
151. on as shown in Figure 16 Furthermore the decision of whether to animate simulate or remote control the model is decided by the radio buttons in the Execution Mode groupbox in the buttom the default setting is to animate Debug Configurations Create manage and run configurations Debugs a CML Model O GB Xx y Name New_configuration a Main Develop Common Project EJ CML Co Simulation Model Project Dwarf Browse E CML Model E BitRegister Top Process E Dwarf Process Dwarf Search Execution Mode E RingBuffer B Animate Simulate Remote Control i i Apply Revert Filter matched 6 of 16 items D Close Debug Figure 16 The configuration dialog after a project and process have been selected This launch configuration will now appear in the drop down menu as described at the beginning of this section The actual interpretation will be described in 6 2 Launch Via Shortcut Another way to launch a simulation is through a shortcut in the Symphony explorer view in the CML perspective To access this right click on a cml file to make the context menu appear From here either choose Debug As CML Model or Run As gt CML Model as depicted in Figure 17 After that two things can happen if the CML source file only contains one process then this process will be launched If however more than one process is defined then a process selection dialog appears with a list of possible
152. on e in the sequence s execute action a for each expression e in the set S execute action a execute action a for each integer i in the range 1 e2el1 e2 such that i el n e3 where n is a natural num ber execute action a while the boolean expression e evaluates to true Table 9 Control statements 125 D31 4a Symphony IDE User Manual Public COMPASS A 2 Processes This section describes all the supported and partially supported processes A and B are both processes e is an expression and cs is a channel expression Operator Syntax Comments A composition Esc choice mera choice B nondeterministically behave either like A or B Generalised parallelism A cs B execute A and B in parallel synchronising on the events in cs Alphabetised parallelism A cs1 cs2 B execute A and B in parallel synchronising in the inter section of X and Y A is only allowed to communicate on X and B is only allowed to communicate on Y Interleaving B execute A and B in parallel without synchronising Abstraction Hiding A es behave as A with the events in cs hidden Process instantiation v T A e or behaves as A where the formal parameters v are in A e stantiated to e Channel renaming A c lt ne 1 behaves as A with event c renamed to nc Table 10 Process constructors 126 D31 4a Symphony IDE User Manual Public COMPASS Operator Syntax Comments Interrupt
153. onfiguration of the test procedure generation context but provides flexibility in test integration and purpose of the generated test procedure This section describes the different configuration files that are taken into account during the test generation and their purpose 12 7 1 Detailed Configuration of Test Procedure Generation Contexts The detailed configuration editor for transition coverage goals is opened by double clicking the TestProcedures lt Test Proc Gen Context gt conf configuration csv file in the project exploret This displays the detailed configuration editor as shown in Figure 95 for the turn indication sample project The columns of this pane have the following meaning Component allows you to browse through the test model components in top down fashion when opening the pane for the first time the complete component structure is unfolded below the top level components for SUT and TE Test Procedure Advanced Configuration Test Procedure Signal Ranges AX Test Procedure Advanced Configuration X BLS Component CT Allocation TC SC SIM DEACT ROB V SystemUnderTest CP Y SystemUnderTest FLASH_CTRL CP Initial true gt EMER_OFF SC EMER_OFF EmerSwitch gt EMER_ON sE A EMER_ON REQ 008 EmerSwitch gt EMER_OFF SC Initial true gt EMER_ACTIVE SC EMER_ACTIVE TurnIndLvr 0 amp amp tilOld TurnIndLvr
154. ons If automatic discharge 51 D31 4a Symphony IDE User Manual Public COMPASS _ POG BitRegister BitRegisterProc cml The Symphony IDE File Edit Navigate Search Project Theorem Prover Isabelle Run Window Help ry At AR Qarvravwey ony Q E HB 16 Pos EJ BitRegisterProc cml 3 A E cro List m i B No Re Type Source inv n lasi sad ARE NIVEA 5 stan BitRegisterProc cml GLOBAL 2 type compatibility BitRegisterProc cml INIT functions 3 type compatibility BitRegisterProc cml INIT LOAD int oflow Byte Byte gt bool i es ls i oflow i j i j gt 255 A 4 type compatibility i BitRegisterProc cml INIT LOAD int READ ADC 5 type compatibility BitRegisterProc cml INIT LOAD int READ ADC cr hele ees Byte bool 6 j operation establishes p BitRegisterProc cml INIT LOAD int READ ADC uTlow 1 code tl ii it bees i J J 7 type compatibility BitRegisterProc cml INIT LOAD int READ ADC 8 type compatibility BitRegisterProc cml INIT LOAD int READ ADC channels a i i i i ea 9 j operation establishes p BitRegisterProc cml INIT LOAD int READ ADC init overflow underflow ae ag p eg read load add sub Byte I cM Po Details El Console 2 Problems m type invariant satisfiable obligation GLOBAL exists n Byte n gt 0 and n lt 255 Figure 52 Results of proof obligation
155. ons e is an expression P x is a predicate expression with x free c is a channel name cs is a channel set expression ns is a nameset expres sion Operator Syntax Termination SK1p Deadlock SLOP Divergence Div Prefixing cle x P x gt A Guarded action le amp A Sequential composition A B External choice A B Internal choice A B Abstraction A WA ES Channel renaming A c lt nc Recursion mu X F X Mutual Recursion mu X Y F X Y G X Y Comments terminate immediately It yields a state with no outgoing transition It yields a livelock It waits specific for units of time represented by tock events offers the environment a choice of events of the form c e p wherep in set x x T P x Only forms like c x where x is an integer are supported if e is true behave like A otherwise behave like Stop behave like A until A terminates then behave like B offer the environment the choice between A and B nondeterministically behave either like A or B behave as A with the events in cs hidden Not implemented definition of a recursive action Recursive actions must be explicit e g P P a gt P Not implemented Table 20 Action constructors 140 D31 4a Symphony IDE User Manual Public COMPASS Operator Syntax Comments Interrupt A _ B The usual CML untimed interruption operator Timed interrupt A _e_ B The usual CML timed interruption o
156. orem prover This tactic is described in more detail in FP13 It is beyond the scope of this document to provide detailed descriptions of theorem proving using the Isabelle tool or to provide a tutorial on it s use We therefore rec ommend that interested parties should read this deliverable in conjunction with tutorials on Isabelle and proving in the Isabelle tool available on the Isabelle website 56 D31 4a Symphony IDE User Manual Public COMPASS O O Isabelle Dwarf generated Isabelle 2013 11 26 09 55 24 Dwarf_User thy The Symphony IDE Users nrjp6 Dropbox University Eclipse Workspaces CMLWorkspace x o HGS A A Quy Qe sr E 5 Oy r T R Proje z li vv Q Quick Access E Ecm b isabelle B Poc Dwarf cml S Dwarf thy S Dwarf_User thy m BE Outline 38 f gt lal amp l theory Dwarf_User E theory Dwarf_User imports utp_cml Dwarf begin CML Project 2 imports utp_cml Dwarf Auto generated THY file for user created proof gt ie Dwarf 3 begin V F lemma SimpleGoall 1 lt 2 true gt 2 InsMinus lt v by gt PSLE 5text Auto generated THY file for user created proof with Dwarf_User thy V F lemma SimpleGoal2 forall x nat amp x gt 5 gt POGTestProject 6 v ey 7 lemma SimpleGoal1 vi syi NeverShowAll mk_DwarfType amp stop amp sto S i Boe YE ai aa ype amp st 16 Y F l
157. orer CML Editor Refinement Law Details Refinement Laws CML Refinement Proof Obli gation RPO List and CML RPO Details The first two are the same as in the CML perspective The panel Refinement Laws presents the list of applicable refinement laws the Refinement Law Details panel shows the details of the selected refinement law the CML RPO List panel list all the proof obligations generated by the application of refinement laws and the RPO Details panel presents the details of a selected proof obligation 11 3 Applying Refinement Laws In order to apply a refinement law the excerpt of the specification to which the law is to be applied must be selected as shown in Figure 82 Next the applicable laws can be searched by right clicking on the excerpt and selecting Refinement Refine or pressing Ctrl 6 as shown in Figure 83 79 D31 4a Symphony IDE User Manual Public COMPASS amp EML E Refinement L orer est cm E Refinement Laws w E cML Expl bd 6 A test cml X 6 JIC Refi tLaws X v channels c nat Law Name o Y test process test begin gt E test cml state v nat 1 actions A true amp c v gt A B val x nat Stop A B v end C CMLRPOList X m Ni Re Type Source E Refinement Law Details amp fm lt Refinement Laws gt E CML RPO Details writable Insert 13 4 Figure 81 Refinement perspective E BL E Refinement B cML Explorer X 6 A test ml X
158. ormulas An RT Tester test procedure is created that consists of RTTL RT Tester test language specifications for a stimulator and a number of test oracles A generic framework for embedding a system under test is generated together with the test procedure Test Execution Test execution describes the process of executing a test procedure together with the system under test Note that a generated RT Tester test procedure has to be compiled before it can be executed The result of a test execution is available as soon as the execution terminates but the test case and requirements tracing information requires to replay the test result against the test model and to create the test procedure documentation These two steps can be performed automatically using RTT MBT and RI Tester Generation Context and Execution Context RI Tester model based test projects use two contexts which are represented by two project sub directories Generation Context The generation context is the place where the generation of all model based test procedures of a project is prepared for every test procedure to be generated there is a separate test procedure generation context created in the sub directory TestExecut iorf named as the procedure to be created 22The folder names for the generation context and the execution context can be changed using the Project page of the RT Tester section in the Eclipse preferences see Figure 88 The names used here are the default
159. ot have any effect on the CML project to which itis attached Deleting a project will also not end the collaboration even if the original creator of the Collaboration Project deletes the project The collaboration will remain alive until the last collaborator deletes their Collaboration Project 7 3 Exchange and negotiation of model data Model data is exchanged between instances of the tool by the individual collaborators selecting the parts of their CML model they want to share with the other collaborators 37 D31 4a Symphony IDE User Manual Public COMPASS Error Log B Problems 4 Tasks E Console Contacts s Collaborative Modelling X a Messages amp Console TaBa Systems Collaboration attached to project TaBa Sys efd93ad9 3829 4c70 b9e5 9b5fac8d8226 hj attached to project Collab2 e8162005 bF55 4083 a0b6 c42e75981370 O Test attached to project EmergencyManagement e6ced7a0 2801 4aeb 9012 9d57e143b5b1 W TaBa Systems Collaboration attached to project TaBa Sys efd93ad9 3829 4c70 b9e5 9b5fac8d8226 Initiate Distributed Simulation Delete Collaboration Project Figure 36 Delete Collaboration Project in the collaboration group The exchange occurs at file level meaning that entire files are being distributed to the collaboration group This means that the model data that a collaborator wants to share has to be kept in files separated from the files containing model data that the collaborator does not want t
160. perator considering e units of time Untimed timeout A gt B The usual CML untimed timeout operator Timeout A e _ gt B The usual CML timeout operator considering e units of time Start deadline A startsby e Not implemented End deadline A endsby e Not implemented Table 21 Timed action constructors Operator Syntax Comments Interleaving no state A B execute A and B in parallel without synchronising Neither A nor B change the state Synchronous parallelism A nsl ns2 B Notimplemented Synchronous parallelism no state A B Not implemented Alphabetised parallelism A nsl csl1 cs2 nsP N implemented Alphabetised parallelism no state A csl cs2 B Not implemented Generalised parallelism A lns1 cs ns2 N implemented Generalised parallelism no state execute A and B in parallel synchronising on the events in cs Neither A nor B change the state Table 22 Parallel action constructors 141 D31 4a Symphony IDE User Manual Public COMPASS Operator Syntax Comments Replicated sequential composition i in seq e A i e must be a sequence for each i in the sequence A i is executed in order Replicated external choice i in set e A i offer the environment the choice of all actions A i such that i is in the set e Replicated internal choice i in set e A i nondeterministically behave as A i for any i in the set e Replicated interleaving
161. phony IDE shows a warning message see Figure 66 recommending the installation of FORMULA and providing the web site to download the necessary software and installation instructions Microsoft FORMULA could not be started Please download and install it from www research microsoft com en us um redmond projects formula If you have installed FORMULA include the lt FORMULA_INSTALL_FOLDER gt Base System folder in your PATH environment variable The CML model checker depends on FORMULA to work Figure 66 Message FORMULA not installed 61 D31 4a Symphony IDE User Manual Public COMPASS e The analysis is performed and the information is shown in different views The Model Checker list view shows a v or an X as result of the analysis mean ing satisfiable or unsatisfiable respectively For each analysis performed over a model there is a corresponding line in the Model Checker List View see Fig ure 67 If the user edits the model the results of the previous analysis the results of the previous analysis are still maintained in the Model Checker List View s U FiA o n MYNAT A es i me CML Model Checker 2 0O Process Property SAT LP Deadlock E top else Skip 4 Aii p 5 v Ex F s A j Figure 67 Successful analysis Itis worth mentioning that the user can cancel the analysis by pressing the cancel or stop button in the Model Checker Progress View component Furthermore for satisfiable models a graph con
162. please wait for the task to be finished gt gt TMPL _P1 PASS generate test procedure _P1 cleaning up test procedure generation context Pl please wait for the task to be finished _P1 PASS cleanup test procedure SampleProject TurnIndication TestGeneration _P1 Figure 89 Outline of the RttPerspective Workbench The Console View provides feedback in the form of log messages and error messages The Eclipse build in progress view provides information about the currently active task The RTT Plugin progress view provides information of the status of the current sub task For the task of test generation additional information about the progress of the test generation is given in the RTT Plugin progress view Whenever a RTT MBT task is started a console message is given to indicate the start of the action and the progress view is reset The completion of a task is indicated by the RTT Plugin progress bar at 100 percent and a message in the console view providing information whether the task as succeeded PASS or not FAIL The Outline is used during the analysis of test procedures This is explained in detail in Section 12 8 2 and in Ver13b 12 3 Terms and Concepts For the understanding of the rest of this chapter it is vital that the following concepts are known by the reader Some of them are just a clarification of how certain terms are used in this document while others are concepts that are used in th
163. r IP address and port number the name and a user identification has to be provided A separate server workspace is created for each user and the workspaces are identified with the 17The RTT Plugin is part of the Symphony IDE and should be installed with Symphony automatically 8More information about users and server workspace is given later in this section Note If no server workspace exists for the specified user id resetting it will fail 20Note This user manual does not cover the installation of the RTT MBT server or the RT Tester backend 83 D31 4a Symphony IDE User Manual Public e080 type filter text gt General gt Ant gt C C gt Help gt Install Update gt Java Preferences RT Tester RTT MBT plugin version Server Server version Uptime COMPASS 0 3 1 995 algieba informatik uni bremen de 9 0 1 3 0 x86_64 6c8f4ea dev up 19 days 07 13 20 gt JavaScript Library Hover gt Maven gt Plug in Development RT Tester gt Run Debug Test server connection Reset server workspace Cancel _ wok Figure 86 The RT Tester Preferences Main Page user id Therefore the user identification has to be unique within the group of users working on the same RTT MBT server An Apache module can be used to access the RTT MBT server through a HTTP S URL instead of a direct TCP IP connection In this case the complete URL has to be provided in the Server field of the pre
164. r the selected items sequentially not in paralle 2l Note that some of the RTT MBT tasks create or delete files or directories in the local file system The 85 D31 4a Symphony IDE User Manual Public COMPASS O O RttPerspective Defines ranges for signal values in this test procedure generation context Symphony IDE Users uwe Development workspa w rie BOS BBP ROUGIIK E 4 QQegr ie eor s Q Quick Access E A cm F RttPerspective o eel ProjectExplorer X amp o A Test Procedure Advanced Configuration Test Procedure Signal Ranges X o DE Outline X o v W SampleProject Abstract Signal Lower Bound Upper Bound SUT writes to TE TE writes to SUT Concrete Signal Identifier o An outline is not available Y Turnindication EmerSwitch 0 1 0 1 EmerSwitch amp conf LampsLeft 0 1 1 0 LampsLeft Outline View gt Ginc LampsRight 0 1 1 0 LampsRight Glogs TurnindLvr 0 1 0 1 TurnindLvr gt model voltage 0 0 1 0 0 I voltage mode ProgressView X o gt amp scripts gt specs Total m gt gt TestExecution TC Coverage vE i TestGeneration BCS Coverage a ra Progress View amp log 4 model amp stubs W Console X o testdata SIM PASS generate simulation gt SIM _P1 generating test procedure Pl please wait for the task to be finished a testsuit _P1 PASS generate test procedure Console Messages amp eu _P1 generating test procedure Pl
165. r to generate tests that wait unreasonably long between input changes The parameter LI Upper limit for the duration between input changes can be set to a nonnegative natural number indicating the upper limit for the duration between two input changes in time unit milliseconds Note that the latency for signals has to be taken into account when defining LI or DI Otherwise it would be possible to define configuration in which the checker will never find problems in the SUT outputs 100 D31 4a Symphony IDE User Manual Public COMPASS RB Robustness Testing ON OFF If robustness tests should be performed by the test procedure to be generated then parameter RB has to be set to 1 In this case the robustness transitions defined in TE state machines are not ignored as it is the case when RB is 0 but are performed with the percentage specified in RP see explanation of RP below and Section 12 7 1 Observe that setting RB to 1 only has an effect if e RP is greater than Q e TE components have been modelled are active and e at least one TE state machine associated with an active TE component has ro bustness transitions The default value for RB is 0 RP Robustness Transition Percentage If RB is set to 1 parameter RP is evalu ated It is an natural number in range 0 100 and specifies the percentage of robust ness transitions to be taken when residing in a TE state machine state from where some emanating trans
166. ration project New XMPP Connection XMPP Connection Wizard D Specify an XMPP account to connect to 9 User ID compass collab gmail com 7 lt user gt lt xmppserver gt port Alternative Server optional use talk google com if User ID is a Google for Domains account Password conei D Figure 29 Screenshot of the Account Information dialog There is currently a limitation in ECF which entails that accounts using Google 2 Step A be used for the Collaborative Modelling plug in as the logon process cannot be completed http www google com landing 2step 34 D31 4a Symphony IDE User Manual Public COMPASS 7 2 Creation of a Collaboration Environment The basis for establishing the collaborative environment between Symphony IDE in stances is the Collaboration Project A collaboration project defines the context for the collaboration by keeping track of the different modelling configurations and by defining a Collaboration Group which contains the collaborators 1 e other accounts logged in on other Symphony IDE instances Project Creation A Collaboration Project is created by selecting the Add new collaboration project as shown in Figure 30 Error Log Problems Tasks E Console 3 Messages Contacts Collaborative Modelling X im g Expand All s Collapse All gt D Test attached to project EmergencyMgm e6ced7a0 2801 4aeb 9012 9d57e143b5b1 P Add new
167. re generation context _P1 in the generation context and the respective test procedure P 1 in the execution context 12 4 Creating a Project RTT MBT projects can be created as a standalone Eclipse project or as a sub directory inside any existing Eclipse project Projects are created like any other Eclipse project using a wizard that is activated through the menu entry New Project from the context menu or from the File menu Although creating a project creates local files a RTT MBT server connection is re quired to retrieve project templates and initiate the server workspace How the server preferences are defined is described in Section On the first page of the wizard the type of project that is to be created has to be selected RTT MBT projects can be found in the category RT Tester as displayed in figure 91 On the next page of the wizard the location for the new project has to be specified Projects can be created anywhere in your file systen gt settings 3Note if you are planning to use RT Tester as the backend to compile and execute your test you should not use spaces in directory or file names 88 D31 4a Symphony IDE User Manual Public COMPASS e090 New Project Select a wizard y Wizards type filter text gt Plug in Development Y RT Tester SF RTT MBT Project gt E Web c Back Next gt Cancel Finish Figure 91 Creating a new RTT MBT Project chosing the project type
168. resendRescueInfoToEru gt processMessage gt receiveMessage gt endRecoveryl gt serviceRescue gt Stop NOMINAL end Listing 6 Deadlocked system example 77 D31 4a Symphony IDE User Manual Public COMPASS 11 The Refinement Tool This section describes the use of the refinement tool plug in which is distributed with the Symphony IDE This plug in takes CML specification and supports the application of refinement laws This plug in currently contains a number of simple laws but can be extended with new refinement laws in two different ways implementing the refinement law in Java or encoding the refinement law in Maude In general the latter option is simpler more powerful and less error prone However for certain types of laws for instance the copy rule that replaces an action call by its definition it is easier to implement directly in Java due to the need to search the AST for the definition of the action being called The details of how the refinement tool can be extended with new laws will be presented in D33 4 FM14 11 1 Using the Maude Tool The Maude tool can be obtained from http maude cs illinois edu and in stallation instructions are provided on that website It is important to notice that the use of Maude refinement laws is optional In order to use Maude in the refinement tool it is necessary to first install Maude and then configure the refinement tool in the Maude Setup section of the Preferen
169. riction missing iteration missing inverse missing product expressions full support record expressions partial support is_ expressions currently missing 137 D31 4a Symphony IDE User Manual Public COMPASS C 5 Operations Operator Syntax Comments Operation Declaration It defines a new operation Credit which receives a operations natural number and does not return values The se Credit nat gt mantics of Credit is to change the value of balance Credit n which should had been defined in the state Pre and post conditions are nor allowed The constructs frame rd and wr are not allowed balance balance n Table 19 Operations 138 D31 4a Symphony IDE User Manual Public COMPASS D CML Support in the Model Checker This section gives an overview of the CML constructs that are implemented We present the constructs using tables where the first column of each table gives the name of the operator the second gives an informal syntax and the last is a short description that gives the operator s status If a construct is not supported entirely no or partial implementation of the semantics then the name of operator will be highlighted in red and a description of the issue will appear in the third column 139 D31 4a Symphony IDE User Manual Public COMPASS D 1 Actions The following tables describe all of the supported and partially supported actions Where A and B are acti
170. rowse through the contents of the project and select the correct files to be exported All the files contained in the project will be selected by default 3 Enter a name for the archive file in the text box following To archive file A specific path to place the final file can be selected through the button Browse 4 Click on the Finish button to complete the export process 14 D31 4a Symphony IDE User Manual Public COMPASS Select an import source type filter text Y amp General G Archive File i Existing Projects into Workspace File System E Preferences gt Install gt Overture gt Run Debug Y amp Symphony gt Team B Finish Figure 7 Symphony Example import dialog Import Projects Select a directory to search for existing Eclipse projects e Select archive file v Browse Projects AccountSys AccountSys Select All Airport Airport Alarm Alarm AVDeviceDiscovery AVDeviceDiscovery a AVDeviceDiscovery_MC AVDeviceDiscovery_MC BEOCoSimulation_MC BEOCoSimulation_MC Refresh BEOStreaming_MC BEOStreaming_MC BitRegister BitRegister BitRegister_MC BitRegister_MC AA RorderTraffic S2C RordarTraffic S2C Options lt 4 Search for nested projects v Copy projects into workspace Working sets Add project to working sets Working sets S lt Back Cancoi Figure 8 Symphony Example selection 15 D31 4a Symphony IDE User Manual Publi
171. s and Cor nela Zahlten Automated model based testing with RT Tester Technical report 2011 http www informatik uni bremen de agbs testingbenchmarks turn_indicator tool rtt mbt pdf A W Roscoe Understanding Concurrent Systems Springer London Dordrecht Heidelberg New York 2010 Verified Systems International GmbH Bremen RT Tester 6 0 4 9 8 User Manual 2013 Available on request from Verified System International GmbH Verified Systems International GmbH RTI MBT Model Based Test Generator RTT MBT Version 9 0 1 0 0 User Manual Technical Re 118 D31 4a Symphony IDE User Manual Public COMPASS WCF 12 WG 11 port Verified INT 003 2012 Verified Systems International GmbH 2013 Available on request from Verified System International GmbH J Woodcock A Cavalcanti J Fitzgerald P Larsen A Miyazawa and S Perry Features of CML a Formal Modelling Language for Systems of Systems In Proceedings of the 7th International Conference on System of System Engineering IEEE July 2012 RTCA SC 205 EUROCAE WG 71 Software Considerations in Airborne Systems and Equipment Certification Technical Report RTCA DO 178C RTCA Inc 1140 Connecticut Avenue N W Suite 1020 Washington D C 20036 December 2011 119 D31 4a Symphony IDE User Manual Public COMPASS A CML Support in the Simulator This section gives an overview of the CML constructs that are implemented for inter pretation As all of th
172. shot of either a whole CML model or parts of a CML model that a modeller proposes as a potential system design A Configuration contains any number of files from the workspace of the CML project to which the Collaboration Project is attached Other collaborators can then either Approve or Reject a proposed Configura tion indicated by red and green colors or they can choose to evolve the model further by making alterations to the model data and placing it in a new Configuration that can be send to the other participating collaborators as an improved proposal m Connectivity Configuration Model elements Figure 26 Basic principles of the Collaboration The key functionality of the Collaborative Modelling plugin can be summed up in four points Connectivity between Symphony IDE instances Establishing connections between Symphony IDE instances using instant messaging technology 32 D31 4a Symphony IDE User Manual Public COMPASS Creation of a collaboration environment Creating an environment in the Symphony IDE that enables collaborative work Exchange and negotiation of model data Transferring model data between collabo ration and reaching consensus on model design Distributed simulation Performing distributed simulation between collaborators in the collaboration environment These four points are detailed in the respective sections below The Collaborative Modelling plug in defines an Eclipse View called Collaborative
173. sts its actions 1 D31 4a Symphony IDE User Manual Public COMPASS O O CML Dwarf Dwarf cml Symphony IDE Users jwc Development compass repo ide product target products eu compassresearch ide product macosx cocoa x w Civ B A A Qr Tv QO Qa Bw Ar v Qr Q Quick Access E Ecm EJ cM Explorer 58 A pwarf cmi 38 g Ge Outline X anwe x oo all y 4 Lampld lt L1 gt lt L2 gt lt L3 gt E f es amp gt airport jire os 4 Signal set of a gt AvDeviceDiscovery Sie ip Id 4 ProperState Signa gt Y BitRegister oe ee V 4 DwarfType record type ee lastproperstate ProperState gt E ChoiceSupportinDebugger setPS ProperState shine Signal me gt Ey Dwarf cmi thunk et B Dwarf launch la process Dwarf begin cu gt i3 IncubatorMonitor gt iS RingBuffer desiredproperstate ProperState y state DwarfSignal DwarfType gt Stack ip Stac dw DwarfType of dark Signal i c3 o stop Signal operations o i Signal Init O O sarig igna InitO o drive Signal dw mk_DwarfType stop stop stop stop NeverShowAll DwarfType boo post dw lastproperstate stop and MaxOneLampChange DwarfType bool dw turnoff and ForbidStopToDrive DwarfType bool dw turnon and DarkOnlyToStop DwarfType bool dw laststate stop and DarkOnlyFromStop DwarfType boo dw currentstate stop and e gt init light Lampid 4 extinguish
174. t can be imported in this fashion can be seen at symphonytool org examples 13 D31 4a Symphony IDE User Manual Public COMPASS E New Project Project Create a new project resource Project name ASystemsOfSystemsProject Use default location Working sets Add project to working sets lt Back Next gt cancel Em F f Figure 6 Create Project Wizard 4 2 2 Existing Symphony projects Follow these steps in order to import an already existing Symphony project 1 Right click the explorer view and select Import followed by General Existing Projects into Workspace this can be seen in Click Next to proceed 2 If the project is contained in a folder select the radio button Select root directory if it is contained in a compressed file select Select archive file These options will be presented in a dialog similar to that in 3 Click on the active Browse button and navigate in the file system until the project to be imported is located 4 Click the button Finish The imported project will appear on the Symphony ex plorer view 4 3 Exporting Symphony projects Follow these steps in order to export a Symphony project 1 Right click on the target project and select Export followed by General Archive File See for more details 2 A new window like the one shown in will follow In this case the selected project will appear as root node on the left side of it It is possible to b
175. taining the trace validating the property is accessible by a double clicking the item in the Model Checker List View If the Graph Viz tool is not installed the Symphony IDE shows a warning message see Figure 68 recommending the installation of GraphViz and providing the web site to download GraphViz Symphony The dot exe program was not found It is distributed with GraphViz www graphviz org Please download and install GraphViz If you have installed GraphViz include the lt GRAPHVIZ_INSTALL_FOLDER gt bin folder in your PATH environment variable The dot exe program is necessary to build the counterexample Figure 68 Message GraphViz not installed e A conversion error occurs This kind of error occurs less frequently and rep resents a translation error from CML to FORMULA and should be reported as explained in Chapter 2 The Symphony IDE shows a popup with this informa tion as illustrated by Figure 69 e An internal FORMULA occurs If some error occurs during the analysis in FORMULA the Symphony IDE shows a corresponding popup see Figure 70 Detailed information about this error will be available at the default Error Log available at the bottom panel of Symphony as in Figure 71 or through the menu Window gt Show View gt Other gt General gt Error Log The model checker analysis uses an auxiliary folder generated modelchecker to generate the FORMULA file with extension 4m1 This file is giv
176. ted gt Action cs test CML Debugger 1 EY test_model cml 5 E Dwarf cml A c Outline CML Event Options X 7 O channels init ab process A begin state v int init gt v a gt Skip end process B begin init gt b gt Skip end process test A init B 0 v l ou console X Tasks 9 Error Log a Ex Be EE e Bri Quick Launch CML Model CML Debugger Evart status AY S AY T LJINAJNALSNLp f Waiting for environment on tau AAssignmentStm gt ASkipAction test cs WAITING FOR ENVIRONMENT RUNNING Waiting for environment on tau ASequentialCompositionAction gt ACommunicationAction test cs WATTTNG ENR ENVUTRANMENT Figure 22 The interpreter is currently suspended because a breakpoint is hit The line of the breakpoint is highlighted in green and has an arrow in the left ruler In the variable view in the top right corner the state variable for process A can be seen iy A z Wey OvrQr AF7 Oey Q E Ecm Debug Debug amp vY OG 6 Variables e Breakpoints O Observable Event History al r BY lt terminated gt Quick Launch CML Model gt amp lt terminated gt CML Debug Target ai lt terminated exit value O gt CML Debugger Simulation Error Error 4072 Postcondition failure post_dummyOp in home akm phd runtime COMPASS ny test test_model cml at line 8 5 test_model cml X E Dwarf cml Outline CML Ev
177. ter environment are available from Atego and Verified Systems International respectively and are not distributed through the SourceForge net website Obtaining those software environments is outside of the scope of this docu ment The URLs for these are http www atego com download center products category artisan studio and https www verified de products rt tester In case any issues are discovered with Symphony bugs should be reported at https github com symphonytool symphony issues new Using the Help Report Symphony bug menu for the tool will automatically get you to that URL http www eclipse org 10 D31 4a Symphony IDE User Manual Public COMPASS 3 Using the Symphony Perspective When the Symphony IDE is started the splash screen from Figure 2 should appear The first time it is started you must decide where you want the default place for your projects to be Click ok to start using the default workspace and close the welcome screen to get started for the first time Symphony Formal Modelling for Systems of Systems Figure 2 The Symphony splash screen used at startup 3 1 Eclipse Terminology Eclipse is an open source platform based around a workbench that provides a common look and feel to a large collection of extension products Thus for a user familiar with one Eclipse product it will generally be easy to start using a different product on the same workbench The Eclipse workbench cons
178. tforward to see that the INIT operation puts the value MAX 1 in the state variable Depending on the increment value the trace to deadlock changes For example using the value 1 two increments are necessary to cause an overflow see Figure 73 If one changes the values of increment to 2 only one increment is performed before reaching a deadlock 64 D31 4a Symphony IDE User Manual Public COMPASS f Model Checker Model checker counterexample The Symphony IDE C AA File Edit Navigate Search Project Theorem Prover Isabelle Run Window Help ri At A QrQrireUr Se eror a Quick Access H Bm E CML Explorer 52 A Symphony A Outline 22 a m A i a i An outline is not available GS AVDeviceDi i 77 init G tau tau inc 1 tau 6 eviceDiscovery_ E BEOCoSimulation_MC E BEOStreamingSo_MC 4 W BitRegister MC amp generated register launch simpler register cml E CUSSoS_MC E DPhilosophers_MC mc CML Model Checke 28 O E InfComm_MCc Process Property SAT PRec Deadlock RegisterProc Deadlock amp 4 T R E Model Checker 2 7 Gi Error Log X E Problems 4 Tasks E Console v Ex pi v Sm 4g 7 Workspace Log No operations to display at this tim type filter text Message Plug in Date Concluido _ _ Figure 73 Graph of Bit Register It is worth noting that the content of any state of the graph is available by putting the cursor over the state
179. the basic configuration is also copied when creating a new generation context from an existing one So changes to the default configuration in the source context also apply to the new target context Solver Configuration File The solver configuration file TestProcedures lt Generation Context gt conf advanced conf contains the fields described in Table 3 Each configuration entry in advanced conf consists of a single line each line is structured into lt Parameter gt lt Value gt lt Comment gt 99 D31 4a Symphony IDE User Manual Public COMPASS Table 3 Configuration parameters and default values Deti GC 1 If 1 cover all goals in addgoals ordered conf even if they are already covered by other procedures Br o f Switch back wacking oni O OOS 10 0 Produce logger threads instead of checkers it A 0 Use abstract interpretation for speed up of solver FE MM 0 Masmiemodcoveag it SOS CSC 0 Perform sanity checks in solver and abstract interpreet RB 0 Dorobusiness testing SSS RP 0 IFRB 1 RP defines the percentage of robustness transitions to be performed MC 0 Perform model checking instead of test generation CI Maximal number of simultaneous input changes Parameter CI changed inputs is a non negative natural number It specifies the number of in puts that may be changed simultaneously after a delay The input vector to the SUT may be changed after time delays during which th
180. theorems Symbol Viewer A quick method of adding mathematical symbols to a theory 49 D31 4a Symphony IDE User Manual Public COMPASS file The user can double click a symbol which will be added to the proof script 4 Using the theory file editor pane theorems and lemmas may be defined and proven The theory editor of Isabelle Eclipse provides an interactive asyn chronous method for theorem proving similar to the jEdit interface distributed with Isabelle The theory file is submitted to Isabelle and results are reported asynchronously in the editor and prover output panes The editor has syntax highlighting for the Isabelle n and problems are marked and displayed in the output pane In the next section we use the steps defined here to use the Isabelle perspective to prove lemmas related to an example CML model 8 4 Proving CML Theorems In this section we provide a brief overview to theorem proving in the Symphony IDE As proving theorems about a CML model in Isabelle is performed in much the same way as normal theorem proving in Isabelle the interested reader should refer to tutori als on theorem proving with Isabelle for more details We consider two main methods of theorem proving in the Symphony IDE discharging POs and model specific conjec tures In Section 8 4 2 we describe the initial Proof Obligation Gneration Thoerem Prover POG TP link and in Section 8 4 3 we consider general theorem proving in CML 8 4
181. tial generation context P1 will be used to create further contexts to be used for the generation of additional test procedures If the test model is changed it can be imported again using the RT I MBT pull down menu and selecting Import Model Note that re importing a test model can lead to necessary adjustments in all test pro cedure generation context definitions and generated test procedures depending on the differences between the old model and the new one 12 5 Automated Generation of the First Test Procedure The automated generation of the very first test procedure is performed in the test pro cedure generation context TestGeneration Pl which has been created as a result of the model import during project setup as de scribed in Section The configuration of the generation context comprises two steps before the automated generation can be activated 90 D31 4a Symphony IDE User Manual Public COMPASS e Configuration of the test procedure generation context e Configuration of the signal map 12 5 1 Configure the first test procedure generation context The test configuration file contains information about model components to be used during the generation process and basic test cases to be covered in the test procedure to be created Before generating the first procedure _P 1 it has to be configured by means of the configuration editor in the RT T MBT perspective e Double click on TestGeneration _P1l cont confi
182. tions of how to prove theorems in the Isabelle tool or to provide a tutorial on its use We therefore recommend that interested parties should read this user manual in conjunction with tutorials on Isabelle and proving in the Isabelle tool available on the Isabelle website Section 8 1 describes how to obtain the software Section 8 2 describes how to install the software in the Symphony IDE Section 8 3 explains how to use the Symphony Eclipse perspective and Section 8 4 describes how to prove theorems in the Symphony IDE 8 1 Obtaining the Software This section of the user manual assumes that has been read and followed 8 1 1 Isabelle Isabelle is a free application distributed under the BSD license It is available for Linux Windows and Mac OS X The tool is available at Instructions for installation for each platform are provided in the following sections Mac OS X Instructions for installation of Isabelle for Mac are as follows 1 Download Isabelle version Isabelle 2013 2 for Mac distributed as a dmg disk image 2 Open the disk image and move the application into the Applications folder 3 NOTE Do not launch the tool at this point Windows Instructions for installation of Isabelle for Windows are as follows 1 Download Isabelle version Isabelle 2013 2 for Windows distributed as an exe executable file 2 Open the executable which automatically installs the Isabelle tool 3 NOTE Do not launch the to
183. ts ErrorDetectionChannels RecoveryChannels and OperationChannels ChaosE CSP s definition of chaos see Ros10 The no fault version of system see APR 13 Lazy definition of system see APR 13 Lazy definition of system in parallel with the limit process see APR 13 NoFault_ lt system gt Lazy_ lt system gt LazyLimit_ lt system gt 10 1 Performing Fault Tolerance Verification To verify a CML model with the Fault Tolerance Plugin open the CML file in the Symphony IDE right click on the relevant top level CML process either on the project navigator as shown in Figure 76 or on the CML model shown in Figure 77 select Fault Tolerance Verify 70 D31 4a Symphony IDE User Manual Public COMPASS CML InsielSimpleFtVerfication insiel ft verification cml The Symphony IDE W File Edit Navigate Search rie las CML Explorer 2 m 7 a InsielSimpleFtVerification gt i t generated j insiel ft vertfication cml 5 Alpha_DLSimple Alpha 5 Alpha_FFTSimple Alph 5 Alpha_LFTSimple Alphi 5 Alpha_NFTSimple Alph 5 Alpha sendRescuelnf t DLSimple NOMINAL _D E faultl errorl failuri a Ss endRecoveryl errorl 5 F faulti failurel 5 fault Project Isabelle Run Window Help Qs insiel ft verification cm 52 5 faulti errori failurel 6 7 chansets 8 E faulti errori fa 9 F faultl 1 H startRecoveryl en
184. ug in creates two theory files with the 53 D31 4a Symphony IDE User Manual Public COMPASS POG The Symphony IDE re EY File Edit Navigate Search Project Theorem Prover Isabelle Run Window Help a b coy FAQ a Got Sros E CML Explorer Fa Blom Po tist z Hg No Res Type Source 1 i state invariant initialized Airport cml inv_ actionClass 2 i state invariant satisfiable Airport cml inv_ actionClass a gaani i state invariant PAMPOEN ak 7 EAn Airport cml Init GivePermi state invariant holds Airport cml Init GivePermi 3 4 5 state invariant holds 6 m 7 state invariant holds Airport cml Init GivePermi Problems I CML Po Details E Console state invariant holds obligation Init landed subset permission gt landed subset Figure 55 Proof Obligation Generation Proof Session Perspective EJ CML Explorer X U Dwarf cmi X B z types LampId lt L1 gt lt L2 gt lt L3 gt Y i Dwarf Sianal set of LampId a New Signal E Dwarf Open s in set dark stop warning drive gt genera p E READM Open With gt lastproperstate ProperState gt ef intrTest turnoff set of LampId H Copy C turnon set of LampId Paste TAN laststate Signal currentstate Signal X Delete E desiredproperstate ProperState Move Rename F2 entstate
185. ugin is not connected to an instant messaging account See Section 7 1 this menu will not appear In the appearing Initialise Distributed Simulation dialog shown in Figure 43 the co ordinating process has to be selected as well as the simulate animate mode in which 41 D31 4a Symphony IDE User Manual Public COMPASS Error Log Problems Tasks E Console A Messages A Contacts s Collaborative Modelling TaBa Systems Collaboration attached to project TaBa System efd93ad9 3829 4c70 b9e5 9b5fac8d8226 gt D hj attached to project Collab1 e8162005 bF55 4083 a0b6 c42e75981370 7 D Test attached to project EmergencyMgm e6ced7a0 2801 4aeb 9012 9d57e143b5b1 gt 1 Configurations 8 gt Collaborators 2 TaBa Systems Collaboration attached to project TaBa System efd93ad9 3829 4c70 b9e5 9b5fac8d8226 gt D Configurations 1 v Collaborators 3 mm compass collab3 gmail com Initiate Distributed Simulation Delete Collaboration Project mm compass collab gmail com mm compass collab2 gmail com Figure 42 Initiate Distributed Simulation menu simulator should be running In the frame below all the processes defined in the CML project that the Collaboration Project is attached to will be listed Each of these processes can be selected as being an external process that needs to be simulated by another collaborator than the coordinator Initialise Distributed Simulation Select the process th
186. un will stay on the perspective that is currently active To create a new breakpoint you have to double click on the ruler to left in the editor view if created this will insert a small dot to the left ruler Breakpoints can be set on processes actions and expressions only Double clicking on a existing breakpoint dot will remove it In a debugging session is in progress Here a breakpoint on the a event in process A has been hit and the interpreter has been suspended At this point the current state can be inspected in the variables view From here it is both possible to resume or stop the debugging session If the resume button is clicked the interpretation is resumed and the stop button stops it 6 3 4 Error reporting If an error occurs a dialog will appear with a message explaining the cause of the error Furthermore the location of the error will be marked in the editor view In Figure 23 a post condition has been violated This is described in the error dialog and a gray marking shows where in the model it happened 26 D31 4a Symphony IDE User Manual Public COMPASS Debug test test_model cml Symphony IDE File Edit Navigate Search Project Run Window Help i E 32 op rOrQar eave Por Q E A cmu Debug Debug X Y A Variables X Breakpoints H Observable Event History tH Y 7 Oo v E Quick Launch CML Model Name Value Y a CML Debug Target a Action test cs test_model cml line 8 a lt termina
187. ut it is always han dled When the process chooses the FAULT action that communicates the lt Fault1 gt event the RECOVERY action always communicates the events processMessage and receiveMessage process FFTSimple begin actions NOMINAL sendRescuelInfoToEru gt processMessage gt RECEIVE FAULT RECEIVE receiveMessage gt serviceRescue gt NOMINAL FAULT unwanted lt Faultl gt gt RECOVERY RECOVERY StartRecoveryl gt logFaultl gt resendRescueInfoToEru gt processMessage gt receiveMessage gt endRecoveryl gt serviceRescue gt NOMINAL NOMINAL end Listing 3 Full Fault Tolerance example The verification of this example raises a warning on the tool Figure 77 D as the model does not include any failures It is recommended that possible failures are modelled even in the case of fully fault tolerant systems I5 Note we acknowledge that no real system is fully fault tolerant in general because there is always a non zero probability of a failure occurring 75 D31 4a Symphony IDE User Manual Public COMPASS 10 2 2 Example The system shown in Listing 4 is not fault tolerant in general but it is with regard to a set of limiting conditions representing foreseen faults Note that the system model in cludes errors and failures which are not handled by the defined recovery mechanisms It represents a real system where detected faults are handled but for those faults the system
188. y 10 2 Fault Tolerance Verification Plugin Example This section provides small examples to illustrate four key cases of verifying fault tolerance The examples were extracted from ERS case study and are summarised as follows FFT Full Fault Tolerance LFT Limited Fault Tolerance NFT No Fault Tolerance DL The system is deadlocked All examples we show use the definitions listed in types Unwanted lt Fault1l1 gt lt Errorl gt lt Failurel gt channels sendRescueInfoTokEru processMessage receiveMessage serviceRescue startRecoveryl endRecoveryl logFaultl resendRescueInfoToEru unwanted Unwanted chansets H startRecoveryl endRecoveryl logFaultl resendRescuelInfoToEru Alpha sendRescueInfoToEru processMessage receiveMessage serviceRescue startRecoveryl endRecoveryl 74 D31 4a Symphony IDE User Manual Public COMPASS logFaultl resendRescueInfoToEru Alpha_LFTSimple Alpha Alpha_NFTSimple Alpha Alpha_DLSimple Alpha Alpha_FFTSimple Alpha process Lim process Lim process Lim process Lim t_LFTSimple Limit t_NFTSimple Limit t_DLSimple Limit t_FFTSimple Limit process Limit begin actions Init unwanted lt Faultl gt gt Init Init end Listing 2 Basic definitions 10 2 1 Example The CML model of a system that is fully fault tolerant is shown in Listing 3 gt Note that no failure occurs in this system model only lt Fault1 gt occurs b
189. y are not defined in the local project properties of the respective project The terms Test Generation Context and Test Execution Context are defined and explained in Sec tion 12 3 The Project page contains two fields to define default names for these two directories 84 D31 4a Symphony IDE User Manual Public COMPASS 0o00 Preferences type filter text Project qv Y gt Help RTT MBT sett gt Install Update WER gt Isabelle Test Execution Context TestExecution P Java Test Generation Context TestGeneration Maude Setup Model Checker Setup Client Mode Symphony gt Plug in Development WRT Tester Verbose Console Logging Retrieve Extra Files Server gt Run Debug Restore Defaults Apply gt Symphony Cancel _ 0K Figure 88 The RTT MBT General Project Settings Page The RTT Plugin can operate in different client modes The current client mode can be selected using the Client Mode drop down listbox Currently only the client modes Symphony Verified and Papyrus are supported The checkbox Verbose Console Logging enables extra output to the RTT MBT con sole view during task execution This output can be helpful to identify problems during test generation or execution Without this switch only essential log messages and error messages are sent to the console view The Checkbox Retrieve Extra Files enables or disables the download of additional files from the RT T MBT server after a server task has
190. yntax These topics are RTT MBT specific and independent of the graphical user interfaces While this document concentrates on the RTT Plugin integrated in the Symphony tool and are recom mended as side reading to this manual The tests that are generated by RTT Plugin within the COMPASS project are RT Tester test procedures The RT Tester manual Ver13a provides detailed information about RT Tester and the test language RTTL the tests are expressed in 12 1 RTT MBT Preferences A number of preferences can be defined to customize the RTT Plugin behaviour If the plugin is installed correctly the Eclipse preferences should contain a separate section RT Tester with two sub sections Server and Project The RT Tester page contains sta tus information about the currently installed RTT Plugin version the configured RTT MBT server the server version and the uptime of the server The server version and uptime are unknown displayed as until the Test server connection but ton is activated This initiates a server connection test and evaluates uptime and server version from the response The button Reset server workspace can be used to erase the data for the configured user id on the RTT MBT server 8 Since RTT MBT operates in client server mode the server name or IP address is re quired in the RTT Plugin preferenceq Figure 87 shows the Server page of the RT Tester section in the Eclipse preferences In addition to the server name o
191. ystem PowerSubsystem cml b BodySubsystem o i InteriorSubsystem E Road cmi vy i InteriorSubsystem a l LightingSubsystem gt A StateMachine_HybridSUV come l Lightingsubsystem a c ChassisSubsystem SUV_EPA_Fuel_Economy_T T c i ChassisSubsystem an 5 N o active_act_Operate lt act_Accelerate 6 Transmission cml s active_act_Operate lt act_Accelerate_Cruising gt lt act_Braking gt lt act_Idle gt lt act_Initial1 gt 2 act exit Final S lt gt lt lt gt Error Log amp R Problems 2 Tasks EJ Console 5 El Ee X of Workspace Log type filter text Message Plug in Date A HSUV HybridSUV StateMachine_HybridSUV cml Figure 109 State machine model 111 D31 4a Symphony IDE User Manual Public COMPASS 14 The Command line Tool The command line interface to the COMPASS tool was conceived as a tool for devel opers to quickly allow them to access and test the core libraries This allows developers of the tool to quickly test new functionality for correctness without having to create the GUI elements that will control the functionality in the integrated IDE A beneficial side effect of having this tool is that general users are not required to load the IDE to test CML programs but instead may invoke them via the command line Presently cm1c is available alongside the main Symphony IDE bundle see Section 2 but as a separate file The command line tool in provided as a ZIP file cmlc 0 4 Q

Fourth Release of the COMPASS Tool Symphony IDE User Manual

Contents

Download Pdf Manuals

Related Search

Related Contents