ºÝºÝߣ

ºÝºÝߣShare a Scribd company logo

Emulink: A graphical modelling environment for PVS

?
?
E
edge7

Emulink is graphical tool that allows software engineers to create PVS specifications starting from a StateCharts based diagram.

1 of 24
Download to read offline
Emulink: a modelling graphical environment for PVS Candidate: Enrico D'Urso Supervisors: Prof. Cinzia Bernardeschi; Prof. Andrea Domenici In collaboration with Queen Mary University Of London
Outline ¡ñ Motivation ¡ñ Development of Emulink ¨C The graphical modelling language (Emucharts) ¨C Model visualisation and animation ¡ñ Case study ¨C Demonstration of a software design error in a commercial medical device
Motivation (1) Software: first failure cause of computing systems ¨C 10-200 faults / KLOC created during development 0.01-10 faults / KLOC residual ? Proof ? Model-checking ? Testing
Motivation (2) Safety cannot rely only on testing. Testing shows the presence, not the absence of bugs. ( Edsger Wybe Dijkstra ) International safety standards such as IEC 61508 highly recommend the use of formal methods in the development of safety critical or safety related components Verification based on formal methods tools can significantly reduce the number of design errors
Motivation (3) Formal methods tools have a steep learning curve ¨C Specialized mathematically based modelling languages ¨C Complex analysis techniques ¨C Not yet mature for widespread use in industry Several manufacturers do not use formal verification tools routinely despite of the potential advantages ¨C As a consequence, design errors are usually identified too late in the design process, or even after system deployment
The focus of this thesis ¡ñ Develop a graphical tool to simplify the use of PVS, a state-of-the-art formal verification tool ¡ñ PVS (Prototype Verification System) ¨C Part of the NASA Langley Verification Tools ¨C Extensive libraries of mathematical theories
PVS language Purely declarative logical language (system: set of functions) HA : THEORY BEGIN x,y : VAR bool HA(x,y) : [bool, bool] = ((x AND y) , % carry (x XOR y)) % sum % convert Boolean to natural b2n(x) : nat = IF x THEN 1 ELSE 0 ENDIF HA_corr : THEOREM % correctness LET (carry, sum) = HA(x, y) IN b2n(sum) + 2*b2n(carry) = b2n(x) + b2n(y) END HA
The intuition Software engineers are familiar with graphical modelling languages such as Statecharts. PVS specifications would be more accessible if they were presented using a graphical language similar to Statecharts
Statecharts: an example
Emulink: a graphical modelling environment for PVS Graphical modelling tool for emulating statecharts in PVS: ¨C Emucharts (essential subset of Statechart constructs) ¨C Automatic generation of PVS models ¨C Animation of PVS models during simulations (useful when debugging PVS models) ¨C Visualisation of existing annotated PVS models
Emucharts editor
Constructs currently supported ¡ñ StatesStates ¡ñ Transition ¡ñ Self transition ¡ñ Default transition ¡ñ Transition Condition ¡ñ Transition Action
Constructs currently supported ¡ñ States ¡ñ TransitionTransition ¡ñ Self transition ¡ñ Default transition ¡ñ Transition Condition ¡ñ Transition Action
Constructs currently supported ¡ñ States ¡ñ Transition ¡ñ Self transitionSelf transition ¡ñ Default transition ¡ñ Transition Condition ¡ñ Transition Action
Constructs currently supported ¡ñ States ¡ñ Transition ¡ñ Self transition ¡ñ Default transitionDefault transition ¡ñ Transition Condition ¡ñ Transition Action
Constructs currently supported ¡ñ States ¡ñ Transition ¡ñ Self transition ¡ñ Default transition ¡ñ Transition ConditionTransition Condition ¡ñ Transition Action
Constructs currently supported ¡ñ States ¡ñ Transition ¡ñ Self transition ¡ñ Default transition ¡ñ Transition Condition ¡ñ Transition ActionTransition Action
Interface simulation PVSio is an extension that enables PVS specifications to be executed
Emulink: Emucharts animation During the simulation the diagram is animated, highlighting states and transitions
Case study Infusion pumps are devices in use in hospitals to deliver medications or nutrients to patients at controlled rates and precise volumes Safety requirement: No over- or under-treatment
Modelling and simulation of the device Device Source Code Emulink Model PVS specification Device interface animation PVSio
A critical interface failure User types 102.3 units Pump inoculates 1023 units without any warning For doses above 100 units:
Emulink helps pinpoint the design fault
Conclusions A graphical tool has been developed to semplify the adoption of formal methods in software development. The utility of the tool has been demonstrated using a case study based on a real medical device. Emulink is part of PVSio-web, a graphical frontend for the PVS formal verification tool. Future work: Extension of the statecharts subset notation supported; Use of the tool in different domains.

More Related Content

Emulink: A graphical modelling environment for PVS

  • 1. Emulink: a modelling graphical environment for PVS Candidate: Enrico D'Urso Supervisors: Prof. Cinzia Bernardeschi; Prof. Andrea Domenici In collaboration with Queen Mary University Of London
  • 2. Outline ¡ñ Motivation ¡ñ Development of Emulink ¨C The graphical modelling language (Emucharts) ¨C Model visualisation and animation ¡ñ Case study ¨C Demonstration of a software design error in a commercial medical device
  • 3. Motivation (1) Software: first failure cause of computing systems ¨C 10-200 faults / KLOC created during development 0.01-10 faults / KLOC residual ? Proof ? Model-checking ? Testing
  • 4. Motivation (2) Safety cannot rely only on testing. Testing shows the presence, not the absence of bugs. ( Edsger Wybe Dijkstra ) International safety standards such as IEC 61508 highly recommend the use of formal methods in the development of safety critical or safety related components Verification based on formal methods tools can significantly reduce the number of design errors
  • 5. Motivation (3) Formal methods tools have a steep learning curve ¨C Specialized mathematically based modelling languages ¨C Complex analysis techniques ¨C Not yet mature for widespread use in industry Several manufacturers do not use formal verification tools routinely despite of the potential advantages ¨C As a consequence, design errors are usually identified too late in the design process, or even after system deployment
  • 6. The focus of this thesis ¡ñ Develop a graphical tool to simplify the use of PVS, a state-of-the-art formal verification tool ¡ñ PVS (Prototype Verification System) ¨C Part of the NASA Langley Verification Tools ¨C Extensive libraries of mathematical theories
  • 7. PVS language Purely declarative logical language (system: set of functions) HA : THEORY BEGIN x,y : VAR bool HA(x,y) : [bool, bool] = ((x AND y) , % carry (x XOR y)) % sum % convert Boolean to natural b2n(x) : nat = IF x THEN 1 ELSE 0 ENDIF HA_corr : THEOREM % correctness LET (carry, sum) = HA(x, y) IN b2n(sum) + 2*b2n(carry) = b2n(x) + b2n(y) END HA
  • 8. The intuition Software engineers are familiar with graphical modelling languages such as Statecharts. PVS specifications would be more accessible if they were presented using a graphical language similar to Statecharts
  • 10. Emulink: a graphical modelling environment for PVS Graphical modelling tool for emulating statecharts in PVS: ¨C Emucharts (essential subset of Statechart constructs) ¨C Automatic generation of PVS models ¨C Animation of PVS models during simulations (useful when debugging PVS models) ¨C Visualisation of existing annotated PVS models
  • 12. Constructs currently supported ¡ñ StatesStates ¡ñ Transition ¡ñ Self transition ¡ñ Default transition ¡ñ Transition Condition ¡ñ Transition Action
  • 13. Constructs currently supported ¡ñ States ¡ñ TransitionTransition ¡ñ Self transition ¡ñ Default transition ¡ñ Transition Condition ¡ñ Transition Action
  • 14. Constructs currently supported ¡ñ States ¡ñ Transition ¡ñ Self transitionSelf transition ¡ñ Default transition ¡ñ Transition Condition ¡ñ Transition Action
  • 15. Constructs currently supported ¡ñ States ¡ñ Transition ¡ñ Self transition ¡ñ Default transitionDefault transition ¡ñ Transition Condition ¡ñ Transition Action
  • 16. Constructs currently supported ¡ñ States ¡ñ Transition ¡ñ Self transition ¡ñ Default transition ¡ñ Transition ConditionTransition Condition ¡ñ Transition Action
  • 17. Constructs currently supported ¡ñ States ¡ñ Transition ¡ñ Self transition ¡ñ Default transition ¡ñ Transition Condition ¡ñ Transition ActionTransition Action
  • 18. Interface simulation PVSio is an extension that enables PVS specifications to be executed
  • 19. Emulink: Emucharts animation During the simulation the diagram is animated, highlighting states and transitions
  • 20. Case study Infusion pumps are devices in use in hospitals to deliver medications or nutrients to patients at controlled rates and precise volumes Safety requirement: No over- or under-treatment
  • 21. Modelling and simulation of the device Device Source Code Emulink Model PVS specification Device interface animation PVSio
  • 22. A critical interface failure User types 102.3 units Pump inoculates 1023 units without any warning For doses above 100 units:
  • 23. Emulink helps pinpoint the design fault
  • 24. Conclusions A graphical tool has been developed to semplify the adoption of formal methods in software development. The utility of the tool has been demonstrated using a case study based on a real medical device. Emulink is part of PVSio-web, a graphical frontend for the PVS formal verification tool. Future work: Extension of the statecharts subset notation supported; Use of the tool in different domains.