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>Tommy mNo edit summary |
||
| (4 intermediate revisions by one other user not shown) | |||
| 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 unwieldy proof obligations (a large disjunction in a goal comprising several hundreds of terms). The tool is developed by Newcastle University with 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 the only positive aspect is that this helped to stress-test and debug the proof handling facilities of the Rodin. 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 single most important feature of the new tool version is the introduction of a new form of diagram structuring to prevent the appearance of large proof obligations. The typical source of such proof obligations is demonstrating that an event enables one or more events from 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. 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 a simple atomic event. | |||
=== 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 feature 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. | |||
Latest revision as of 17:36, 3 December 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 unwieldy proof obligations (a large disjunction in a goal comprising several hundreds of terms). The tool is developed by Newcastle University with 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 the only positive aspect is that this helped to stress-test and debug the proof handling facilities of the Rodin. 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 single most important feature of the new tool version is the introduction of a new form of diagram structuring to prevent the appearance of large proof obligations. The typical source of such proof obligations is demonstrating that an event enables one or more events from 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. 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 a simple atomic event.
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 feature 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.
