Difference between pages "Rodin Developer Support" and "UML-B"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Nicolas
 
m (move content of iUML-B page to this one)
 
Line 1: Line 1:
−
The Developer Support provides resources for developing plug-ins for the Rodin Platform.
+
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.
  
−
== Rodin Platform Overview ==
+
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.
  
−
== Architecture of the Rodin Platform ==
+
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.
  
−
=== Rodin Platform Core ===
+
* [[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.
  
−
* [[Database]]
+
* [[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.
  
−
* [[Builder]]
+
==Lectures==
  
−
=== Event-B User Interface ===
+
* [[Media:iUML-BClassDiagramsLecture.pdf | iUML-B Class-diagrams Lecture]] : Lecture slides on the use of iUML-B Class-diagrams
  
−
The Event-B User Interface of the Roding Platform has two major components that are concerned with either [[Modelling User Interface|modelling]] in Event-B or [[Proving User Interface|proving]] properties of models.
+
* [[Media:iUML-BStatemachinesLecture.pdf | iUML-B State-machines Lecture]] : Lecture slides on the use of iUML-B State-machines.
  
−
* [[Modelling User Interface]]
+
==Tutorials==
  
−
* [[Proving User Interface]]
+
* [[iUML-B Class-diagrams Tutorial]] : A tutorial on the use of iUML-B Class-diagrams.
  
−
=== Event-B Component Library ===
+
* [[iUML-B State-machines Tutorial]] : A tutorial on the use of iUML-B State-machines.
  
−
Event-B models and all proof-related information are stored in the Rodin database. The syntax of the mathematical notation, that is, expressions, predicates, and assignments, are maintained in an [[Abstract Syntax Tree|abstract syntax tree]]. Abstract syntax trees are manipulated by means of a class library that can be used independently of Eclipse. They are saved in the database in human-readable form as Unicode character strings. Event-B constructs, such as contexts and machines, are not represented as abstract syntax trees. They are stored and retrieved directly from the database (by contrast, mathematical formulas need additional parsing). Well-formedness of Event-B constructs is verified by a [[Static Checker|static checker]]. The static checker has two main purposes: (1) it generates error messages for ill-formed constructs, and (2) it filters well-formed parts of components to be subjected to proof obligation generation. The [[Proof Obligation Generator|proof obligation generator]] uses those parts of constructs that are well-formed and generates proof obligations from them. Finally, the [[Proof Manager|proof manager]] attempts to prove proof obligations and maintains existing proofs associated with proof obligations. The proof manager works automatically and interactively. When new proof obligations have been generated it attempts to discharge them automatically. If it does not succeed, it permits interactive proof (by means of the [[Proving User Interface|proving user interface]]).
+
==Guidelines==
  
−
* [[Abstract Syntax Tree]]
+
* [[iUML-B Modelling a control system]] : Some guidelines on modelling styles for a control system
  
−
* [[Static Checker]]
 
  
−
* [[Proof Obligation Generator]]
+
[[Category:User documentation]]
−
 
+
[[Category:UML-B]]
−
* [[Proof Manager]]
+
[[Category:Plugin]]
−
 
 
−
== Extending Rodin ==
 
−
 
 
−
* [[Getting Started]]
 
−
 
 
−
* [[Plug-in Tutorial]]
 
−
 
 
−
* [[Extending the project explorer]]
 
−
 
 
−
* [[Extending the Proof Manager]]
 
−
 
 
−
* [[Extending the Index Manager]]
 
−
 
 
−
== Useful Hints ==
 
−
 
 
−
=== Testing ===
 
−
 
 
−
=== Debugging ===
 
−
 
 
−
=== Publishing ===
 
−
 
 
−
A Plug-in developed for the Rodin Platform will normally consist of a collection of eclipse 'plugin' projects and a single eclipse 'feature' project. The feature project contains branding information such as logo's icons and licensing details. It is also used to identify your Plug-in so that users can install it. To build your Plug-in use an eclipse 'site' project. This will build the jar files for your plugin projects and a jar for your feature. See eclipse documentation for more details.
 
−
 
 
−
Now you need to make your Plug-in available for users to install via the Main Rodin Update site (which comes built-in to the Rodin platform).
 
−
 
 
−
First upload your jar files onto the Sourceforge uploads area and then create a new release in the FRS (Admin-file releases). Note that you should include a zip of the complete source projects to comply with Sourceforge rules. You must not repeat files that have not changed. Sourceforge does not allow you to upload multiple copies of the same jar file. The Feature jar will take care of unchanged plugin jars and use the existing links. Only new jars should be included in a particular release.
 
−
See here for details:- http://alexandria.wiki.sourceforge.net/File+Release+System+-+Offering+Files+for+Download
 
−
 
 
−
Finally, the update site must be updated to redirect the update requests to the files on the FRS.
 
−
(Currently this is done by Colin Snook on request - see Rodin developers page for contact details).
 
−
 
 
−
[[Details for Maintaining Main Rodin Update Site]]
 
−
 
 
−
== Rodin Developer FAQ ==
 
−
 
 
−
[[Category:Developer documentation]]
 
−
[[Category:Rodin Platform]]
 

Revision as of 21:53, 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=Rodin_Developer_Support&oldid=14392’