Get the user manual - School of Computer Science
Contents
1. amp Model Explorer amp EEEE Y stationaryobstacles v gt ra lt Package Import gt UML Primitive Types Es gt cS System SystemDynamics gt Object Robot gt gt gt Object Obstacle System CollisionAvoidance gt collisionAvoidance_robot_1 gt collisionAvoidance_obstacle_1 gt 2 RobotConstraints EB v n Outline X E r stationaryobstacles di X lt 2 Palette gt Kaa gt g Nodes vr 0 M rs Activity Partit kdeterministicAssignment deterministicAssignment knondeterministicAssignment e Initial nod Brake Coast Sense 7 Constraint 2 B_r Abs 0 gt v_rA2 2 A_r Output Pi 2 B_r Abs y y_0 gt v_rA2 2 A_r 3 Expansi f deterministicAssignmel raat cana Curve amp Broadcast Signal r 0 Action Edge knondeterministicAssignment 4 Control Flow Acc A Bu Exception Handler B_r lt ar amp ar lt Ar Vv o iz StationaryObstacles Eg StationaryObstacles Fr Controller X Properties Model Validation EJ Console X x Hybrid Simulation Proof Library Java JavaVirtualM Formula equals x_r a a g NFF equals x_r x r4 gt Start t Prune Proof BY Reus 30 Object Flow Y Link KeYmaera Prover e Ta TE i Der vir dx_r a M eoo Proof closed Hybrid Strategy x_r vir dx_r2. 2 S al and left th 8 6 al and left 3 Vs Del 7 al and left We might have changed the original HYPO Loop_inv_box_quan PROVABLE inv lt e ho amp vA 2 27T KRY Strategy Applied 49 rules 56 1 sec closed 9 goals 0 remaining h v t h v t Figure 5 3 The KeYmaera console PROOF COLLABORATION Abstract This chapter introduces the proof collaboration features of Spnx Spnx uses Eclipse for model and proof versioning and is thus compatible with common versioning systems such as SVN and GIT Contents 6 1 Share and Collaborate on Textual Models 23 6 2 Share and Collaborate on a Proof 23 6 3 Export Open Goals of Partial Proofs 24 6 4 Import Geometric Relevance Filtering Results 25 6 1 SHARE AND COLLABORATE ON TEXTUAL MOD ELS Textual models in d just as ordinary source code can be versioned in a source code repository Differences between versions updates deletions and conflicts can be compared and resolved using the standard Eclipse tools EP Compare 04c 1 1_robot_2D DynamicWindow key 589 and 575 X g K Text Compare 4 AA K 04c 1 1_robot_2D DynamicWindow key 589 K 04c 1 1_robot_2D DynamicWindow key 575 27 R cy rotation center y 28 R cy rotation center y 28 Rr radius of curvature 29 Ror radius of curvature 29 R ox position of obstacle 0 R ox position of obstacle R oy 31 R oy R odx
3. Appearance Advanced 5 Model associations between your classes as appropriate Currently these are for documentation purposes only and do not influence code generation 6 Select Constraint from the palette to define conditions that must always be true In the bouncing ball example we add constraints on gravity must be strictly positive the damping coefficient must be positive and less than 1 time must be positive and the initial height of the ball must be positive The popup editor for constraints in d supports syntax highlighting and code completion You can confirm the constraint by pressing Ctrl Enter or leave the popup editor with Esc a 7 Constraint N DataType BallConstraints A ___ dL H gt 0 amp d DurationObse FE Enumeration a as Edges nuva system object World Ball constante c Real 1 h Real 1 t Real 1 v Real 1 constant g Real 1 H Real 1 i i i E InterfaceReali 7 Link E Ez Packagelmport 9 PackageMerge E E 0 lt g9 amp 0 lt ckc lt 1 0 lt t bo Ex Dynamics Ep Structure 2 CATA Ai Problems Javadoc 2 Declaration El Y Yen 12 WorldConstraints gt JE E UML Name WorldCo _ Jli lt gt Profile Visibility public TW arance anne Context lt Undefined gt a me Specification xl O lt g O lt cc lt 10 lt t iP Fi Ei Advanced Constraine
4. direction and linear velocity of obstacle 32 R odx direction and linear velocity of obstacle m R ody 3 R ody R t time 34 Rt time 4 5 6 problem 37 schemaVariables v gt 38 term R trm amp Abs x ox gt vA2 2 b v V b 9 amp Abs y oy gt vA2 2 b v V b 10 8r gt 0 t1 rules amp dx 2 dy 2 1 42 absolute amp A gt 0 43 find CAbs trm amp b gt 4 Wreplacewith MifCtrm gt 0 then trm else trm amp V gt 0 5 heuristics beta if comment then not used autor amp Om gt te Es 8ep gt 0 17 gt C control obstacle 8 odx 49 ody 50 probLlem odxA2 odyA2 lt VA2 51 v gt 0 8 Abs x ox gt vA2 2 b v V b brake or remain stopped on your current curvatur 53 8 Abs y oy gt vA2 2 b v V b la h 54 RrsA E Properties El Console ErrorLog g Progress History X og et Ev Tp aja a trunk robix models map2d 04c 1 1_robot_2D DynamicWindow key in https cvs concert cs cmu edu multigoali Revision Y Date Author Comment 589 1 31 13 5 28 PM smitsch Update to work with KeYmaera 3 1 575 1 30 13 8 20 PM smitsch Models and proofs with simpler invariants and preconditions Action Affected paths 4 Description Figure 6 1 Comparison of textual models 6 2 SHARE AND COLLABORATE ON A PROOF Just as for textual models Spnx supports any source code repository con nected to Ecli
5. Hide right Select All Deselect All O U lt ack GENE Cancel Finish Figure 6 7 Select 5 Select the applicable goals usually all and click Finish applicable goals 860060 Goal selection Select where to apply the geometric relevance filtering result Applicable open goals W g gt 0 h gt 0 t gt 0 O lt c c lt 1 vA2 lt 2 g H hil select All Deselect All lt Back Next gt _ Cancel Gin Commit the changes to the source code repository or load the partial proof in KeYmaera to continue proving BIBLIOGRAPHY 1 M TschH S GHORBAL K AND PLATZER A On provably safe obstacle avoidance for autonomous robotic ground vehicles In Robotics Science and Systems 2013 2 Mrrscu S Loos S M AND PLATZER A Towards formal verification of freeway traffic control In ICCPS 2012 IEEE pp 171 180 3 Mirscu S PASSMORE G O AND PLATZER A A vision of collaborative verification driven engineering of hybrid systems In Do Form 2013 M Kerber C Lange and C Rowat Eds AISB pp 8 17 21
6. a_r m Ignoring t lt ep Proof Ignoring v_r gt 0 Proof E Ignoring t gt Ignoring dx_r A 2 c E Proof Tree Ignoring v_r 0 4 Replacements are t Formula equals y_r NFF equals y_r y_r_1 x_r vir dx_r ani x_r vir dx_r a_r F 2 ind loop invariant E Invariant Initially Valic H Misi Use Case E Body Preserves Invariant aS Property proved Statistics Nodes 859 Branches 67 ok K stationaryobstacles key X Xproblem vir gt 0 8 2 B_r Abs x_r x_0 gt v_rA2 2 B_r Abs y_r amp dx_rA2 dy_rA2 1 amp rl 0 8 Ar gt 08Br gt 08 ep gt 0 1 MC BEGIN Controller C v_r 0 7 Coast 2y a r Re 0 Sense xo B 5 ES 2 B_r Abs x_r x_0 gt v_rA2 2 A_r 2 B_r AbsCy_r y_o gt v_rA2 2 A_r Curve r l 0 B_r lt ar amp a_r lt A_r a NS w Sill o a o N a r B r END Controller ResetClock cu ME Ex EE t Se ri KRY Integrated Deductive Software Design Ready Figure 1 1 Screenshot of the Spnx toolkit Details on the underlying principles of Spnx can be found in 3 Spnx was used in formal verification case studies on road traffic safety 2 and obstacle avoidance for autonomous robotic ground vehicles 1 INSTALLATION Abstract This chapter introduces the installation procedure of Spnx and the subsequent con
7. H h H gt 0 gt forall R v_1 forall R h_1 forall Rt Y Body Preserves Invariant g gt 0 h gt 0 t gt 0 0 lt c c lt 1 v42 lt 2 g H h H gt 0 gt forall R v_0 forall R h_0 forall Rt lt Back Next gt Cancel Finish 6 4 IMPORT GEOMETRIC RELEVANCE FILTERING RESULTS 4 Select or create a new file to export click Finish 80 8 Create Open Goal File Create a new Open Goal File The selected goal will be exported into this file Enter or select the parent folder sphinxtutorial src proof A eS sphinxtutorial bin 2 META INF 2 src 2 model gt proof gt src gen File name Advanced gt gt soas came mana lt Back 6 4 IMPORT GEOMETRIC RELEVANCE FILTERING RE SULTS 1 Open the context menu of a proof and click Import 2 Select Sphinx Geometric Relevance Filtering Result 3 Select a file from the file system or from the Eclipse workspace 4 Select the hiding suggestions to import into the proof usually all and click Next 25 Figure 6 5 Select or create a new file to export 26 PROOF COLLABORATION Figure 6 6 Select hiding suggestions e00 Geometric relevance filtering Select geometric relevance filtering result O from pe A From workspace sphinxtutorial src proof invariant grf Browse Hide left Y t gt 0 i Select All Y O lt c Mc lt Deselect All gt
8. UML Package Diagram H UML Sequence Diagram ta UML StateMachine Diagram _ 2 UML UseCase Diagram You can load a template WI A UML model with basic primitive types ModelWithBasicTypes _ Remember current selection x Back Next gt Cancel Figure 4 1 Create a new graphical model of a hybrid system describing structure and behavior C Finish 11 12 GRAPHICAL MODELING 6 Click Finish The editor pane now shows the graphical editor Switch to the class di agram structure and follow the steps below to apply the UML profile for d 1 In the Properties View select the tab Profile and click the button Apply Registered Profile 2 Select Differential Dynamic Logic Structure and Differential Dynamic Logic Behavior and click OK 3 Check dldynamic and dlstatic and click OK 4 2 MODEL SYSTEM STRUCTURE In this section we discuss how to model the system structure with classes and properties We will use the stereotypes of the d UML profile to mark important parts of the model for code generation and subsequent verification 1 From the palette select Class and click on the editing area Alternatively wait for the popup palette to appear in an empty part of the editing area We create two classes one represents the bouncing ball the other Figure 4 2 Create one the world new classes by 1 600 Java sphinxtutorial src model bouncingball
9. behavior Overview of bouncing ball dynamics Add a new activity diagram Discrete dynamics of the bouncing ball example Create a new hyperlink Set a default hyperlink 0 cunas a amp aras Transform a UML model into a textual d model Inspect simulated traces of hybrid programs Run KeYmaera from the context menu of any key or LOO Hee Ener ap The KeYmaera console Comparison of textual models Prost comparison ia or OP ew ee Export an arithmetic goal Search an open goal EXPORT 00 ts 2 do Sevag Ae a Soe Boke a Select hiding suggestions Select applicable goals si a ste eee a h VDO OOO CON OV A Rh A Re RR RR RR RR RB RR RR o ONN N NV VS A BWW N m NO 21 OVERVIEW 1 1 GENERAL INFORMATION his document is a user manual for the Spnx verification driven engineer ing environment for hybrid systems Spnx is an extensible verification driven engineering toolkit based on the Eclipse platform It provides textual and graphical modeling editors to describe the structure the discrete dy namics and the continuous dynamics of cyber physical systems Spnx uses KeYmaera as hybrid verification tool ES Project Explorer X eBle 7 Y jmathincs gt proofs gt sre gen gt temp Y J stationaryobstacles KY key notation 2 uml
10. di Eclipse Users smitsch Downloads eclipse workspace A dragging Class rae OF SEB ted or rre NO Oar BO elements from the AE a uc Grande Mar Ar dr FQ Quick Access j ES ava palette to the editing j a cc rue sd area Kr Rae EE model S 3 bou ag Sone Beeeag AA a Sono cingi di K bouncingball key bouncingball no 2 On the properties view select the profile element Use System to flag the main system class and Object to flag other agents in the system 3 From the palette select Property and click on a class to add a new prop erty We add three properties to the class World a clock t a damping coefficient c and gravity g 4 On the properties view you can apply stereotypes Constant or Variable to these properties to flag them as either being constant or variable By default all properties are variable Alternatively you can use the UML tab to set a property read only or use the popup editor to add readOnly 4 3 MODEL SYSTEM DYNAMICS World h Real 1 j c PrimitiveTypes Real readOnly L3 Dynamics B Structure E Problems Javadoc Declaration EJ Console Properties 53 Ez lied stereotypes LL lt ae gg UML iii typ E Profile gt Constant from distatic
11. does nothing 1 In the Model Editor view add a New Activity Diagram to the Discret eDynamics behavior created above using the context menu v verity BOUNCING Bar J Validation gt Y New SysML Child gt L4 Export e ey Import gt B Outline Model Explor New Child gt a BE New Diagram gt Createanew Activity Diagram VE Model E New Table gt Sa Create a new Class Diagram de lt Package Import gt U Delete 9 Create a new Communication Diagram jpe eran ED Rename p2 Create a new Component Diagram gt t_ ownedRule 2 Create a new Composite Structure Diagram Y t ownedBehavior 1 Undo 36Z 4 Create a new Deployment Diagram Redo 32 E Create a new Package Diagram f cama Cut eX ET Create a new Sequence Diagram gt t edge 6 Copy 38C a Create a new StateMachine Diagram gt L node 6 Paste 38 V g Create a new UseCase Diagram e O wAhiart Ball Enable write 2 Add an Initial Node to denote the start of the discrete dynamics 3 Connect the initial node to a decision node This is the start of the if condition 4 Add an Opaque Action to set the new velocity and another one to reset time Tag both with the stereotype Deterministic Assignment to define that they will set the value of variables in a deterministic manner Click the label of the action and set the values of velocity v c v and time t 0 Figure 4 13 Use the context menu to add a new activity diagram to a UML behavi
12. hyperlinks Document hyperlinks Web hyperlinks Defaults HyperLinks Hyperlink diagram with Heuristic Hyperlinks Default Hyperlinks by double click E DiscreteDynamics DiscreteDynamics Ok Cancel 4 4 GENERATE TEXTUAL MODEL 4 4 GENERATE TEXTUAL MODEL 1 Open the context menu of bouncingball uml in the package explorer 2 Click Acceleo Model to Text Generate DifferentialDynamicLogic HE Package Explorer 53 v2 sphinxtutorial w amp src Y E model 7 bouncingball di K bouncingball key B bouncingball notal Y bouncingball um E Task List 3 e ASE Find b All b Ver Y Uncategorized 7 Verify Bouncing Ball Outline E Model Explorer Sh os ES gt t ownedRule 2 Y t ownedBehavior 1 E Diagram Discr Y t edge 6 gt ControlFlow gt A ControlFlow b Z ControlFlow b 7 ControlFlow gt 7 ControlFlow gt Z ControlFlow bouncingball uml sphinxtutorial s m bouncingball di 3 New gt Open F3 Open With gt Show In NEW gt Int E Copy C 5 E Copy Qualified Name 2 Paste V Delete DD tnt t Show Filtered Children Alt click 2 Remove from Context XE Mark as Landmark 081 Build Path gt Refactor XET gt 21 Import 14 Export Refresh F5 creteDynamics 3 Assign Working Sets Run As gt laration El Console E Properties 53 Debug As gt o Team gt Compare With gt false Replac
13. key ext jars recoderKey jar Browse Log4J JAR Applications KeYmaera3 1 key ext jars log4j jar Browse JLink JAR Applications KeYmaera3 1 key ext jars JLink jar Browse Restore Defaults Apply Cancel OKs 4 If necessary supply the remaining JAR libraries manually using the respective Browse buttons 2 2 2 Configure the Editors Click Eclipse gt Preferences to open the Eclipse preferences dialog 1 Select DifferentialDynamicLogic gt Compiler to activate deactivate IAIEX code generation and configure output directory and further code gen eration settings 1 http symbolaris com info KeYmaera html download 2 2 CONFIGURATION 5 2 Select DifferentialDynamicLogic Syntax Coloring to change the color ing of terminal symbols comments and other syntactical elements of d 3 Select DifferentialDynamicLogic Templates to change the existing tem plates or add new ones see Sect 2 2 5 for details 4 Select DifferentialDynamicLogic Refactoring to change the default refactoring settings 5 Select Papyrus Embedded Editors to set the Spnx included d editors as default popup editors for the UML elements Constraint OpaqueAction and ControlFlow Figure 2 2 Set the gt d editors of Spnx 600 Preferences p as embedded popu type filter text Embedded Editors Drew p p p tmr Compare editors for Papyrus P EMF Facet Elements to edit Help org eclipse uml2 uml Tra
14. APHY o ONN ABU HS A AWW A A N N N NN NNN BRR RR J A UY G QW N BR RO WN pa A N N LU LIST OF FIGURES Figure 1 1 Figure 2 1 Figure 2 2 Figure 2 3 Figure 3 1 Figure 3 2 Figure 3 3 Figure 3 4 Figure 3 5 Figure 3 6 Figure 4 1 Figure 4 2 Figure 4 3 Figure 4 4 Figure 4 5 Figure 4 6 Figure 4 7 Figure 4 8 Figure 4 9 Figure 4 10 Figure 4 11 Figure 4 12 Figure 4 13 Figure 4 14 Figure 4 15 Figure 4 16 Figure 4 17 Figure 5 1 Figure 5 2 Figure 5 3 Figure 6 1 Figure 6 2 Figure 6 3 Figure 6 4 Figure 6 5 Figure 6 6 Figure 6 7 Screenshot of the Spnx toolkit KeYmaera configuration o Configure d popup editors Configure hybrid program simulation Create a new d project o Open the quick outline Syntax checkine 24 us says be eee Code completion 2 i482 se dea Eode told ac aaa Sr nn a ak an Quick peek into folded code Create a new UML model Crealo a ew ClaSS a pe tia a wre Flag properties as constant or variable Define constraints using the d popup editor Add a new constralMt o o Select the constrained element Specify a constraint as OpaqueExpression Enter d as constraint specification language Use d to specify a constraint body Use d to specify the continuous dynamics Hierarchically decompose
15. ELING Hybrid model of a bouncing ball functions Rc damping coefficient Rg gravity R H x initial height programVariables state variable declarations x R A Y t problem 4 initial state characterization g gt 0 amp h gt 0 t gt 0 O lt c amp c lt 1 amp v 2 lt 2xgx H h H gt 0 gt MI system dynamics h v v g t 1 h gt 0 falling jumping if t gt 0 h 0 then if on ground V i C V bounce back t 0 fa x repeat transitions Xx O lt h h lt H safety postconditionx REFACTOR YOUR MODEL Spnx has preliminary model refactoring support in the form of variable renaming Proofs are not yet adapted automatically 1 Right click a variable select Refactor Rename FURTHER EDITOR FEATURES e Double click any tab to make it full screen e Open a searchable quick outline of your textual model from the context menu of a d textual model J gt programVariables state variahle declarations Rh v Ev 2 WIE bouncingball problem Y I2 Problem 5 vwE gt g gt 0 h v ER gt YI E NL VIZ lt W A 1h w if wi dL Modality Y Box Modality a a Y Z Statlmpl A 1 Y Starimpl Y StatReent JN i tReen rylmpl Press Esc to exit the quick outline Spnx checks the syntax of hybrid programs for correctness and indi cates syntax errors with an
16. STEFAN MITSCH MODELING AND ANALYZING HYBRID SYSTEMS WITH SPHINX A USER MANUAL Computer Science Department Carnegie Mellon University Johannes Kepler University http www cs cmu edu smitsch December 2013 Stefan Mitsch Modeling and Analyzing Hybrid Systems with Sphinx A User Manual O December 2013 WEBSITE http www cs cmu edu smitsch E MAIL smitsch cs cmu edu CONTENTS I OVERVIEW 1 1 General Information 2 INSTALLATION 2 1 Installation from Eclipse Update Site 2 2 Configuration sisa s a Way od 2 2 1 Install and Configure KeYmaera 2 2 2 Configure the Editors 2 2 3 Configure Mathematica and Hybrid Program Simulation 2 2 4 Show Additional Views 2 2 5 Add Modeling Templates 3 TEXTUAL MODELING 3 1 Create anew Project 3 2 Refactor your Model 3 3 Further Editor Features 4 GRAPHICAL MODELING 4 1 Create a new Graphical Model 4 2 Model System Structure 4 3 Model System Dynamics 4 4 Generate Textual Model 5 HYBRID SYSTEM ANALYSIS 5 1 Plot Simulated Traces of Hybrid Programs 5 2 Verify a Model with KeYmaera 6 PROOF COLLABORATION 6 1 Share and Collaborate on Textual Models 6 2 Share and Collaborate on a Proof 6 3 Export Open Goals of Partial Proofs 6 4 Import Geometric Relevance Filtering Results BIBLIOGR
17. ces to configure how hybrid program simulation handles nondeterministic choice nondeter ministic repetition and nondeterministic assignment when simulating your models Note that in the current version Spnx makes those choices in a randomized fashion which means that you may have to simulate multiple times to develop an intuition about possible execution behav ior of your program 6 INSTALLATION Figure 2 3 Set the Preferences 000 number of loop type filter text unrollings the Fun Benug maximum time spent A gt DIProofLink per loop execution gt and bounds for als Local Installation d b Mathematica Setup random numoer gt Proof Term generation de Hybrid Program Simulation Preferences Edit Hybrid Program Simulation Settings Unroll loop Maximum time per loop Minimum random numbers for simulation 10 0 Maximum random numbers for simulation 10 0 Y Print Mathematica input to console Pr v 10 6 Restore Defaults Apply Cancel ok 2 2 4 Show Additional Views Click Window Show View Other then select the following views e Select General Properties e Select Papyrus Model Explorer e Select Spnx Hybrid Simulation 2 2 5 Add Modeling Templates TEXTUAL MODELING Abstract This chapter introduces the textual modeling features of Spnx These include project creation wizard loading d models to KeYmaera model refactoring syntax checking c
18. d element t a oP rd 4 3 MODEL SYSTEM DYNAMICS Now that we defined the structure of our system we can define its dis crete and continuous dynamics Since system dynamics can become rather complicated we will model hierarchically We start with the overall system dynamics and will supply details in sub diagrams As cautious modelers we first define a safety condition before we model any behavior 1 Define the safety condition select the tab UML of the properties view and scroll to the precondition and postcondition section Click the button on the postcondition to open the postcondition window and add a new Constraint 13 Figure 4 3 Flag properties as constant or variable using stereotypes setting readonly to true false on the UML tab of the properties view or apply readOnly with the popup editor Figure 4 4 Define constraints using the d popup editor 14 Figure 4 5 Add a new constraint as postcondition for a UML activity Figure 4 6 Select the constrained element Figure 4 7 Specify the constraint using a new OpaqueExpression GRAPHICAL MODELING 80980 Postcondition gt o m 3 Ge amp DurationConstraint InteractionConstraint IntervalConstraint TimeConstraint Cancel OK 2 On the constraint definition window name the constraint and option ally select the constrained element In our example of the bouncing ball the safety condi
19. de and the merge node with a Control Flow The default condition for such a flow is true which means that it is executed unconditionally The condition can be hidden using Filter gt Manage Connector Labels from the context menu of the control flow 4 Add an OpaqueAction from the palette and connect the merge node with a control flow to the opaque action This action represents the continuous dynamics of our system On the properties view choose a descriptive name for the action e g Fall and Jump and add the stereotype Dynamics on the properties view The opaque action 15 Figure 4 8 Enter d as constraint specification language Figure 4 9 Specify the constraint body in d and confirm your definition by clicking outside the text field 16 GRAPHICAL MODELING represents the continuous dynamics in our system Click the Fall and Jump label to open the d popup editor and define the dynamics Figure 4 10 Define using a differential algebraic equation the continuous dynamics of a hybrid system as true differential algebraic equation in the d popup editor of an OpaqueAction with stereotype Dynamics dynamics h v v g t 1 h gt 0 5 Add a Behavior Call Action from the palette Although the discrete dynamics of the bouncing ball example is rather simple we want to have a separate activity diagram to demonstrate decomposition We Figure 4 11 Use Call create a new behavior named Discr
20. e With gt true Ei n March 22 2 amp Discovery gt false 3 Paste V Users smit bouncingba Properties 36l sphinxtute 15 082 byt 7 Refactor Model gt Ej Generate DifferentialDynamicLogic Acceleo Model to Text Figure 4 17 Click Acceleo Model to Text Generate DifferentialDynam icLogic to generate a textual d model from a graphical UML model HYBRID SYSTEM ANALYSIS Abstract This chapter introduces the analysis features of Spnx Cor rectness properties about hybrid programs can be formally verified in KeYmaera In order to develop an intuition about the actual behavior of a hybrid program Spnx additionally simulates hybrid programs using Mathematica and displays the traces of variable valuations Contents 5 1 Plot Simulated Traces of Hybrid Programs 21 5 2 Verify a Model with KeYmaera 0 22 5 14 PLOT SIMULATED TRACES OF HYBRID PROGRAMS Spnx uses Mathematica to create simulated traces of hybrid programs The simulation traces are displayed in the simulation view which can be activated by clicking Window Show View Other Spnx Hybrid Simulation You can create a simulation run for the model in the active editor by pressing the gears icon in the simulation view The context menu on the simulation plot lets you select the displayed variables scale and zoom the plot save a bitmap image or print the simulation trace K bouncingball key X H 1 Hyb
21. entation of the model 9 Figure 3 3 Syntax and cross references are checked on the fly Figure 3 4 Get cross references to variables and other code completion help by pressing Ctrl Space Figure 3 5 Use code folding Figure 3 6 Hover the mouse over a folded code snippet to take a quick peek GRAPHICAL MODELING Abstract This chapter introduces the graphical modeling features of Spnx Spnx uses UML class diagrams to model the structure of a hybrid system and UML activity diagrams to model their behavior Graphical models can be transformed into textual d models and then loaded to KeYmaera Contents 4 1 Create a new Graphical Model 4 3 Model System Dynamics CREATE A NEW GRAPHICAL MODEL Click File gt New Other Select Papyrus Model and click Next Enter the name of your new model and click Next Select uML and click Next 4 2 Model System Structure 2 222222 4 4 Generate Textual Model 2 2 2 2 2m nn nennen Select UML Activity Diagram system dynamics and UML Class Diagram system structure then check A UML model with basic primitive types en Initialization information New Papyrus Model Select name and kind of the diagram Diagram Name BouncingBall Select a Diagram Kind M Ez UML Activity Diagram cal By UML Class Diagram er a UML Communication Diagram UML Component Diagram Ed UML Composite Structure Diagram _ Y UML Deployment Diagram Pa
22. eteDynamics Behavior Actions to decompose the 8090 dynamics and create Create a new Call Behavior Action new Behavior nodes Create a new Behavior 7 Create behavior Behavior type Activity gt Behavior Name DiscreteDynamics Element owner lt lt System gt gt lt Activity gt SystemDynamics ce Or assign an existing one Select behavior Behavior Synchronous call 2 Fn FT 2 Cancel mon 6 Add a Decision Node from the palette This node represents the end of the loop body 7 Connect the decision node with the merge node using a Control Flow as back edge Select the stereotype Nondeterministic repetition for this control flow Then specify a loop invariant for the stereotype 8 Add an Activity Final Node and connect the decision node with a control flow This finalizes the overall system dynamics as follows 4 3 MODEL SYSTEM DYNAMICS 1 Figure 4 12 bouncingball di 3 Overview of bouncing ball dynamics PreCondition Init PostCondition Height bounceback Discretebynsnies hz Dynamics 33 B Structure In the next step we will specify the discrete dynamics of the system The discrete dynamics of the bouncing ball is rather simple if the ball hits the ground it bounces back i e the discrete dynamics inverts the ball s velocity and reduces it according to the damping factor else it just keeps falling or jumping i e the discrete dynamics
23. figuration steps to setup KeYmaera as hybrid verification tool Contents 2 2 4 Show Additional Views 2 2 5 Add Modeling Templates o 2 1 Installation from Eclipse Update Site 3 22 Configuration amaba ra ss 4 2 2 1 Install and Configure KeYmaera 4 2 2 2 Conheure the Editors si rana OS ee ee 4 22 3 Configure Mathematica and Hybrid Program Simulation 5 6 6 2 1 INSTALLATION FROM ECLIPSE UPDATE SITE nx comes with an Eclipse update site which automates installation and updates It assumes that Eclipse Kepler Modeling Tools is already downloaded from http ww eclipse org and installed 1 Start Eclipse 2 Click Help Install Modeling Components to open the modeling compo nent selection wizard 3 Select Xtext and Papyrus and click Finish Follow the on screen instruc tions to install these modeling components 4 Click Help Install new Software to open the Eclipse update manager 5 Click Add to add a new Spnx update site and type the following into the location of the update site http www cs cmu edu smitsch updates releases to use the latest tool release 6 Click Add to add a new Xsemantics update site and type the following into the location of the update site http master dl sourceforge net project xsemantics updates releases 1 3 7 If you want to compare proofs a Click Add to add a new EMF Compare update site b Type the f
24. ht gt Rule hide left gt Rule random_ass_box_right gt Rule hide left gt Builtin Update Simplification gt Rule hide left gt Rule all_right gt Rule hide_left gt 4 Rule modality_split_right gt Rule random_ass_box_right gt Rule random_ass_box_right gt 4 Builtin Update Simplification gt 4 Builtin Update Simplification gt Rule all_right gt Rule all_right Open Goal wut 5 07 Ax Lhe dyed ie 1 ED Open Goal v_1 gt 0 dx_1 A 2 dy_1 2 1 r_1 gt 0 Differences Properties j Differences Properties i 4 Use the buttons in the structural differences view header to copy changes between versions 0 3 EXPORT OPEN GOALS OF PARTIAL PROOFS 1 Open the context menu of a proof and click Export Figure 6 3 Export an 2 Select Sphinx Export Arithmetic Goal and click Next arithmetic goal via 600 Export the export wizard ey Select an export destination type filter text Run Debug Export Arithmetic Goal gt amp Tasks gt 2 Team gt XML gt Other lt Back Next gt Cancel Finish Figure 6 4 Search an 3 Search for and select the open goal to export click Next open goal Select goal Select an open goal to export type filter text Y Invariant Initially Valid g gt O0 h gt 0 t gt 0 0 lt c c lt 1 vA2 lt 2 g H h H gt 0 gt h gt O08vVA2 lt 2 g H h Y Use Case g gt 0 h gt 0 t gt 0 0 lt c c lt 1 v42 lt 2 g
25. k the button next to language to add d Type dL into the text 3 MODEL SYSTEM DYNAMICS field on the left side and add it by clicking the right pointing arrow 600 Language Java Natural language gt Add selected elements Finn LS oF Es canei NOK 3 Click into the body field and provide the constraint specification in d In our example we want the ball s height to be between o and its initial height H Click somewhere outside the body field e g reselect the name field to adopt the new body specification 600 Create a new OpaqueExpression Name Valid Height f Bod Language 8J Le LB Z x dL O lt h 4 h lt H Visibility public y Behavior lt Undefined gt S Type lt Undefined gt UML Profile D Cancel oa 4 Exit the constraint specification window the constraint window and the postcondition window by clicking OK on each Next we define the overall system dynamics These consist of the con tinuous dynamics the ball falls and jumps and discrete dynamics when it hits the ground the ball bounces back We want the ball fall and jump arbitrariliy often Thus discrete and continuous dynamics are repeated non deterministically many times in a loop 1 Add an Initial Node from the palette This node represents the start of our system 2 Add a Merge Node from the palette This node represents the loop start 3 Connect the initial no
26. light bulb exclamation mark icon in the left editor bound and a red wiggly line 3 3 FURTHER EDITOR FEATURES F initial state characterization g gt 0 amp h gt 0 amp t gt 0 amp B lt c amp cel amp v 2 lt 2 g CH h amp H gt 0 f amp undefinedVariable gt e Code completion problem initial state characterization g gt 0 amp h gt 9 t gt 9 Be c amp cel amp vA2 lt 2 g H h H gt 0 XL 2 namics Ea umping t und l ck IZ gt SF Y Z lt gt ansitions E istcondition IE A e Keep overview with Code Folding using in vertical editor bar Ki bouncingball key 53 an Hybrid model of a bouncing ball functions programVariables problem e Quick peek folded content as tooltip in vertical editor bar KY bouncingball key 53 fee Hybrid model of a bouncing ball functions programVaribbles amp problem initial state characterization g gt 0 amp h gt 0 amp t gt 9 amp O lt c amp cel amp vA2 lt 2 g H h amp H gt 9 gt ME system dynamics h v v g t 1 h gt 0 falling jumping if t gt 0 amp h 0 then if on ground v i c v bounce back t Fi PL repeat transitions 0 lt h amp h lt H safety postcondition e Whenever you save a d textual model Spnx generates a K IEX repre s
27. n directory Spnx will try to figure out Fi Speci the lib d denci tomaticall igure 2 1 Specify e library dependencies automatically K Y 8609 Preferences J type filter text KeYmaera Local Installation Br row libraries to enable General a gt Ant it KeYmaera Settings KeYm a era st artu CDO KeYmaera installation directory Applications KeYmaera3 1 Browse p P gt Ecore Tools Diagram GE EMF Compare bital E 3 licati k bial B from S p nx gt EMF Facet Orbital Extensions JAR Applications KeYmaera3 1 key ext jars orbital ext jar Browse PHelp gt Install Update Scala Library JAR Applications KeYmaera3 1 key ext jars scala library jar Browse _ H P Java gt Model Validation Orbital Core JAR Applications KeYmaera3 1 key ext jars orbital core jar ir Browse MoDisco i gt Mylyn KeYmaera JAR Applications KeYmaera3 1 key ext jars keymaera jar Browse POCL Zaren gt Papyrus JMath Plot JAR Applications KeYmaera3 1 key ext jars jmathplot jar Browse gt Plug in Development em me gt Proof f z gt Run Debug Commons Compress JAR Applications KeYmaera3 1 key ext jars commons compress 1 4 jar Browse Sphinx gt DifferentialDynamicLogic Java CC JAR Applications KeYmaera3 1 key ext jars javacc jar Browse gt Key KeYmaera Local Installati ANTLR JAR Applications KeYmaera3 1 key ext jars antlr 3 4 complete jar Browse Term P Team RecoderKEY JAR Applications KeYmaera3 1
28. nsition UML models Install Update org eclipse uml2 uml State gt Java OS org eclipse uml2 uml Port gt Model Validation org eclipse uml2 uml Property MoDisco org eclipse papyrus uml profile structure AppliedStereotypeProperty Mylyn org eclipse uml2 uml Constraint POCL org eclipse uml2 uml OpaqueAction Y Papyrus i org eclipse uml2 uml CollaborationUse Connection Tools org eclipse uml2 uml ControlFlow gt Diagrams org eclipse uml2 uml Parameter Drag and drop org eclipse uml2 uml ConnectionPointReference gt Embedded Editors Model loading Navigation Associated editor Papyrus Model Explorer Essential OCL constraint editor Default Pathmaps JAVA constraint l Printing Property view customizal Property views an ll Cancel o Differential Dynamic Logic Default Editor Simple Direct Editor 2 2 3 Configure Mathematica and Hybrid Program Simulation 1 Select Spnx Mathematica Setup to let Spnx access your local Mathe matica installation e On MacOS a typical Mathematica link is similar to Applications Mathematica app Contents Mac0S MathKernel mathlink includ ing the quotation marks e On Unix Linux use math mathlink e On Windows use a link similar to c program files wolfram research mathematica 9 0 mathkernel exe including the quotation marks For debugging purposes Spnx logs Mathematica output to the console if activated 2 Select Spnx Hybrid Program Simulation Preferen
29. ode completion outline and quick outline as well as code folding Contents 31 Createa new Projet es iras aan ee hea ricsi 3 2 Refactor your Model lt a se ss essre rare nera 3 3 Further Editor Features 3 1 CREATE A NEW PROJECT 1 Click File New Other 2 Select Differential Dynamic Logic Project and click Next 600 New Select a wizard Wizards N type filter text gt Git Java b Java Emitter Templates MoDisco Papyrus Plug in Development Y Sphinx KRY Differential Dynamic Logic File 4 Differential Dynamic Logic Project P SVN Tasks User Assistance Other b Examples mn TT lt Back Next gt Jj Cancel 3 Enter the name of your new project and click Finish The project creation wizard creates a new project with a sample key file that shows the principal structure of a theorem in d including a hybrid program Details on d can be found on the KeYmaera web site including tutorials and cheat sheets Below we give a of a bouncing ball Listing 3 1 Hybrid model of the bouncing ball example in d 1 http symbolaris com info KeYmaera html download Finish Figure 3 1 Create a new d project using the new project wizard Figure 3 2 Open the quick outline using Ctrl O Windows Unix or Cmd O Mac Co m VD CON BD VW A W N m m 12 13 14 15 16 17 18 19 20 21 22 23 24 TEXTUAL MOD
30. ollowing into the location of the update site http download eclipse org modeling emf compare updates releases 8 If you want to install the simulation features of Spnx a Click Add to add a new Wolfram Workbench update site Spnx installation retrieves the Mathematica integration libraries from this update site Note you need a Mathematica license to use the hybrid program simulation features of Spnx Type the following To check for Spnx updates click Help Check for Updates 4 INSTALLATION into the location of the update site http workbench wolf ram com update b Click Add to add a new Eclipse Indigo compatibility update site for Wolfram Workbench and type the following into the location of the update site http download eclipse org releases indigo 9 Select Spnx from the drop down menu and choose the features to install 10 Follow the screen instructions to complete the installation 2 2 CONFIGURATION his section details the configuration of Spnx once it is installed Spnx uses KeYmaera as hybrid verification tool 2 2 1 Install and Configure KeYmaera 1 Follow the instructions on the KeYmaera web site to download and install KeYmaera locally Note that Spnx does not yet work with the Webstart version 2 Click Eclipse Preferences and select KeYmaera Local Installation from the tree view 3 Click Browse on the KeYmaera Installation Directory line and select your local KeYmaera installatio
31. or 18 Figure 4 14 The discrete dynamics of the bouncing ball example Figure 4 15 Create a new hyperlink Figure 4 16 Set a hyperlink as default action for double click on a diagram element GRAPHICAL MODELING 5 Add a Merge Node an Activity Final Node and set the control flows to get the final dynamics as below bouncingball di 23 DiscreteDynamics edeterministicAssignment Bounce Back deterministicAssignment Reset Time i Dynamics BA Structure y DiscreteDynamics 28 l 6 To set up navigation from the dynamics overview to the detailed discrete dynamics switch back to the tab Dynamics 7 Double click the behavior call action bounceback DiscreteDynamics to open the hyperlink configuration window 8 Click the button on the tab View Hyperlinks to open the Edit Hyperlink Window 9 Click the button Search and select the DiscreteDynamics activity dia yaris El Editors list Tree View i type filter text t re Dynamics B Structure q ts DiscreteDynamics F View hyperlinks Document hyperlinks Web hyperlinks Defa L List of View hyperlinks OK Cancel 600 Edit Hyperlink View a Tooltip text dm Use default 1 Cancel J ir ok Jj Cancel 10 Switch to the tab Default Hyperlinks select the DiscreteDynamics hyper link and press the right arrow button to add it as default 00 HyperLink View
32. pse to version proofs You can compare changes between your 23 24 PROOF COLLABORATION local version of a proof and the latest version in the source code repository as follows 1 Open the context menu of a proof and click Compare with Latest from Repository 2 Click Complete resource set s Figure 6 2 Proof 3 Browse the proof comparison comparison rJ PassiveSafety2 di an Compare PassiveSafetyPartial key proof lt workspace gt and versions X B Structural differences ly Spy E Y 13 change s in Branch Body Preserves Invariant v 1 change s in Open Goal v_1 gt 0 dx_1 42 dy_1 42 1 r1 gt 0 v1 0 Abs x_1 ox_1 gt VW_IA2 2 b V v_1 l sea Attribute goal EString in Open Goal v_1 gt 0 dx_1 2 dy 1 42 1 r1 gt 0 v1 0 Abs x_1 ox_1 gt v_ A2 2 k gt Rule modality_split_right has been added gt Rule random_ass_box_right has been added o gt Builtin Update Simplification has been added g Rule all_right has been added B Visualization of Structural Differences v a E LD Workspace file PassiveSafetyPartial key proof Repository file PassiveSafetyPartial key proof vw rue anyit gt Rule all_right gt Rule imp_right gt Rule and_left gt Rule and_left gt Rule and_left Rule and_left gt Rule hide_left gt Rule hide_left gt Rule hide_left gt Rule hide_left Rule hide_left Rule hide_left gt Rule modality_split_rig
33. rid bouncing ball example h height v velocity H height limit g gravitation c elastic dampening factor at floor h 0 provable w gt functions R C g H V gt programVariables 14 Rh V5 Es 15 6 Xproblem g gt 08 h gt 08 VA2 lt 2 g H h amp H gt 0 amp c 4 5 gt C fh v v g h gt 0 C h 0 v c v h gt 0 invariant vA2 lt 2 g H h amp h gt 0 J lt h amp h lt H Y Tasks Ej History Progress E Console 9 Error Log Properties C Proof 27 Search e Hybrid Simulation X 2040 0 75 0 50 0 25 0 00 0 25 0 50 0 75 1 00 0 00 0 25 0 50 0 75 1 00 1 25 1 50 1 75 2 00 2 25 2 50 2 75 3 00 3 25 3 50 3 75 4 00 4 25 4 50 4 75 5 00 5 25 5 50 5 75 6 00 6 25 6 50 t h v Figure 5 1 Inspect simulated traces of hybrid programs 21 22 HYBRID SYSTEM ANALYSIS 5 2 VERIFY A MODEL WITH KEYMAERA Spnx uses KeYmaera to prove correctness properties about models in d You can start KeYmaera from the context menu of a key or key proof file in the package explorer or from the context menu of a textual editor oh Fi Hybrid model of a bouncina ball hi Undo 8 Z zi ga Revert File R g Save 36S R H Quick Outline 0 AprogramVa Open Declaration F3 sta O With gt Rh v pen Wit Show In XW S problem fe il Cut oh X g gt 8 Copy 38C CH h amp H gt 0 gt AL Paste 3V mic
34. s i l Validate f bing i Rename Element XR yy Content Assist Space _ Toggle Comment 36 by Format QEF sitions ca Quick Fix 81 condition Shift Right Shift Left Find References TEG Run As gt 52 1 KeYmaera Proof Local Debug As gt Team gt Run Configurations r Prohlems Comnare With gt rries 57 Figure 5 2 Run KeYmaera from the context menu of any key or proof file S nx will start KeYmaera as external application and show KeYmaera s information output in a console view If absolutely necessary you can stop KeYmaera from the console using the red stop button not encouraged Note that this will force quit KeYmaera without saving your work Problems Javadoc Declaration El Console 23 ES Properties Ex BEE PRE mo JLibrary Java JavaVirtualMachines jdk1 7 0_1 KeYmaera Prover Found CE HYPO loop_inv_box_quan DISPROVABLE P gt Start Prune Proof Reuse wm E inve vA2 lt _ 2 g CHE Tasks hy Inner Node HYPO Loop_inv_box_quan i 2 ren Env with no model 1 v s2 g H h a 00 Proof closed Hybrid Stra h v t Property proved We might have changed the original Proof d Said CEX Counterexample mi Proot Iree S Er Found CE 1 gt r imply right lt Nodes 57 HYPO loop_inv_box_quan DISPROVABLE 2 al and left Branches 9 Eee 3 al and left HYPO loop_inv_box_quan 4 al and left Cox inve h gt 08vA2 lt
35. tion will demand that the ball s height is positive but no larger than its starting height thus we constrain h en Constrained element type filter text Ez h ES Model E lt Package Import gt UML Primiti a ve e SystemDynamics Q Y t ownedAttribute 3 m PEY ails gt Ez H gt H System World i Cancel EB 3 Exit the constrained element selection the constraint definition win dow and the postcondition window A new postcondition without specification has been added to the activity 4 Click on the postcondition to open the d popup editor Enter the postcondition and confirm with Ctrl Enter As an alternative to the popup editor constraint specifications can be added from the constraint editor continue from step 2 above 1 Add a constraint specification using the button next to the specifica tion text field Specifications are always of kind OpaqueExpression Create a new Constraint eoo Name Height y Visibility public Duration DurationInterval Expression InstanceValue Interval LiteralBoolean Literallnteger LiteralNull LiteralReal LiteralString LiteralUnlimited Natural OpaqueExpression StringExpression TimeExpression Timelnterval Context Specific es lt Undefined gt e a FR i Constrained element Ez h UML Profile e Software released under the GNU GPL License 2 On the constraint specification window name the new specification Clic
Download Pdf Manuals
Related Search