Tutorial for Overture/VDM++
Contents
1. This is exactly describing that in order for this expression to be defined it is necessary to gurantee that there exists at least one such expert Thus without taking the pre condition for the operation here into account it would not be possible to gurantee that So it will never be possible to automat ically to determin this using simple pattern matching because this is only guranteed because of the invariant over the instance variables for the P1ant class that has been defined 3 11 A Command Line Interface So far only the graphical user interface of Overture has been presented but the core of Overture also provides a simple command line interface This is useful for the automatic batch execution of tests though the command line also provides a full set of interactive execution and debugging commands which can be useful when examining batch tests Overture is written in Java and so to run it from the command line the Overture jar file should be executed with a Java JRE version 7 or later java jar Overture 2 0 0 jar 15See the Overture documentation at sourceforge net projects overture for the location of the jar file or use the script or windows bat file incorporating this 20 Chapter 3 Overture Tool Support for VDM an Introductory Guide E If the jar file is executed with no further options like this it will print a list of available options and exit The most important option is the VDM dialect that the2. Sfin Serverlisten 0 aP ObjectThread 5 on vCPU RUNNABLE vi VOM debugger plentvdmpp testalarmvdmst E alarmvdmst ES pop3testvdmpp ES pop3message vdmpp Ed messagechannel vdmpp E Sc D SE Outline 2 Lao xo MessageChannel ROI data ClientCommand ServerResponse syno sei per ServerListen gt ffin ClientSend 1 a debug b fin ServerListen m Send ChentCommand ServerResponse 17 m Listen ClientCommand ServerResponse o ServerSend ServerResponse isten gt ffin ServerSend 1 fin ClientListen ClientListen ServerResponse ClientSend ClientCommand ServerListen wen D per Servertisten 5 dicate EJ Console 3 gt j Tasks LR Debug Console POP3 Testi VDM PP Model VDMJ debugger Debug console Creating POP3ClientHandler ClientSend fin ClientSendClient c says gt mk POPSTypes USER paul Figure 3 12 Debugging perspective Button Explanation Resume debugging Suspend debugging Terminate debugging Step into Step over Step return Use step filters Table 3 1 Overture debugging buttons 12 Chapter 3 Overture Tool Support for VDM an Introductory Guide E The Variables view shows all the variables in a given context when a breakpoint is reached The variables and their displayed values are automatically updated when stepping through a model The view is located in the upper right corner in the Debug perspe
3. 000010 traces Adding ndDeleting let myex in set exs 6 in 37 let myex2 in set exs in myex let p in set ps in plant AddExpertToSchedule p myex plant AddExpert ToSchedule p myex2 plant RemoveExpertFrom chedule p myex 3 Test 000011 3 Test 000012 f Test 000013 ze Test 000014 f Test 000015 Test 000016 44 plant RemoveExpertFromSchedule p ryex2 45 4 Test 000017 e xl A El Problems El Console CT Test Case result 3 lt LI Trace Test case Result A plant AddExpertToSchedule mk_token Tuesday day myex i plant AddExpertToSchedule mk token Tuesday day myex2 D plant RemoveExpertFromSchedule mk token Tuesday day myex Error 4130 Instance invariant violated inv Plant in Part at line 6 e 4 gt Figure 3 17 Using Combinatorial Testing for the Alarm VDM model The syntax for traces also enables operation repetition and alternatives to be specified but these were not needed for this simple case Using the full power of traces it is possible to efficiently generate and execute very large test suites Naturally this is most likely to find inconsistencies when the model attempts to define its essential predicates invariants pre and post conditions 14Note that when using repetitions and sequencing in combination it is easy to define traces that expands to hundreds of thousands of test cases and naturally their execution may then
4. 3 2 Exporting the UML model to XMI format in Modelio Chapter 3 Overture Tool Support for VDM an Introductory Guide E workbench consists of several panels known as views such as the VDM Explorer view at the top left of Figure 3 3 A particular collection of panels designed to assist a specific activity is called a perspective For example Figure 3 3 shows the standard Overture perspective which contains views for managing Overture projects viewing and editing files As we shall see later several other perspectives are also available in Overture EE VOM AlarmPP plantvdmpp Overtwe Toois II imm File Edit Navigate Search Project Run Window Help ri ia 0O m Switch coins aii ES PO Proof Obliga B Combinatori 35 Debug EJ YH VfB vom Explorer 53 D E alarmvdmpp Ea opetvampp E mp O Ss Outline 2 wwew inberOfExperts p O Plant VOM Projets return card schedule p ay MP e TTITTe p in set dom schedule s bra ped il hi dui of E AlarmEn a schedule map Period to set of Expert E SS public ExpertIsOnDuty Expert gt set of Period E AlarmPP 54 ExpertIsOnDuty ex m Plantinv set of Alarm map Period to osetof Exp E generated 9 return p p in set dom schedule amp 5 Palod tokem A ex in set schedule p o ExpertToPage Alarm Period Expert E epertvdmpp 6 NumberOfExperts Period nat amp plantvdmpp public Plant set of Alarm e ExpertlsOnDuty Expert set of Pe E RE
5. 3 PlantExpertToPage Alarm Period map apply A post ed expert ME 4 Plant ExpertToPage Alarm Period operation post condition A expert in set sEIEEBWETD and 5 PlantExpertToPage Alarm Period let be st existence A ReqQuali in set expert GetQuali 6 PlantExpertToPage Alarm Period map apply A 7 Plant NumberOfExperts Period map apply A 1 8 Plant ExpertisOnDuty Expert map apply public NumberofExperts Period gt nat 9 PlantPlant set of Alarm map Period to set of Expert state invariant A NumberofExperts p 10 Testl plant map sequence compatible A return card schedule p pre p in set dom schedule public ExpertIsOnDuty Expert gt set of Period ExpertIsOnDuty ex return p p in set dom schedule amp ex in set schedule p public Plant set of Alarm map Period to set of Expert Plant Plant als sch alarms als Schedule sch E Problems EJ Console PO Proof Obligation View 7 EN let expert Expert RESULT in p in set dom schedule Figure 3 18 The Proof Obligation view for the Alarm VDM model One of the first proof obligations listed for this example is related to the Plant Inv function Recall that the first part of the function s definition is as follows PlantInv set of Alarm map Period to set of Expert gt bool PlantInv as sch forall p in set dom sch sch p lt gt and The proof obligation records the constraint that th
6. Appendix A A Chemical Plant Example class Plant instance variables alarms set of Alarm schedule map Period to set of Expert inv PlantInv alarms schedule functions PlantInv set of Alarm map Period to set of Expert gt bool PlantInv as sch forall p in set dom sch amp sch p lt gt and forall a in set as amp forall p in set dom sch amp exists expert in set sch p amp a GetReqQuali in set expert GetQuali types public Period token operations public ExpertToPage Alarm zx Period gt Expert ExpertToPage a p let expert in set schedule p be st a GetReqQuali in set expert GetQuali in return expert pre a in set alarms and p in set dom schedule post let expert RESULT in expert in set schedule p and a GetReqQuali in set expert GetQuali public NumberOfExperts Period gt nat NumberOfExperts p 29 E Tutorial to Overture VDM RT return card schedule p pre p in set dom schedule public ExpertIsOnDuty Expert gt set of Period ExpertIsOnDuty ex return p p in set dom schedule amp ex in set schedule p public Plant set of Alarm x map Period to set of Expert gt Plant Plant als sch alarms als Schedule sch pre PlantInv als sch end Plant A 2 3 The Expert Class class Expert instance variables quali set of Qualificati
7. Combinatorial Testing perspective you will see the CT Overview view Inside this combinatorial testing view you can select the Alarm tracesPP project right click it and choose the Full Evaluation option as shown in Figure 3 16 Now Overture expands and executes all 48 test cases one after another The results of these executions are illustrated with green check marks and red crosses meaning 17 that the tests passed or failed respectively see Figure 3 17 Note that in the Combinatorial Testing perspective the view in the lower region is able to show the individual steps of a selected test case along with the corresponding results from its four operation calls Tutorial to Overture VDM RT Full Evaluation Filtered Evaluation Go Home Go Back Go Inte Figure 3 16 Invoking the combinatorial testing feature test1 vdmpp Overture Tools E L Di xj Project Run Window Help ES ES combinatorial 3 gt EEN Cas B Steg 2 E plant vdmpp ES expert vdmpp Es tracker vdmpp Dis Bo Overview ES N ELI ei al x 24 operations e o e 8 26 public Run gt set of Plant Period Expert Wa Wc ACCES 27 Run DI 8 let periods plant ExpertIsOnDuty exi Bw AddingAndDeleting 29 expert plant ExpertToPage al pi Test 000001 30 in Test 000002 return mk periods expert 103 4 Test 000005 Test 000006 f Test 000007 f Test 000008 Test 000009 f Test
8. Expert 8 m Plantinv set of Alarm map Period to set of Expert bo 29public ExpertToPage Alarm Period Expert E a Period token 30ExpertToPage a p e ExpertToPage Alarm Period Expert let expert in set schedule p be st 6 NumberOfExperts Period nat a GetReqQuali in set expert GetQuali e ExpertlsOnDuty Expert set of Period in return expert 35pre a in set alarms and 4 m 4 m r f Plant set of Alarm map Period to set of Expert Plant Figure 3 6 The Outline View couple of expressions typed in at the box at the botton of the view are evaluated Note that in order to get a console where you are able to make use of definitions you need to use the console launch mode as described in Section 3 7 1 below E Problems 23 Tasks E Console 9 wom Quick Interpreter 3 4x l gt 2 x x in set 1 20 amp x mod 2 0 16 gt 32 2 gt 4 18 gt 36 4 gt 8 20 gt 40 6 gt 12 8 16 10 gt 20 12 gt 24 14 gt 28 E power 7 3 1 fh 1 3 3 1 7 47 1h 0 35 47 3 13 s En p Figure 3 7 The VDM quick interpreter view Most of the other features of the workbench such as the menus and toolbars are similar to those used in other Eclipse applications though it is worth noting that there is a special menu with Overture specific functionality One convenient feature is a toolbar that appears on the right side of the s
9. be very slow if one executes them all Thus it is also possible to use a feature that reduce the numbers of tests to be executed 18 Chapter 3 Overture Tool Support for VDM an Introductory Guide E 3 10 Proof Obligations The Overture tool is also able to generate Proof Obligations automatically for VDM models Proof obligations are boolean expressions that describe constraints to be met at various points in the model in order to ensure that the model is internally consistent 1 e no run time errors will occur while debugging if these are all satisfied Proof obligations are generated to ensure for example that operations will always respect invariants on instance variables Each proof obligation generated from a model should evaluate to true The proof obligation generator is invoked by right clicking on the project in the Explorer view and then selecting the Proof Obligations gt Generate Proof Obligations entry This will start up a proof obligation perspective with a special PO view For the alarm example this view takes the form shown in Figure 3 18 EJ popatestvdmpp El plantvdmpp 7 A PO Proof Obligation Explorer 33 Filter proved O a GetReqQuali in set expert GetQuali No PO Name Type Status in return expert 1 PlantPlantinv set of Alarm map Period to set of Expert map apply pre a in set alarms and 2 Plant Plantinv set of Alarm map Period to set of Expert map apply p in set dom schedule
10. double clicking in left margin in the editor view When the debugger reaches the location of a breakpoint evaluation suspends and you can inspect the values of different variables and step through the VDM model line by line 3 7 2 The Debug Perspective The Debug view in the upper left corner of the Debug perspective shows all running threads in the VDM model and their call stacks It also shows whether a given model is stopped suspended or running All threads are also shown along with their running status It is possible to switch between threads from the Debug view At the top of the view are buttons for controlling debugging such as stop step into step over and resume These are standard Eclipse debugging buttons see Table 3 1 11 Tutorial to Overture VDM RT Bono POP3 messogechoncelvdmen Overture Tools NENNEN CC E beste F e Edit Navigate Search Project Run Window Help re O rQ EE A bA E DaB ES PO Proof Obliga Bl Combinatori 3 Debug EJ VOM 3 Debug 1 r wg anables lt s E POP3 Testi VOM PP Model H me Value i i SU Call traces in debug Ir Inspecting variables in WATIN 4 Instance Variables aff ObjectThread 6 on vCPU RUNNABLE 4 9 date POP3Types USER aP ObjectThread 7 on vCPU RUNNING nime pau messagechannelvdmpp line 94 Y debug true pop3clienthandler vdmpp line 400 en 10 566 popiserver vdmpp line 130 4 fin ClientSend 1 aP ObjectThread 4 on vCPU WAITING
11. gt Clearly a batch of test evaluations could be performed automatically by running a series of similar commands and saving the output results for comparison against expected results To run the command line interpreter interactively the i command line option must be given Instead of terminating after the type check this will cause VDMJ to enter its interactive mode and give the interactive prompt Type checked 4 classes in 0 078 secs No type errors Initialized 4 classes in 0 063 secs Interpreter started 21 E Tutorial to Overture VDM RT E From this prompt various interactive commands can be given to evaluate expressions debug their evaluation or examine the VDM model environment The help command lists the commands available The quit command leaves the interpreter For example the following session illustrates the creation of a test object followed by an evaluation using a print command of its Run operation and a debug session with a breakpoint at the start of the same operation create test new Test1 print test Run mk mk token Monday day Expert f3 quali lt Mech gt lt Bio gt Executed in 0 15 secs gt gt gt break Testl Run Created break 1 in Testl testl vdmpp at line 26 3 26 let periods plant ExpertIsOnDuty ex1 gt print test Run Stopped break 1 in Test1 testl vdmpp at line 26 3 26 let periods
12. the IO standard library Afterwards one simply select Finish Now you have an almost empty project with the exception of the IO vdmpp file in the 1ib directory and you can then either add new VDM files to the project or simply paste in existing VDM source files from elsewhere Adding a VDM file to a project you can rightclick on the project and then select New VDM PP Class and then give a meaning full name e g Test to the class you would like to start defining and press Finish This will create a new class file with the selected name and with space for the different kinds of definitions you can make inside such a VDM class 19Tt is possible to see and enhance the complete list of these by selecting Window Preferences gt VDM gt Templates Chapter 3 Overture Tool Support for VDM an Introductory Guide E lala Select a wizard gt Wizards de VDM SL Project Figure 3 9 Creating a New VDM Project BB Add Library Wizard Add Library Select the libraries to include Figure 3 10 The VDM Standard Libraries 3 6 Mapping Between UML and VDM In order to map the UML class diagram created in Modelio to VDM use a new project inside the VDM Explorer Paste the UML file exported from Modelio into this new project By right clicking on the XMI UML file in the VDM Explorer view the UML Transformation can be chosen followed by Convert to VDM This will create a new
13. tool should use In the case of our alarm example we want to use VDM for which the option is vdmpp After this we can simply specify the names of the VDM model files to load or the name of a directory from which all VDM model files will be loaded java jar Overture 2 0 0 jar vdmpp AlarmPP That will perform a syntax and type check of all the VDM model files in the AlarmPP directory producing any errors and warning messages on the console before terminating Parsed 4 classes in 0 109 secs No syntax errors Type checked 4 classes in 0 093 secs No type errors In the case of our alarm example there are no syntax or type checking errors Any warnings can be suppressed using the w option If a VDM model has no type checking errors it can either be given an expression to evaluate as an option on the command line or the user can enter an interactive mode to evaluate expressions and debug their execution To evaluate an expression from the command line the e option is used followed by a VDM expression to evaluate You may also find the q option useful as this suppresses the informational messages about the parsing and type checking java jar Overture 2 0 0 jar vdmpp q new Testl Run AlarmPP This produces a single line of output for the evaluation since the parsing and checking messages are suppressed mk mk token Monday day Expert f3 quali lt Mech gt lt Bio
14. 0 0 2 plant vdmpp 89 096 5 where the Expert IsOnDut y and ExpertToPage operations are fully covered by just one call due to the fact that its body is simply one line whereas the Plant Inv operation is called twice Exercise 3 4 Before reading on try to add two new operations to the Plant class called AddExpertToSchedule and RemoveExpertFromSchedule respectively for adding and removing an expert to from the schedule for a paticular period Please remmebr to include pre conditions when necessary 15 Ei Tutorial to Overture VDM RT E ES generated latex AlarmPP aux B AlarmPP log AlarmPP pdf la AlarmPP tex AlarmPP toc 2 overture sty n overturelanguagedef sty ES generated latex specification alarm vdmpp expert vdmpp E plant vdmpp test1 vdmpp E README 5 8 EC Figure 3 15 The generated pdf file with test coverage information 3 9 Combinatorial Testing The previous sections have shown how to test and debug models manually However Overture also contains a feature enabling more automation in the testing process making more comprehensive high volume testing feasible It is possible to write regular expressions as traces that one would like to expand into a large set of individual tests When new traces are incorporated in a VDM project you may need to press the Refresh button in the CT Overview view In order to illustrat
15. ADME txt map Period to set of Expert gt Plant 6 Plant set of Alarm map Period to set of Expert vdmpp Plant als sch als VDM Model files z pret Interpreter fem view 3 errors 606 warnings 0 other rs Filter matched 103 of 609 items Description Location Type Errors 3 items Problem view amp Warnings 100 of 606 items vi seg Error Log E Writable Insert 52 1 SS M See Figure 3 3 The Overture Perspective The VDM Explorer view allows you to create select and delete Overture projects and navigate between the files in these projects Start by importing the alarm project from zip file mentioned above This can be done by right clicking the project view and selecting Import followed by General Existing Projects into Workspace In this way the projects from zip file mentioned above can be imported easily Initially it is recommended that you only import the AlarmErrPP and the Alarm tracesPP projects as shown in Figure 3 48 An editor customised to the dialect of VDM being used in the project will appear when one of the imported files are selected in the Explorer view by double clicking When the AlarmErrPP project has been imported one can right click on the project in the Explorer view and then select the Properties item in the menu and then Figure 3 5 will pop up This includes the properties set for this project including specific VDM options Note that there i
16. Expert Qualification GetReqQuali return reqQuali e oper operationName parameterNames statements pre preCondition post postCondition onName parameterTypes resultType end Alarm el Figure 3 8 Explicit operation template Templates can be particularly useful when modifying VDM models If you hit the key combination CTRL space after the initial characters of the template needed Overture triggers a proposal For example if you type op followed by CTRL space the Overture IDE will propose the use of an implicit or explicit operation template as shown in Figure 3 8 The Overture IDE supports several types of template cases quantifications functions explicit implicit operations explicit implicit and many more Additional templates can easily be added in the future The use of templates makes it much easier for users lacking deep familiarity with VDM syntax to nevertheless construct models A new VDM project is created by choosing File New gt Project The dialog box shown in Figure 3 9 will appear Ensure that VDM is selected as the project type click Next and then name the project AlarmUML Following this it is possible to select standard libraries as shown in Figure 3 10 These standard libraries gives the possibility to get standard input output math and general utility functionality by selecting the appropriate standard libraries In this AlarmUML project we can try to select
17. Overture Technical Report Series No TR 004 April 2013 Tutorial for Overture VDM by Peter Gorm Larsen John Fitzgerald Sune Wolff Nick Battle Kenneth Lausdahl Augusto Ribeiro Kenneth Pierce Overture Open source Tools for Formal Modelling Tutorial to Overture VDM RT Document history Month Year Version Version of Overture exe January 2010 0 1 5 March 2010 0 2 May 2010 1 0 2 February 2011 2 1 0 0 April 2013 3 2 0 0 11 Contents 3 Overture Tool Support for VDM an Introductory Guide 1 Sub dntFOdUCHON hes det Sou e roe ded cU SO ue oe Pee oe dedo e mob edt Geo 1 3 2 Obtamime ENEE 2 33 Usima Modelo at a a nae is GRE wot EE 3 3 4 Using the Overture Perspective 2 ards d edu E Se Deia E 3 3 5 Getting Started using Templates esco RE RE SE SRS 7 3 6 Mapping Between UML and VDM lle 9 AJ Deb gsmg A en NI aha xe xo A AE A AE SR 10 3 7 1 The Debug Configuration uuu msn RR hup RSEN 10 37 2 The Debug Perspective 29v EREETETRESQE EE 11 2 53 A um Ede kde Rx 13 e A co dard uta Ae he gti Qu Ma uo die MP eg to det aus 14 3 9 Combinatorial Teste gar soe uto BC A A Rent RS A en A RN a 16 3 10 Proof Obligations 55 5 S te gana e eC oC ROO CLR LOO A 19 3 11 A Command Line Interface 234 uoce ci oe ee reote ete dr ess 2 20 SEES TOES MER E RC E ROT T E T ETT LT TTC CERTO TETTE 23 A A Chemical Plant Example 27 A l An informal description vi
18. Overture for serious applications including the exercises in the book However this is by no means a complete guide to Overture more information can be obtained from www overturetool org 3 1 Introduction One of the main benefits of combining VDM and UML class diagrams and sequence diagrams is the ability to use software tools to assist in the analysis of the models Often the analytic power of John Fitzgerald Peter Gorm Larsen Paul Mukherjee Nico Plat and Marcel Verhoef Validated Designs for Object oriented Systems Springer New York 2005 ISBN 1 85233 881 4 www vdmbook com 3Note that the Overture tool suite support three different VDM dialects VDM SL Specification Language VDM and VDM RT Real Time so although this tutorial illustrate how to use Overture with VDM models you will see multiple references to these dialects 2 E Tutorial to Overture VDM RT UML models alone can be limited as many tools concentrate on just the structural view of classes However the combination of Modelio and Overture provides a significant number of benefits This guide can be used to illustrate the combination of Modelio and Overture support or just Overture support if a UML tool is not available or desired Section 3 2 describes how to obtain the tools For those readers who would like to start using Modelio Section 3 3 briefly explains how a first model can be built in UML Section 3 4 provides an initial introduction
19. VDMTools originally developed by IFAD A S is now maintained and developed by SCSK see http www vdmtools jp en From Overture it is also possible automatically to transfer a project over to VDMTools 3 3 Using Modelio This section describes the tool support available if you wish to start model construction using UML class diagrams The AlarmInitUML uml file can be found on the book s web site This UML class diagram model is identical to the initial class diagram from the previous chapter except that the Plant class has been updated with the three operations identified in Appendix A Note that the operations have not yet been given signatures Download this um1 file and import it using Modelio When this model is open the class diagram should look like that shown in Figure 3 1 The small next to the r le name schedule indicates that this association is public The in front of the r le name alarms indicates that it is private You can change the visibility of the schedule association to private by selecting the association and changing the Visibility with the To Expert You can update the signatures for the operations in the Pl ant class However this is awkward and most developers prefer to use a text editor to perform such updates in the VDM text then converting back to the UML model automatically To convert a UML class diagram model to a VDM model you first need to export the UML model from Modelio to the Eclipse
20. XMI format called UML using the EMF UML3 0 0 format see Figure 3 2 This is then subsequently imported into Overture as will be explained in Section 3 6 3 4 Using the Overture Perspective Eclipse is an open source platform based on a workbench that provides a common look and feel to a large collection of extension products Thus if a user is familiar with one Eclipse product it will generally be easy to start using a different product on the same workbench The Eclipse http www vdmbook com twiki bin viewfile Main BookExamples rev 1 filename AlarmInitUML uml Tutorial to Overture VDM RT Expert2Page ExpertisOnDuty NumberOfExperts mmm St Period string schedule quali integer Figure 3 1 The initial UML class diagram in Modelio 00 Operation gt Esse L f 2 Raised Exception SP a 3 Alarminit ai 3 E Plant Lf Create a diagram gt E Alem Create an element E E XMI Export E Alar Add stereotype dica i utis iin Ej Close project I C Users pgl modelio workspace Alarm XMI AlarminitUML um e Cut ES Options E Copy Compatibility Extension Paste Cte V Y Adding Modelio annotations O xmi leges Comte EMFUMI300 uml CSS Ier Rename E Em Macros p E T Desc Th Ben Th moda E Create Update automatic diagrams Model Components i m LU m Litems selected Figure
21. at the VDM level Save it and it will automatically be syntax and type checked at the VDM level Then export the model to XMI in order to see your changes in a new project in Modelio 3 7 Debugging This section describes how to debug a model by testing it using the Overture IDE A test file Test1 vdmpp can be found in the alarm project and it is provided in Appendix A 2 Using this test it is possible to exercise the system informally in order to check if the correct expert is paged as a result of a given alarm 3 7 1 The Debug Configuration Before the debugging can begin in Overture a debug configuration must be created by right click ing the project and choosing Debug As Debug configuration The debug configuration dialog have 3 different launch modes Entry Point This is the standard Eclipse approach where one decides before debugging which operation function to call Remote Console This is an anvanced option that enables remote control of the interpreter and this is described in the Overture user manual Larsen amp 10 Console This will simply start up a console where the user interactive can debug different opera tions functions defined in the selected project For VDMTools users this will be a familiar console corresponding to a VDM model that has been initialised in VDMTbols interpreter 10 Chapter 3 Overture Tool Support for VDM an Introductory Guide E Here we will start with u
22. creen and allows the user to switch between perspectives the particular perspectives on show here vary dynamically according to history 3 5 Getting Started using Templates Before proceeding please make sure that you have imported both the AlarmErrPP and the Alarm tracesPP projects as shown in Figure 3 4 When editing a VDM model the Over ture IDE parses the content of the editor buffer continuously as changes are made Any parse errors will be reported in the problems view as well as being highlighted in the editor See the bottom of Figure 3 3 Each time a VDM model file is saved the editor type checks the model and reports any errors or warnings Note also that the suggestions made in the error messages may not always be entirely the action you may wish to take when correcting the source since the tool cannot guess what you intended to write If errors appear in this evaluation the current version of the Overture IDE simply yield a Fatal error where it is anticipated that later releases will provide more helpful run time errors to the users 7 E Tutorial to Overture VDM RT Ed talarmavdmpo 23 Ed expert vdmpp E plant vdmpp ES testi vdmpp EPI public String seq of char instance variables descr String reqQuali Expert Qualification operations public Alarm Expert Qualification String gt Alarm Alarm quali str descr str reqQuali quali 17 public GetReqQuali gt
23. ctive 09 Variables Co Breakpoints 53 GL Expressions S w DE B nt 9 wDM PP Plant vdmpp line 29 Figure 3 13 Breakpoint View 3 7 3 Breakpoints The Breakpoints view gives an overview of all breakpoints set see Figure 3 13 From this view you can easily navigate to the location of a given breakpoint disable or delete them or set their properties Conditional breakpoints are also supported These are a powerful tool for the developer since they allow a condition to be specified which has to be true in order for the debugger to stop at the given breakpoint The condition can either be a boolean expression using variables in scope at the breakpoint or it can be a hit count after which the breakpoint should become active n Properties for S xq Breakpoint properties Line Breakpoint M TY Filename tree vdmpp Line 83 V Enable Hit Counter Enable Condition condition is true value of condition changes o EM Figure 3 14 Conditional breakpoint options You can make a simple breakpoint conditional by right clicking on the breakpoint mark in the left margin of the editor and selecting the option Breakpoint properties This opens a dialog shown 13 Ei Tutorial to Overture VDM RT in Figure 3 14 The Expressions view allows the user to enter watch expressions whose values are automati cally displayed and updated when stepping Watch expressions can be added man
24. e how this can be used we extend the Plant class with two additional operations for adding and removing experts from a given schedule Both operations take a given Period and an Expert and then update the schedule instance variable from the Plant class The AddExpertToSchedule operation can be defined as public AddExpertToSchedule Period Expert gt AddExpertToSchedule p ex schedule p if p in set dom schedule then schedule p union ex else ex and the RemoveExpertFromSchedule operation can be expressed as public RemoveExpertFromSchedule Period Expert gt RemoveExpertFromSchedule p ex let exs schedule p in schedule if card exs then p schedule else schedule p gt exs ex 16 Chapter 3 Overture Tool Support for VDM an Introductory Guide E pre p in set dom schedule l Note that RemoveExpertFromSchedule contains a deliberate error It fails to take account of the invariant so the operation can leave the Plant in a state where it cannot be guaranteed that experts with the right qualifications are available in the periods that have been scheduled AddExpertToSchedule has a similar error If nobody is scheduled at the period provided as an argument and the expert added for the schedule at this period does not have all the necessary qualifications the invariant will again be violated In fact this means that one would probably have
25. e mapping application sch p should be valid i e that the p is in the domain of the mapping sch This is described as a proof obligation in the following form forall as set of Alarm sch map Period to set of Expert amp forall p in set dom sch amp p in set dom sch 19 Ei Tutorial to Overture VDM RT Itis easy to see with simple pattern matching that this proof obligation is true and thus in the Proof Obligation Explorer view the status field the small checkmark indicates that indeed the proof obligation generation have been able to automatically determine this In general proof obligations represent checks that should be made on a model in order to gain confidence in its consistency At present proof obligations have to be checked by manual inspec tion of the model code Proof tools are being developed for Overture to check as many as possible of the proof obligations automatically and with human assistance but there are always likely to be some that have to be checked manually If we for example instead consider the fifth proof obligation it is derived from the body of the expert ToPage operation That body looks like let expert in set schedule p be st a GetReqQuali in set expert GetQuali in return expert where an expert on duty with the right qualifications are being selected The proof obligation here states exists expert in set schedule p amp a GetReqQuali in set expert GetQuali
26. elopment of a model of an alarm system to meet these requirements is initiated The purpose of the model is to clarify the rules governing the duty roster and calling out of experts to deal with alarms A 2 A VDM model of the Alarm example This section presents the UML class diagram and the full VDM model of the alarm example However it does so without any explanatory text That is placed in the VDM book so if you are a newcommer to VDM please read that there A 2 1 A UML Class Diagram In Figure A 1 the final class diagram for the extended alarm example is shown from Enterprise Architect Plant Alarm st1 nat alarms Plantinv in as Set Alarm in sch Map lt Plant Period Set lt Expert gt bool __ reqQuali Qualification ExpertToPage in a Alarm in p Period Expert 1 Alarm in quali Qualification in str MyString NumberOfExperts in p Period nat GetReqQuali Qualification ExpertlsOnDuty in ex Expert Set Plant Period gt Plant in als Set lt Alarm in sch Map Plant Period Set lt Expert gt gt Plant Period Period schedule Expert quali Qualification Expert in qs Set lt Expert Qualification gt Expert GetQuali Set lt Expert Qualification gt E Figure A 1 UML diagram translated from VDM files A 2 2 The Plant Class The Plant class is the main class in this example 28
27. erface 23 Tutorial to Overture VDM RT 24 References Fitzgerald amp 98 Larsen amp 10 John Fitzgerald and Peter Gorm Larsen Modelling Systems Practical Tools and Techniques in Software Development Cambridge University Press 1998 Peter Gorm Larsen and Kenneth Lausdahl and Augusto Ribeiro and Sune Wolff and Nick Battle Overture VDM 10 Tool Support User Guide Techni cal Report TR 2010 02 The Overture Initiative www overturetool org May 2010 103 pages 25 Tutorial to Overture VDM RT 26 Appendix A A Chemical Plant Example This appendix presents the requirements for a simple alarm system for a chemical plant It forms a running example that serves to illustrate the process described earlier and to introduce elements of the VDM modelling language Although the modelling process is described here as though it were a single pass activity a real development would usually be iterative A 1 Aninformal description The example is inspired by a subcomponent of a large alarm system developed by IFAD A S and introduced in Fitzgerald amp 98 A model of the system will be developed and validated using the facilities of Enterprise Architect and Overture enabling a graphical overview of the model in the form of UML class diagrams and sequence diagrams corresponding to traces Chapter 3 provides an interactive and hands on tour of the tools available for supporting the development of the model Imagine that yo
28. ike Overture this tool is built on top of the Eclipse platform The product can be obtained from http www modelio org A large library of sample VDM models including all those needed for the exercises in the book is available and can be downloaded from the URL https sourceforge net projects overture Dit is planned to develop an update facility allowing updates to be applied directly from within the generic Eclipse platform without requiring a reinstallation However this can be a risky process because of the dependencies on non Overture components and so is not yet supported The library files are created to be used with Eclipse but can be opened with file compression programs like Winrar on Windows Chapter 3 Overture Tool Support for VDM an Introductory Guide E http overture sourceforge net examples ExamplesVDM_PP zip You can import the example library zip folder as described in Section 3 4 Finally the web site www vdmbook com contains all the examples used in this book as plain text files but these are also all present in the above mentioned zip file Finally in order to make use of the test coverage feature described in Section 3 8 it is necessary to have the text processing system called ATEX and its pdf latex feature This can for example be obtained from http miktex org 2 9 Note for VDMTools users Overture provides a new open source VDM tool set but it can also be used with VDMTools
29. ken Tuesday night operations public Run gt set of Plant Period zx Expert Run let periods plant ExpertIsOnDuty ex1 expert plant ExpertToPage al pl in return mk periods expert end Testl 32
30. on types public Qualification Mech Chem Bio Elec operations public Expert set of Qualification Expert Expert qs quali qs public GetQuali gt set of Qualification GetQuali return quali end Expert 30 Appendix A A Chemical Plant Example A 2 4 the Alarm Class class Alarm types public String seq of char instance variables descr i String reqQuali Expert Qualification operations public Alarm Expert Qualification String gt Alarm quali str descr str reqQuali quali Alarm public GetReqQuali gt Expert Qualification GetReqQuali return reqQuali end Alarm A 2 5 A Test Class class Testl instance variables al Alarm 31 new Alarm Mech Mechanical fault a2 Alarm new Alarm lt Chem gt Tank overflow Tutorial to Overture VDM RT ex1 Expert new Expert lt Mech gt lt Bio gt ex2 Expert new Expert Elec ex3 Expert new Expert lt Chem gt lt Bio gt lt Mech gt ex4 Expert new Expert lt Elec gt lt Chem gt plant Plant new Plant al pl gt exl ex4 p2 gt ex2 ex3 values pl Plant Period mk token Monday day p2 Plant Period mk token Monday night p3 Plant Period mk token Tuesday day p4 Plant Period mk_to
31. own in Figure 3 11 Once the debugger has completed and the result is written out in the console it is possible to right click on the AlarmPP project and select the Latex Latex coverage The coverage information that have been gathered in any expressions that have been debugged since the last change to a file have been saved or the project have been cleaned will be turned into a pdf file The AlarmPP pdf file is placed in the generated 1latex directory as shown in Figure 3 15 and it includes the VDM definitions from all the files included in the project including coverage information Note that whenever the model is adjusted or it is cleaned so it gets type checked again all the files in the generated directory are deleted The coverage information is provided in a way where uncovered expressions are shown in red in the generated pdf file In addition to the content of each VDM source file a table with coverage overview is provided in tabular form For the plant vdmpp file this looks like Function or operation Coverage Calls ExpertIsOnDuty 100 0 1 ExpertToPage 100 0 1 12Note that this feature is not yet supported for models using unicode characters such a Japanese identifiers 13Note that using this feature required pdflatex to be installed 14 Chapter 3 Overture Tool Support for VDM an Introductory Guide E NumberOfExperts 0 0 0 Plant 100 0 1 PlantInv 10
32. plant ExpertIsOnDuty ex1 MainThread 10 print plant NumberOfExperts mk token Wednesday Runtime Error 4071 Precondition failure pre NumberOfExperts in Testl console at line 1 1 MainThread 10 continue mk_ mk_token Monday day Expert 3 quali lt Mech gt lt Bio gt Executed in 72 651 secs Notice that the print command is available at the breakpoint to examine the runtime state of the system In the example we attempt to evaluate an operation which fails its precondition because the system is not yet initialized The help command is context sensitive and will list the extra debugging commands available at a breakpoint such as continue step stack list and so on The full set of commands is described in the Overture User Guide 16 Supplied with the Overture documentation 22 Chapter 3 Overture Tool Support for VDM an Introductory Guide 3 12 Summary In this guide we have introduced the following major features of tool support for VDM using Modelio with class diagrams mapping back and forth between Modelio and Overture syntax checking of VDM models type checking of VDM models executing and debugging VDM models collecting and displaying test coverage information on VDM models a command line interface combinatorial testing enabling automation of parts of the testing process proof obligation generation and a command line int
33. s e oe eo RU e EU TRO 2T A 2 A VDM model of the Alarm example llle 28 A 2 1 A UML Class Diagram 2 6 2 9 oo a 28 A22 The Plant Classi 2 ona ko das Pe OS wee A A 28 2 3 The Expert Class se uuu hex RE ERREUR 30 ADA the Alarm Class S s eto ch Peat haat imt ras ea Mag caries 31 Pura A Test Clases ii Bod ee three A dub G 31 111 Chapter 3 Overture Tool Support for VDM an Introductory Guide Preamble This is an introduction to the Overture Integrated Development Environment IDE and its facilities for supporting modelling and analysis in VDM It may be used as a substitute for Chapter 3 of Validated Designs for Object oriented Systems or as a free standing guide Additional material is available on the book s web site Throughout this guide we will refer to the textbook as the book and the book s web site simply as the web site We use examples based on the alarm case study introduced in Chapter 2 of the book For read ers using this as a free standing guide an informal explanation of the case study and its VDM model are given in Appendix A The model has been slightly extended from the original version in order to illustrate Overture s test automation features We introduce the features of Overture that support the combination of formal modelling in VDM with object oriented design using UML This is done by providing a hands on tour of Overture providing enough detail to allow you to use
34. s a language version option that for the AlarmErrPP project set to vdm10 which indicates that it include non standard features such as traces which is explained in Section 3 9 In addition options are gathered here for additional checks where the AlarmErrPP project simply follow the standard settings used for new projects The Outline view to the right of the editor see Figure 3 6 displays an outline of the file selected in the editor It shows all declared classes their instance variables values types functions operations and traces Figure 3 3 shows the outline view on the right hand side Clicking on an operation or a function will move the cursor in the editor to the definition of that operation function You need both of these to carry out various exercises throughout this chapter Tutorial to Overture VDM RT Import Import Projects aw a Select a directory to search for existing Eclipse projects SES C Select root directory Browse C TEMP examplesPP zip Browse Select All Deselect All Refresh Select archive file Projects m Alarm proofPP Alarm proofPP Alarm tracesPP Alarm tracesPP AlarmErr AlarmErrPP O larmPP AlarmPP O AutopilotPP AutopilotPP O buffersPP buffersPP O CalculatorPP CalculatorPP O CashDispenserPP CashDispenserPP O concfactorialPP concFactorialPP zi Jv Copy Working sets Space Add project to working se
35. sing the traditional Eclipse approach with an Entry Point launch configuration which requires the project name and the class and the operation function used as the entry point of the test Figure 3 11 shows the debug configuration for the alarm model The class and operation function name can be chosen from a Browse dialog if the operation or function has arguments these must be typed in manually between the brackets of the entry point function oper ation VDM PP Launch Configurations ge mv ep Create manage and run configurations Debug Cex Br Name AlermPP type filter text Main Runtime 7 Source E Common Debugger Develop Java Applet Project Appl ae Project AlarmPP Browse Remote Java Applicatior VUMIEP Model Launch Mode AlarmPe Entry Point Remote Control Console i VDM RT Model amp VDM SL Model Entry Point Function Operation Run Remote Control Fully qualified remote control class Other Y Generate coverage H A Revert Filter matched 7 of 7 items w JI Ree J A 2 Debug Close Figure 3 11 The debug configuration dialog Once the debug configuration is ready the model can be debugged If any breakpoints are set this will change the main perspective of the Overture IDE to the Debug perspective which contains the views needed for debugging in VDM The Debug perspective is illustrated in Figure 3 12 Breakpoints can easily be set by
36. to change the signature of this operation such that it instead of taking a simple expert would take a collection of experts Instead of adding the two operations manually use the Alarm tracesPP project We could use the debugger presented above to test these two new operations manually but we can also automate a part of this process In order to do the automation Overture needs to know about the combinations of operation calls that you would like to have carried out so it is necessary to write a kind of regular expression called a trace VDM has been extended such that traces can be written directly as a part of a VDM model In our case inside the Test 1 class one can write traces AddingAndDeleting let myex in set exs in let myex2 in set exs myex in let p in set ps in plant AddExpertToSchedule p myex lant AddExpertToSchedule p myex2 lant RemoveExpertFromSchedule p myex lant RemoveExpertFromSchedule p myex2 OS CO UO The three nested let be statements in the trace called AddingAndDeleting yield all possible combinations of their variable bindings whereas manual debugging will just select a few combina tions The cardinality of these sets determines the overall number of test cases each being formed as a sequence of four operation calls as shown In this case the cardinality of the three sets are respectively 4 3 and 4 Multiplying these gives 48 tests in total If you select the
37. to the terminology used by Eclipse tools such as Overture Section 3 6 shows how to import Modelio UML model into Overture and export them back to UML again Section 3 7 describes the process of testing and debugging using Overture Section 3 8 describes how line coverage from using the debugger can be covered and displayed Section 3 9 shows how parts of the test process can be automated using Overture s combinatorial testing feature Section 3 10 demonstrates how it is possible to automatically generate the additional checks called proof obligations needed in order to ensure that a model is consistent Finally Section 3 11 illustrates how parts of Overture s functionality can be accessed from a command line 3 2 Obtaining the Tools In order to run the examples and exercises presented in the book it is necessary to install two separate tools Overture and Modelio Overture This is an open source tool developed by a community of volunteers and built on the Eclipse platform The Overture development project is managed on SourceForge The best way to run Overture is to download a special version of Eclipse with the Overture functionality already pre installed If you go to http sourceforge net projects overture files you can find pre installed versions of Overture for Windows Linux and Mac Modelio This is a tool that is both available in a commercial version as well as in an open source setting from a company called Softeam Just l
38. ts Working sets Y lt Back Netz JI oe Cancel Figure 3 4 Importing the Alarm VDM Projects Properties for AlarmErrPP 9 X type filter text YDM Settings lt P y vv Resource Builders Language options Project References Language version vamo gt Refactoring History Run Debug Settings Type checking VDM Build Path E Suppress warnings VDM Settings Restore Defaults Apply o Figure 3 5 Properties for the AlarmErrPP Project At the top of the outline view there is a button to optionally order the elements of the outline view alphabetically The Problems view presents information about all the open projects you are working on such as warning and error messages In Figure 3 3 the problems view is shown at the bottom In the standard Overture perspective there is a VDM Quick Interpreter view in a pane in the same area as the problems view This can be used for evaluation of standard VDM expressions independent of all VDM projects incorporated in your Overture IDE This can be very convenient to gain understanding of the different VDM operators In Figure 3 7 it is possible to see how a 6 Chapter 3 Overture Tool Support for VDM an Introductory Guide E E bag vdmsl li bagtest vdmsl plant vdmpp 23 B Outline 53 IW WR Wiele SS Ee 2 4 Plant 25 public token a alarms set of Alarm 6 n stl nat 27 operations a schedule map Period to set of
39. u are developing a system that manages the calling out of experts to deal with operational faults discovered in a chemical plant The plant is equipped with sensors that are able to raise alarms in response to conditions in the plant When an alarm is raised an expert must be called to the scene Experts have different qualifications for coping with different kinds of alarms It has been decided to produce a model to ensure that the rules concerning the duty schedule and the calling out of experts are correctly understood and implemented The individual requirements are labelled R1 R8 for further reference R1 A computer based system is to be developed to manage the alarms of this plant R2 Four kinds of qualifications are needed to cope with the alarms electrical mechanical biological and chemical R3 There must be experts on duty during all periods allocated in the system R4 Each expert can have a list of qualifications R5 Each alarm reported to the system has a qualification associated with it along with a descrip tion of the alarm that can be understood by the expert 27 E Tutorial to Overture VDM RT R6 Whenever an alarm is received by the system an expert with the right qualification should be found so that he or she can be paged R7 The experts should be able to use the system database to check when they will be on duty R8 It must be possible to assess the number of experts on duty In the next section the dev
40. ually or created by selecting create watch expression from the Variables view It is possible to edit existing expres sions Like the Breakpoints view this view is hidden in the upper right hand corner in Figure 3 12 Exercise 3 3 Use the interpreter to evaluate the following expression new Testl1 Run O 3 8 Test coverage It is often useful to know how much of a model has been exercised by a set of tests This gives some insight into the thoroughness of a test suite and may also help to identify parts of the model that have not been assessed allowing new tests to be devised to cover these When any evaluation is performed on a VDM model the interpreter records the lines of the VDM model that are executed This permits the line coverage to be examined after a test to identify the parts of the VDM model that have not yet been exercised coverage is cumulative so a set of tests can be executed and their total coverage examined at the end In our simple example the different tests in the exercise above does cause the majority of the VDM model to be executed but for demonstration purposes let us start by cleaning the model right click on the project and select Clean If we simply take the AlarmPP debug launch configuration the Expert IsOnDuty and ExpertToPage operations in plant vdmpp are called by the Run function Remember that whenever test coverage information is desired the Generate Coverage option must be selected as sh
41. um import directory with one vdmpp file per class from the UML model The round trip engineering abilities of this link however is still at a prototype stage so if you wish to use this you have to expect that this part is still not as automatic as we would like The three classes from the Alarm system will be converted to VDM format vdmpp one file per class Before proceeding delete the AlarmUML project in the Overture IDE For the following the 9 Ei Tutorial to Overture VDM RT AlarmErrPP project is used This project contains a number of VDM model files with a number of deliberate errors The errors are common ones such a semicolons separating definitions that has been forgotten Exercise 3 1 Correct all the errors discovered by the syntax and type checker from Overture and save the corrected files Continue this process until no errors appear Hint Consult the model presented in Appendix A to see how values note using rather than types and construc tors should be defined and how access modifiers should be used After correcting all the errors in the AlarmErrPP project it is possible to map the complete VDM model to UML To do this simply right click the project root and choose UML Transforma tion Export XMI The XMI file can subsequently be imported in Modelio enabling the user to get an overview of the complete model Exercise 3 2 Add an instance variable to one of the other classes
Download Pdf Manuals
Related Search