Choreographer Platfrom User Guide NV Haenel
Contents
1. The Choreographer provides background parsing for PEPA files while they are being edited This means that Choreographer will perform a syntax check at regular intervals while the file is being modified in the editor To be precise every time a single character modification to the file is made a timer is restarted when the timer expires the automatic syntax check kicks in If any syntax mistakes are found the line in question is underlined clearly with a red wave like graphic and a red cross appears in the margin of the editor If you now hover the mouse over the red cross a short description of the syntax error is displayed Diagram 7 shows a syntax mistake the underline graphic and the short error message The settings for the background parsing can be customised using Tools gt Options gt PEPA Module Settings gt General This allows you to enable disable background parsing and set the delay for the timer For more information about the State Space Derivation and the two solvers is included in the User Manual for the PEPA workbench that can be obtained from 1 6 Support for the LySa formalism The LySa module offers support for the LySa formalism the LySa menu layout is as follows Choreographer User Guide Val Haenel January 11 2005 9 DRAFT VERSION File Edit View Tools Window Help PEPA XMI LySa bg WF Attacker pepa x Ki WMFxmi x EE Bw Extractor for XMI 1 2 1 nvh degas choreographer tes2. Editor Settings gt LySa Editor There are a small number of settings to customise the LySa support offered by choreographer Tools gt Options gt LySa Settings This allows you Choreographer User Guide Val Haenel January 11 2005 10 DRAFT VERSION Syntax Font Default Guarded Block Monospaced 12 Plain i pepa comment C inherit Highlight Insertion Point Row Status Bar Glyph and Line Number Margin Foreground Color epa error l ET Text E 255 00 la pepa incomplete C Inherit pepa process identifier Matching Bracket Highlighted by Search Background Color pepa keyword mi pepa separator 255 255 255 Search Wrapped Inherit pepa operator epa action identifier ian Preview Incremental Search pepa number Code Folding pepa error Figure 8 PEPA Editor Fonts and Colours Detail to set the location of the Standard ML installation as described in the Quick Start guide There are two other options LySa Heap Image and number of instances n however these are undocumented developer features used in de bugging and development 1 7 Support for the XMI format Extractors Reflectors XMI etc explain what the extractors can do extract reflect PEPA and LySa explain how to invoke them the imp details are discussed elsewhere the concept of Extractor Reflector is discussed in background References 1 Degas choreographer website univer
3. select WMF_Attacker security zuml and then leave the default name as WMF Attacker security performance zuml This produces the file WMF_Attacker security performance zuml that contains the results from both the LySa reflection and the PEPA reflection e Lastly view the reflected model in Poseidon to convince yourself that it has worked 1 4 Using the Choreographer This section describes the three main modules offered by choreographer namely PEPA LySa and XMI and what functionality is provided by each of these from Choreographer User Guide Val Haenel January 11 2005 7 DRAFT VERSION the users point of view documenting what features are provided by each module and how to use them 1 5 Support for the PEPA formalism The PEPA module of choreographer is an interface layer that binds the PEPA Workbench Java Edition 2 into the Choreographer framework Support for the PEPA formalism is provided partly by the PEPA Workbench and partly by the Choreographer platform The PEPA menu has the following layout e Check Syntax e Derive Silent Compressed Uncompressed e Solve LNBCG Solve SOR Solve e Reflect These menu items are displayed in two distinct places the PEPA menu in the menu bar at the top of the application and in the context menu for PEPA files in the explorer PEPA files are displayed using a butterfly combinator icon in the explorer Throughout the next section assume that example p
4. Val Haenel January 11 2005 6 DRAFT VERSION q Properties Fonts and Colors Fonts amp Colors Font Size i Abbreviations Abbreviations J Line Numbers Oo Macros Macros Tab Size 8 Indentation Engine Simple Indentation Engine vil Key Bindings Key Bindings m q Expert Overwrite Caret Solid Block X Text Limit Line Color O 255 235 235 Highlight Caret Row oO Insertion Point Vertical Bar X Status Bar Visible m Display Text Limit Line Line Number Margin Iz If True the status bar showing insert mode line number TT Highlight Matching Bracket wi Line Height Correction 1 0 Scroll Find Insets 0 0 10 0 ial Overwrite Caret Color E 0 0 0 a Status Bar Caret Delay 200 Insertion Point Color E 0 0 0 Insertion Point Blink Rate 300 Margin null Scroll Jump Insets 5 10 5 30 a Text Limit Character Count 80 Plain Editor No description available _ctose_ Figure 6 Editor Properties e Now select the file WMF_Attacker pepa and right click to show the menu To solve the model Select Check Syntax Select Derive gt Silent Select Solve gt SOR Progress messages are displayed in the console as the tool advances e Reflection is now possible right click on WMF_Attacker pepa and select Reflect Again you will be presented with two file browsers the first for selecting the original and the second for selecting the destination file for the reflection For the first
5. Choreographer Platfrom User Guide N V Haenel valentin haenel gmx de The Laboratory for Foundations of Computer Science School of Informatics University of Edinburgh 2004 2005 January 11 2005 1 DRAFT VERSION latex 1 User Manual This section describes the Choreographer Platform from the point of view of the user 1 1 Introduction to the NetBeans Platform This section gives an introduction to the features of the NetBeans Platform Diagram 1 shows a common screen layout for the Choreographer Observe the Menus and Tool bars at the top of the screen The left hand side is occupied by the Explorer The right hand side contains the Editor and the bottom of the screen encompasses the output tab One of the benefits of the NetBeans Platform is that all the visual components are float able and can be repositioned within the main window for example diagram 2 shows an alternate layout a xmi o ki WMF_Attacker lysa o E wwer_anaci WMF_Attacker xmi WME_Attacker proj E WMF_Attacker pepa sino Editor ty S15 Explorer Output Window Figure 1 The Screen Layout of Choreographer NetBeans 3 6 requires a directory to be mounted in order to view or use the files in it To mount a local directory right click the icon labelled Filesystems at the top of the explorer window Select the option mount and then local directory Now select the desired directory using the file browser Once Choreographer
6. User Guide Val Haenel January 11 2005 2 DRAFT VERSION File Edit View Tools Window Help PEPA XMI LySa bOTdC Rees a a CoE Output amp Filesystems E Filesystem jamd nfs wyvern disk ptn043 s9905941 nvh degas choreogr results i WME mi o ki WMF_Attacker lysa ia WMF_Attacker zum WMF_Attacker pepa Ez Ba WMF_Attacker pepa x Pilz The following PEPA model was generated by the PEPA Extractor for XMI 1 2 From the file amd nts wyvern disk ptn043 s9905941 nvh degas choreographer test_models WMF_Attacker zum On Friday September 17 2004 3 43 05 PM BST 1 i 1 A sendKeyToS r4S A1 Al sendDataToB rAB A B sendKkeyToB infty 61 B1 sendDataToB infty B 5 sendKeyToS infty S1 S1 sendKeyToB rSB S A lt sendKeyToS gt S lt sendDataToB sendKeyToB gt B 5 9 INS Figure 2 Alternative Screen Layout of Choreographer mounted the directory is displayed as a child node of Filesystems and can be explored from there The Explorer is used to browse any mounted file systems or local directories and allows you to inspect their contents Nodes in the explorer can be expanded and collapsed to vary the depth of the displayed file system The Explorer recognises file types and will display an appropriate icon for each different file type Furthermore all file types have an associated context menu that can be used to invoke actions
7. e Context Menu Rename Properties Figure 3 Details of the Explorer as Find Selection and Find Next Occurrence that allow you to highlight a string within a document and then search the document for this string All the tool bar items have tool tips that appear when you hover the mouse over the item for 2 seconds The editor itself can be customised in a variety of ways to make the user experience more pleasant and productive Diagram 6 shows the multitude of configurable options and settings for the plain text editor All the entries have associated tool tips that are displayed at the bottom of the window The properties window can be found under Tools gt Options gt Editing gt Editor Options gt Plain editor 1 2 Installation Instructions Choreographer itself has been developed in the Java programming language the LySa tool is written in Standard ML SML Choreographer will happily work under both Windows and Linux We used Red Hat Linux kernel 2 4 and Windows XP SP1 for development and testing Choreographer requires Choreographer User Guide Val Haenel January 11 2005 4 DRAFT VERSION File Edit View Tools Window Help PEPA XMI LySa 396 23 n F 3 a ve Memory New Cut Save Copy Save All Patse Print Delete Undo Redo Figure 4 Menus and Toolbars An installation of Poseidon for UML to draw the UML diagrams An installation of Java 1 4 2 Runtime Environment for the ma
8. e for the linear biconjugate gradient method and results example sorstate for the suc cessive over relaxation To invoke the solvers select either Solve gt LNBCG Solve or Solve gt SOR Solve Progress messages will be displayed in the output window The settings for the two solvers can be accessed through Tools gt Options gt PEPA Module Settings gt LNBCG SOR settings Reflect is related to the Extractor Reflector support offered by Choreog rapher and is described in 1 7 The Choreographer provides syntax highlighting for the PEPA formalism This means that certain classes of identifiers such as component and action identifiers the PEPA keywords such as infty operators such as all numerical values and comments are displayed in differing colours This makes it easier and more comfortable to work with PEPA models Syntax highlighting is enabled by default and cannot be disabled Diagram 7 shows the syntax highlighting The syntax highlighting settings for the editor may be modified Select Tools gt Options gt Editing gt Editor Settings gt PEPA Editor This will provide you with a settings panel to tweak the settings for the PEPA editor To change the default highlighting select Fonts and Colours this will open up a list of categories such as pepa comment or pepa keyword Each of these categories has a default font size and colour that can be customised Figure 8 shows the fonts and colours window for PEPA
9. epa is the model being used The Choreographer provides some simple syntax checking that can be per formed to assert the lexical and the syntactical correctness of the model To invoke this from the menu select Check Syntax the results of the check will be displayed in the output window The Choreographer provides State Space Derivation in three output formats Silent Compressed and Uncompressed This will derive the state space of the model Silent produces no output Compressed will produce a compressed version of the state space in the file results example states This lists all the states but the sequential derivatives have been replaced with integer encoding In addition a file results example seq is produced This contains the integer encoding of the sequential derivatives and allows the compressed state space to be decoded Uncompressed will produce the file results example states this time the state space has not been encoded and the file lists all possible states of the PEPA model in verbose detail Progress messages will be displayed in the output window Choreographer User Guide Val Haenel January 11 2005 8 DRAFT VERSION There are two available solvers for steady state solution the linear biconju gate gradient method and the successive over relaxation method The first is known to converge faster and use less memory and is therefore recommended The steady state solution will be written to a file results example steadystat
10. in applica tion An installation of Standard ML of New Jersey for the LySa subcompo nent Download the latest zip from the downloads section of the choreographer website at 1 Unzip the downloaded file e Launching For Windows open the directory choreographer in an explorer and change to the bin directory From there double click runidew For Linux open a terminal and cd to the choreographer bin directory and from there execute runide sh e Set the location of the SML runtime SelectTools gt Options gt LySa settings and in the properties window select SML Runtime To set the location click on the white box on the far right hand side and select the appropriate file in the file browser window For Linux this is the file bin sml bin in the SML installation directory and for Windows it is the file bin sml bat in your SML installation directory This completes the installation and you may now use the tool Choreographer User Guide Val Haenel January 11 2005 5 DRAFT VERSION Eile Edit View Tools Window Help PEPA XMI LySa EA ww Atackerpepa Ig WHF ami x mm g ag SH From the e 5 e On Fr Septembe 17 2804 3 B t Ye eT fs model s WMF_Atta Current File Inactive File Editor Toolbar wr Main Text Window Line and Column numbers Figure 5 Editor Detail 1 3 Quick Start e Download the WMF example from the choreographer website at 1 e Se
11. lect the filesystems icon in the explorer window on the left hand side of the screen Click select mount gt local directory Then select the directory that contains the example and expand it e Now select the file WMF_Attacker zuml and right click on it From the menu select either Extract PEPA or Extract LySa to invoke the respec tive extractors This produces the files WMF_Attacker pepa and WMF Attacker lysa respectively and you should see progress messages in the console at the bottom of the screen e To invoke the LySa tool select the file WMF_Attacker lysa and right click Then select Invoke LySa from the menu to run the tool Any output appears in the console For this example the tool will determine that the protocol has possible errors This is the correct behaviour as LySa models without errors provide no results that could be reflected e Reflection is now possible right click on WMF_Attacker lysa and select Reflect You will now be presented with two file browsers the first allows you to select the original file that contains the model and the second allows you to enter a file name for the result of the reflection procedure In the first file browser select the file WMF_Attacker zuml and in the second one leave the default as WMF_Attacker security zuml This will produce the file WMF_Attacker security zuml that contains the results from the analysis The original file WMF_Attacker remains intact Choreographer User Guide
12. sity of edinburgh http groups inf ed ac uk choreographer 2 Pepa workbench java edition university of edinburgh http homepages inf ed ac uk s9905941 jPEPA Choreographer User Guide Val Haenel
13. specific to this file Diagram 3 shows the features of the Explorer in detail The Menus and Tool bars in Choreographer are used to invoke basic file and text operations such as New File Load File Save File Cut Copy Paste Undo Redo and Find Tool bars can be enabled and disabled Diagram 4 shows some of the more commonly used tool bar items All tool bar items are equipped with tool tips that appear when you hover the mopuse over the item for a couple of seconds The NetBeans Editor is a sophisticated text editor that can be used to view and modify the content of files Diagram 5 shows the most important features of the Editor Clearly visible are one active and one inactive file in a tab the editors own tool bar the main text window that is currently displaying a PEPA file and lastly the field in the lower left hand corner that displays the line and column number The tool bar contains some useful text editing commands such Choreographer User Guide Val Haenel January 11 2005 3 DRAFT VERSION Eile Edit View Tools Window Help PEPA XMI LySa Filesystems fe Filesystems e famd nts wyvern disk ptn043 s9905941 nvh degas choreographer test_models WMF_Attacker seq tacker sorstate wer_attackers WMF_attacker steadystate WMF xmi Collapsed Directory o Ei WMF AT Expanded Directory WMF_Attacker zuml F_Attack Child Node Cut Cut Icon Copy Ctrl C Check Syntax gt gt Delete Delet
14. t_model s WMF Action Identifier Process Identifier Keyword Error Message Encountered S at line 16 column 27 Osi sendkeyToB rSB S3 Error Indicator A lt sendkeyToS gt 5 lt sendDataToB sendKeyToB gt B 11 1 INS Figure 7 PEPA Editor Details e Invoke LySa Tool e Reflect This menu is accessible from the LySa menu item in the menu bar and from the context menu for LySa files in the explorer Lysa files are recognised by the explorer and displayed with the LySa icon The command Invoke LySa will run the LySa tool on the selected file The Support for PEPA allows you to complete the model analysis step by step i e check syntax derive state space and solve model and therefore provides a more elaborate menu The LySa support performs the equivalent steps for the LySa formalism with a single command Thus invoking the LySa tool will perform a syntax check and also analyse the model The Reflect command is used in conjunction with the Reflector for LySa and is described in section 1 7 The support for the LySa formalism offers simple syntax highlighting much th same way that it is provided for PEPA The difference is that no background parsing is provided for LySa and all syntax checking is be performed by the tool itself The editor and default syntax colours can be customised the same way they are customised for PEPA however the settings are located in Tools gt Options gt Editing gt
Download Pdf Manuals
Related Search