Flows Plug-in: Difference between revisions
imported>Alexili m New page: === Overview === The flows plug-in allows a modeller to define event ordering constraints using a visual notation. Its main purpose is to give a clean and concise view of model control fl... |
imported>Alexili No edit summary |
||
| Line 1: | Line 1: | ||
=== Overview === | |||
Event-B, being an event systems formalism does not have a mechanism for explicitly defining event ordering. Although event guards may express any desired event ordering, the ability to have a summary of possible event flows in a concise and compact form is useful for many tasks, for example, code generation and connecting with other formalisms. The Flows plug-in addresses one aspect of event ordering: it allows a modeller to specify and prove that a given sequence of events does not contradict a given machine specification. More precisely, if we were to execute a machine step-by-step following our prescribed sequence of events we would not discover divergencies and deadlocks not already present in the original machine. In other words, the constraining of event ordering must be such that the overall specification is an Event-B refinement of the original model. Importantly, this means that all the desired model properties proved before are preserved. | |||
The main purpose of the Flows plug-in is to give a modeller a clean and concise view of the control flow aspects of a model without cluttering the model with program counter variables and associated guards and actions. The plug-in is essentially a graphical notation for formulating certain kind of theorems. The new version is to be released in February 2011 and this will include facilities for expressing a wider range of enabledness properties as well as tools for describing event refinement. It is going to address one of the critical shortcomings of the previous version: generation of extremely proof obligations (a large disjunction in a goal comprising several hundreds of terms). The tools is developed by Newcastle University following the requirements and suggestions from Bosch and SAP. | |||
The | |||
=== Motivations === | === Motivations === | ||
The tool was applied by Bosch in the development of the cruise control model to verify deadlock-freedom and liveness properties of the model. Being a sizable case-study, this was an important test for the ideas and techniques behind the plug-in. The general conclusion was that a tool of this kind is essential and the current version should be improved in many directions. This experience has uncovered a rather fundamental issues with the size and complexity of the generated proof obligations. These were the largest theorems ever generated in Rodin and some core platform issues were uncovered as the result. It was clear that such proof obligations can never be comfortably handled by Rodin tools (although there were some encouraging results in the application of ProB as a disprover for these kind of proofs) and it was decided that the approach to proof generation requires a complete redesign. | |||
=== Choices / Decisions === | === Choices / Decisions === | ||
The new tool version introducing new forms of diagram structuring primitives to prevent the appearance of very large proof obligations. The typical source of such a proof obligation is demonstrating that an event enables one or more of a long list of events. Technically, the proof would state that the after-state of the event implies the disjunction of the guards of the next events. We apply the divide and conquer principle. To prevent the appearance of such a disjunction a modeller is encouraged to split the list into a set of sub-models. Each sub-model has a pre- and post-conditions and there are proof obligations demonstrating that all the entry events of the sub-model are enabled when the precondition is satisfied and, symmetrically, every exit event satisfies the sub-model post-condition. Externally, a sub-model appears to be an event with an the precondition as a guard and the postcondition as the set of actions. Although it is more work now for a modeller to produce a flow diagram the extra effort should pay off at the proving stage. | |||
=== Available Documentation === | === Available Documentation === | ||
* An extensive example of the application of the flows in the modelling (the old version) is available to the Deploy Project members as a part of the Bosch cruise control case study. | |||
* There is a wiki page describing the core proof obligations generated by the tool - [[Flows]] | |||
* Tutorial slides available from the project file share | |||
* | |||
* | |||
=== Planning === | === Planning === | ||
The plan is to gather feedback from the users within the Project and encourage the external users to try out the plug-in and provide feedback and future requests. There are many ideas on the tool extension, in particular using the tool to document event refinement (split, merge, group, refinement diagrams) and provide mechanised patterns for some of the more important cases. | |||
Revision as of 18:58, 29 November 2010
Overview
Event-B, being an event systems formalism does not have a mechanism for explicitly defining event ordering. Although event guards may express any desired event ordering, the ability to have a summary of possible event flows in a concise and compact form is useful for many tasks, for example, code generation and connecting with other formalisms. The Flows plug-in addresses one aspect of event ordering: it allows a modeller to specify and prove that a given sequence of events does not contradict a given machine specification. More precisely, if we were to execute a machine step-by-step following our prescribed sequence of events we would not discover divergencies and deadlocks not already present in the original machine. In other words, the constraining of event ordering must be such that the overall specification is an Event-B refinement of the original model. Importantly, this means that all the desired model properties proved before are preserved.
The main purpose of the Flows plug-in is to give a modeller a clean and concise view of the control flow aspects of a model without cluttering the model with program counter variables and associated guards and actions. The plug-in is essentially a graphical notation for formulating certain kind of theorems. The new version is to be released in February 2011 and this will include facilities for expressing a wider range of enabledness properties as well as tools for describing event refinement. It is going to address one of the critical shortcomings of the previous version: generation of extremely proof obligations (a large disjunction in a goal comprising several hundreds of terms). The tools is developed by Newcastle University following the requirements and suggestions from Bosch and SAP.
Motivations
The tool was applied by Bosch in the development of the cruise control model to verify deadlock-freedom and liveness properties of the model. Being a sizable case-study, this was an important test for the ideas and techniques behind the plug-in. The general conclusion was that a tool of this kind is essential and the current version should be improved in many directions. This experience has uncovered a rather fundamental issues with the size and complexity of the generated proof obligations. These were the largest theorems ever generated in Rodin and some core platform issues were uncovered as the result. It was clear that such proof obligations can never be comfortably handled by Rodin tools (although there were some encouraging results in the application of ProB as a disprover for these kind of proofs) and it was decided that the approach to proof generation requires a complete redesign.
Choices / Decisions
The new tool version introducing new forms of diagram structuring primitives to prevent the appearance of very large proof obligations. The typical source of such a proof obligation is demonstrating that an event enables one or more of a long list of events. Technically, the proof would state that the after-state of the event implies the disjunction of the guards of the next events. We apply the divide and conquer principle. To prevent the appearance of such a disjunction a modeller is encouraged to split the list into a set of sub-models. Each sub-model has a pre- and post-conditions and there are proof obligations demonstrating that all the entry events of the sub-model are enabled when the precondition is satisfied and, symmetrically, every exit event satisfies the sub-model post-condition. Externally, a sub-model appears to be an event with an the precondition as a guard and the postcondition as the set of actions. Although it is more work now for a modeller to produce a flow diagram the extra effort should pay off at the proving stage.
Available Documentation
- An extensive example of the application of the flows in the modelling (the old version) is available to the Deploy Project members as a part of the Bosch cruise control case study.
- There is a wiki page describing the core proof obligations generated by the tool - Flows
- Tutorial slides available from the project file share
Planning
The plan is to gather feedback from the users within the Project and encourage the external users to try out the plug-in and provide feedback and future requests. There are many ideas on the tool extension, in particular using the tool to document event refinement (split, merge, group, refinement diagrams) and provide mechanised patterns for some of the more important cases.
