Difference between pages "State-Machines and Code Generation" and "UML-B"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Andy
 
 
Line 1: Line 1:
−
= Generating Code from State-Machine Diagrams =
+
Return to [[Rodin Plug-ins]]
−
We have introduced the ability to generate code from state-machine diagrams, in version 0.2.3 of the code generation feature plug-in. Implementation code is generated from the diagram itself, and no additional mark-up of the model is required; that is, nothing over and above the usual mark-up required for Tasking Event-B, such as identifying non-typing/typing invariants, and guards etc. State-machines are created, using the existing state-machine plug-in, subject to the limitations described below.
 
−
== Limitations ==
 
−
The current code generation tool is restricted to generating code for a single Event-B machine, which may contain one or more state-machines. We have yet to explore the decomposition/composition of machines containing state-machines. In principal we should be able to apply decomposition techniques to decompose the single Event-B machine with state-machines into a number of machines, with the state-machines, or the elements of state-machines, distributed between them.
 
  
−
Another limitation is that we do not handle nested state-machines, although this should be feasible.
+
UML-B provides a 'UML-like' graphical front end for Event-B. It provides various diagrammatic modelling notations and editors for creating models which are then translated into Event-B for verification. [[UML-B]] works alongside Event-B allowing the modeller to model in normal Event-B but also contribute some aspects of the model via diagrams.  
  
−
== Translations ==
+
Our [https://www.uml-b.org UML-B] website contains more information about installing UML-B and getting started, as well as our current research and collaborations.
  
−
< Diagram here >
+
UML-B is a collection of diagrammatic editors for Event-B. The diagrams are used to elaborate the machine and its content with extra model features. The diagrams may either by contained within the machine they contribute to, or can be contained in a separate UML-B model file that is linked to the machine.
  
−
The translation of the diagrammatic elements to code has been hard-coded in the code generation plug-in. We have introduced new types to the translator's common language model (IL1). We add case-statements, and a container for them (analogous to ''switch'') since these are commonly used to implement state-machines. The code generator navigates through each state of a state-machine, generating an internal representation of the state-machine, which is used to create the IL1 model. The IL1 model is then used to generate code for the various target languages that may have been implemented. We have also updated the IL1-to-target code generators, to generate case/switch statements in Ada, C and Java.  
+
* [[Image:IUMLB.png]] [[Event-B Statemachines| State-machine diagrams]] a hierarchical state-machine diagram editor which can be used to impose sequential ordering to your events. An animator is also provided to visualise the progress of the state-machine.
  
−
Each state-machine has an Enumerated type whose elements take the names of the states. A state variable is created in the target that keeps track of the current state, and has the type of the enumeration.
+
* [[Image:IUMLB.png]] [[Event-B Classdiagrams| Class diagrams]] a class diagram editor which can be used to define data entities and their relationships and to lift behaviour based on data sets.
  
−
Each state in the state machine is related to a case statement. For instance, the Ada code for the diagram above, is,
+
==Lectures==
  
−
case sm_state is
+
* [[Media:iUML-BClassDiagramsLecture.pdf | UML-B Class-diagrams Lecture]] : Lecture slides on the use of UML-B Class-diagrams
−
when A then <body> ; sm_state := B;
 
−
when B then ...
 
  
−
The <body> translation is determined by the number of outgoing transitions and the guards and actions of the elaborated events. In the event that a state has a single outgoing transition, then the translation is straightforward. The event's action is mapped to a statement in the generated IL1 model. In the event that a state has multiple outgoing transitions, then each outgoing transition of the state gives rise to a branching statement. Each outgoing transition is linked to an event, and the guards of the outgoing transitions must be disjoint and complete. Note that we do not yet generate proof obligations to show this.  
+
* [[Media:iUML-BStatemachinesLecture.pdf | UML-B State-machines Lecture]] : Lecture slides on the use of UML-B State-machines.
  
−
For example, if we have a machine variable v:INT and events ''ab'' and ''ac'' defined as follows:
+
==Tutorials==
  
−
ab = when v < 10 then <a1> end;
+
* [[iUML-B Class-diagrams Tutorial]] : A tutorial on the use of UML-B Class-diagrams.
−
ac = when v >= 10 then <a2> end
 
  
−
Then this is translated to a branching statement, as in the following Ada statement: 
+
* [[iUML-B State-machines Tutorial]] : A tutorial on the use of UML-B State-machines.
  
−
if v < 10 then <a1>
+
==Guidelines==
−
elsif v >= 10 then <a2>
 
−
end if;
 
  
−
== Tooling ==
+
* [[UML-B - Modelling a control system]] : Some guidelines on modelling styles for a control system
 +
 
 +
 
 +
[[Category:User documentation]]
 +
[[Category:UML-B]]
 +
[[Category:Plugin]]

Revision as of 22:09, 30 September 2020

Return to Rodin Plug-ins

UML-B provides a 'UML-like' graphical front end for Event-B. It provides various diagrammatic modelling notations and editors for creating models which are then translated into Event-B for verification. UML-B works alongside Event-B allowing the modeller to model in normal Event-B but also contribute some aspects of the model via diagrams.

Our UML-B website contains more information about installing UML-B and getting started, as well as our current research and collaborations.

UML-B is a collection of diagrammatic editors for Event-B. The diagrams are used to elaborate the machine and its content with extra model features. The diagrams may either by contained within the machine they contribute to, or can be contained in a separate UML-B model file that is linked to the machine.

  • IUMLB.png State-machine diagrams a hierarchical state-machine diagram editor which can be used to impose sequential ordering to your events. An animator is also provided to visualise the progress of the state-machine.
  • IUMLB.png Class diagrams a class diagram editor which can be used to define data entities and their relationships and to lift behaviour based on data sets.

Lectures

Tutorials

Guidelines

Retrieved from ‘https://wiki.event-b.org/index.php?title=State-Machines_and_Code_Generation&oldid=14397’