Difference between revisions of "Event Model Decomposition"
imported>Pascal |
imported>Pascal m (→Specification) |
||
Line 26: | Line 26: | ||
* Configuring the decomposition | * Configuring the decomposition | ||
− | ** | + | ** Identifying the machine to be decomposed |
− | ** | + | ** Identifying the sub-machines to be created |
− | ** | + | ** Specifying how to perform the decomposition (event partition) |
− | ** | + | ** Asking for simplifications |
* Performing the decomposition | * Performing the decomposition | ||
** Generating the sub-machines | ** Generating the sub-machines | ||
Line 41: | Line 41: | ||
==== About the events ==== | ==== About the events ==== | ||
− | * Identifying an event as external. | + | * Identifying an event as external |
− | * Generating an external event. | + | * Generating an external event |
− | * Defining an external event as an abstraction of an event of the non-decomposed model that modifies the considered shared variables | + | ** Generating an external event where the action is deterministic |
− | * Ensuring that an external event cannot be refined | + | ''eg.'' <math>x,y := x + z,y - x</math> |
+ | ** Generating an external event where the action is non-deterministic | ||
+ | ''eg.'' <math>x,y :| x' > y \land y' > x' + z</math> or <math>x :\in A \lor {y}</math> | ||
+ | * Defining an external event as an abstraction of an event of the non-decomposed model that modifies the considered shared variables | ||
+ | * Ensuring that an external event cannot be refined | ||
==== About the variables ==== | ==== About the variables ==== | ||
− | * Identifying a variable as shared | + | * Identifying a variable as shared |
− | * Ensuring that a shared variable is always present in the state space of any refinement of the component (a shared variable cannot be data-refined) | + | * Ensuring that a shared variable is always present in the state space of any refinement of the component (a shared variable cannot be data-refined) |
* Replicating a shared variable in the sub-components of the decomposition | * Replicating a shared variable in the sub-components of the decomposition | ||
Revision as of 12:42, 12 June 2009
Introduction
One of the most important feature of the Event-B approach is the ability to introduce new events during refinement steps, but a consequence is an increasing complexity of the refinement process when having to deal with many events and many state variables.
The main idea of the decomposition is to cut a model into sub-models
, which can be refined separately and more confortably than the whole.
The constraint that shall be satisfied by the decomposition is that these refined models might - the recomposition will never be performed in practice - be recomposed into a whole model in a way that guarantees that
refines
. An event-based decomposition of a model is detailed in Event Model Decomposition: the events of a model are partitioned to form the events of the sub-models. In parallel, the variables on which these events act are distributed among the sub-models.
The purpose is here to precisely describe what is required at the Rodin platform level to integrate this event model decomposition, and to explain why. The details of how it could be implemented are out of scope.
Terminology
- Event model decomposition: The decomposition of a model, as defined in the modelling language, in sub-models.
A model can contain contexts, machines, or both. The events are contained in the machines, as well as the variables on which they act, the invariants constraining these variables, and optionnally the variants. The notion of model decomposition is then an extrapolation for the notion of machine decomposition.
- Shared variable: A variable of a given model which is accessed (read/written) by several distinct events.
- External event: An event of a sub-model simulating the way the read (but not written) variables of a sub-model are handled in the initial model.
Architecture
Specification
High-level requirements
- Configuring the decomposition
- Identifying the machine to be decomposed
- Identifying the sub-machines to be created
- Specifying how to perform the decomposition (event partition)
- Asking for simplifications
- Performing the decomposition
- Generating the sub-machines
- Generating the sub-contexts
- Generating the useful proof obligations
- Not "propagating" useless proof obligations
- Checking the decomposition
Low-level requirements
About the events
- Identifying an event as external
- Generating an external event
- Generating an external event where the action is deterministic
eg.
- Generating an external event where the action is non-deterministic
eg. or
- Defining an external event as an abstraction of an event of the non-decomposed model that modifies the considered shared variables
- Ensuring that an external event cannot be refined
About the variables
- Identifying a variable as shared
- Ensuring that a shared variable is always present in the state space of any refinement of the component (a shared variable cannot be data-refined)
- Replicating a shared variable in the sub-components of the decomposition
About the invariants
- Copying an invariant dealing with the private variables of a sub-component in the sub-component
- Copying an invariant involving a shared variable only in the sub-components where this variable is shared
- Not copying an invariant related to private and shared variables (?)
About the variants
About the contexts
- Linking the sub-contexts
Bibliography
- J.R. Abrial, Mathematical Models for Refinement and Decomposition, in The Event-B Book, to be published in 2009 (lien externe).
- J.R. Abrial, Event Model Decomposition, Version 1.3, April 2009.
- M. Butler, Decomposition Structures for Event-B, in Integrated Formal Methods iFM2009, Springer, LNCS 5423, 2009 (lien externe).