Difference between pages "Changes to the Mathematical Language of Event-B" and "D32 Code generation"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Laurent
 
imported>Andy
 
Line 1: Line 1:
−
This document describes the evolution of the Event-B mathematical language that will soon take place. The previous version of the language will still be supported.
+
=== Overview ===
  
−
== Generic Identity and Projections ==
+
The code generation activity has been undertaken at the University of Southampton. This has been a new line of work for DEPLOY that was not identified in the original Description of Work for the project. Development of the approach, and the tools to support, it involved a number of team members at Southampton; and also at other institutions. The code generation approach draws on our recent experience with technologies such as ''Shared Event Decomposition'' [[http://wiki.event-b.org/index.php/Event_Model_Decomposition]], and the ''EMF Framework for Event-B'' [[http://wiki.event-b.org/index.php/EMF_framework_for_Event-B]]. There was collaboration at an early stage with Newcastle University, where we explored the commonalities between their work on work-flow [[http://wiki.event-b.org/index.php/Flows]] and the algorithmic structures used in our approach. Collaboration with the University of York was also established since we chose to use their ''Epsilon'' [[http://www.eclipse.org/gmt/epsilon/]] model-to-model transformation technology.
  
−
Three operators were still unary while they could be atomic and generic:
+
=== Motivations ===
−
* the identity relation <math>\id</math>
 
−
* the first projection  <math>\prjone</math>
 
−
* the second projection <math>\prjtwo</math>
 
  
−
These operators are defined as follows in the old version:
+
The decision was taken in 2009 [[http://wiki.event-b.org/index.php/D23_Code_Generation]] to include code generation as a project goal, and to focus our efforts on supporting the generation of code for typical real-time embedded control software. To this end we have developed a multi-tasking approach such as that supported by the Ada tasking model. Individual tasks are treated as sequential programs. These are modelled by an extension to Event-B, called ''Tasking Machines''.  Tasks have mutually exclusive access to state variables through the use of protected resources. The protected resources correspond to Event-B machines. For real-time control, periodic and one-shot activation is currently supported; and it is planned to support aperiodic tasks in the near future. Tasks have priorities to ensure appropriate responsiveness of the control software.
  
−
<math>
+
For the DEPLOY pilots, it was regarded as sufficient to support construction of programs with a fixed number of tasks and a fixed number of shared variables – no dynamic creation of processes or objects has been accommodated. In the past year our goal has been to provide an approach, and tool support, to act as a proof-of-concept. We also gained much practical experience with the development of a code generation framework.  
−
\begin{matrix}
 
−
  E\mapsto F &\in\id(S) && E\in S\;\land\; F = E\\
 
−
  (E\mapsto F)\mapsto G &\in\prjone(r)
 
−
  && E\mapsto F\in r\;\land\; G = E\\
 
−
  (E\mapsto F)\mapsto G &\in\prjtwo(r)
 
−
  && E\mapsto F\in r\;\land\; G = F    .
 
−
\end{matrix}
 
−
</math>
 
  
−
If we drop the parameter, we get
 
−
much more straightforward definitions that capture the essence of the
 
−
operator.  The new definitions are
 
  
−
<math>
 
−
\begin{matrix}
 
−
E\mapsto F &\in\id && E = F\\
 
−
(E\mapsto F)\mapsto G &\in\prjone && E = G\\
 
−
(E\mapsto F)\mapsto G &\in\prjtwo && F = G    .
 
−
\end{matrix}
 
−
</math>
 
  
−
We have the following equivalence between the old
+
This paragraph shall express the motivation for each tool extension and improvement. More precisely, it shall first indicate the state before the work, the encountered difficulties, and shall highlight the requirements (eg. those of industrial partners). Then, it shall summarize how these requirements are addressed and what are the main benefits.
−
and the new versions of the operators
 
  
−
<math>
+
=== Choices / Decisions ===
−
\begin{matrix}
 
−
    \textbf{Old Version} & \textbf{New Version}\\
 
−
    \id(S)  & S\domres id\\
 
−
    \prjone(r) & r\domres\prjone\\
 
−
    \prjtwo(r) & r\domres\prjtwo  .
 
−
\end{matrix}
 
−
</math>
 
  
−
Moreover, in the case where the parameter is not needed, then it can
+
This paragraph shall summarize the decisions (eg. design decisions) and justify them. Thus, it may present the studied solutions, through their main advantages and inconvenients, to legitimate the final choices.
−
be dropped altogether: no domain restriction is needed.  For instance,
 
−
to express that a relation <math>r</math> is irreflexive, one would now write
 
−
<math>r\binter\id = \emptyset</math>.
 
  
−
== Partition ==
+
=== Available Documentation ===
  
−
A new partition predicate is introduced. It is intended to provide an easier way to enter enumerated sets, while getting rid of the <math>\frac{n(n-1)}{2}</math> axioms needed to express pairwise distinctness (or disjointness). The partition operator is defined as follows:
+
This paragraph shall give pointers to the available wiki pages or related publications. This documentation may contain:
  
−
<math>
+
    * Requirements.
−
\begin{array}{ll}
+
    * Pre-studies (states of the art, proposals, discussions).
−
partition(E_0, E_1, \ldots, E_n)\defi &
+
    * Technical details (specifications).
−
  E_0 = E_1\bunion \cdots\bunion E_n \\ &
+
    * Teaching materials (tutorials).
−
  \;\land\; E_1\binter E_2=\emptyset
+
    * User's guides.
−
  \;\land\;\cdots
 
−
  \;\land\; E_{n-1}\binter E_n = \emptyset \\ &
 
−
  (\;\land\; i \ne j \limp E_i \binter E_j = \emptyset ) \\
 
−
\end{array}
 
−
</math>
 
  
 +
A distinction shall be made on the one hand between these different categories, and on the other hand between documentation written for developers and documentation written for end-users.
  
−
where the <math>E_i</math> are expressions bearing the same type.
+
=== Planning ===
  
−
Then, we can enter into a context :
+
This paragraph shall give a timeline and current status (as of 28 Jan 2011).
−
 
 
−
<math>
 
−
  \begin{array}{ll}
 
−
    \mathsf{set}  & S\\
 
−
    \mathsf{constant}  & a_1\\
 
−
    \vdots & \vdots\\
 
−
    \mathsf{constant}  & a_n\\
 
−
    \mathsf{axiom}  & partition(S, \{a_1\}, \ldots, \{a_n\})
 
−
  \end{array}
 
−
</math>
 
−
 
 
−
which is a particular case of a set being defined by listing all its elements.
 
−
 
 
−
== Operator Associativity ==
 
−
 
 
−
Operators used to build sets of relations or functions, viz.
 
−
* relation
 
−
* total relation
 
−
* surjective relation
 
−
* total surjective relation
 
−
* partial function
 
−
* total function
 
−
* partial injection
 
−
* total injection
 
−
* partial surjection
 
−
* total surjection
 
−
* bijection
 
−
 
 
−
have no more relative priorities and loose associativity. Instead, users have to make it explicit by entering parenthesis in formulas.
 

Revision as of 11:48, 1 December 2010

Overview

The code generation activity has been undertaken at the University of Southampton. This has been a new line of work for DEPLOY that was not identified in the original Description of Work for the project. Development of the approach, and the tools to support, it involved a number of team members at Southampton; and also at other institutions. The code generation approach draws on our recent experience with technologies such as Shared Event Decomposition [[1]], and the EMF Framework for Event-B [[2]]. There was collaboration at an early stage with Newcastle University, where we explored the commonalities between their work on work-flow [[3]] and the algorithmic structures used in our approach. Collaboration with the University of York was also established since we chose to use their Epsilon [[4]] model-to-model transformation technology.

Motivations

The decision was taken in 2009 [[5]] to include code generation as a project goal, and to focus our efforts on supporting the generation of code for typical real-time embedded control software. To this end we have developed a multi-tasking approach such as that supported by the Ada tasking model. Individual tasks are treated as sequential programs. These are modelled by an extension to Event-B, called Tasking Machines. Tasks have mutually exclusive access to state variables through the use of protected resources. The protected resources correspond to Event-B machines. For real-time control, periodic and one-shot activation is currently supported; and it is planned to support aperiodic tasks in the near future. Tasks have priorities to ensure appropriate responsiveness of the control software.

For the DEPLOY pilots, it was regarded as sufficient to support construction of programs with a fixed number of tasks and a fixed number of shared variables – no dynamic creation of processes or objects has been accommodated. In the past year our goal has been to provide an approach, and tool support, to act as a proof-of-concept. We also gained much practical experience with the development of a code generation framework.


This paragraph shall express the motivation for each tool extension and improvement. More precisely, it shall first indicate the state before the work, the encountered difficulties, and shall highlight the requirements (eg. those of industrial partners). Then, it shall summarize how these requirements are addressed and what are the main benefits.

Choices / Decisions

This paragraph shall summarize the decisions (eg. design decisions) and justify them. Thus, it may present the studied solutions, through their main advantages and inconvenients, to legitimate the final choices.

Available Documentation

This paragraph shall give pointers to the available wiki pages or related publications. This documentation may contain: 

   * Requirements.
   * Pre-studies (states of the art, proposals, discussions).
   * Technical details (specifications).
   * Teaching materials (tutorials).
   * User's guides.

A distinction shall be made on the one hand between these different categories, and on the other hand between documentation written for developers and documentation written for end-users.

Planning

This paragraph shall give a timeline and current status (as of 28 Jan 2011).

Retrieved from ‘https://wiki.event-b.org/index.php?title=Changes_to_the_Mathematical_Language_of_Event-B&oldid=2188’