Difference between pages "Rodin Plug-ins" and "UML-B"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Rivera
(→‎Code Generation: added EventB2SQL)
 
 
Line 1: Line 1:
−
''For developer support, see [[Rodin Developer Support]]''
+
Return to [[Rodin Plug-ins]]
  
−
== Rodin Plug-in Documentation ==
+
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.
  
−
=== Modelling ===
+
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.
−
* [[Text Editor]] augments the standard structured editor of Rodin with a text editor.
 
−
* [[Rodin Editor]] augments the standard structured editor of Rodin with a structured text based editor.
 
−
* [[Records_Extension|Records]] provide structured types for Event-B.
 
−
* [[UML-B]] provides a 'UML-like' graphical front end for Event-B.
 
−
* [[Parallel Composition using Event-B]] allows the composition of machines through events for Event-B.
 
−
* [[Decomposition Plug-in User Guide|Decomposition Plug-in]] allows the decomposition of Event-B machines/contexts (shared variables (A-style) and shared events decomposition (B-style))
 
−
* [[Refactoring Framework]] allows the refactoring of elements that are part of file (and also on related files).
 
−
* [[Rose (Structured) Editor]] a model structured editor.
 
−
* [[Flows]] plug-in allows the addition of control flow to a machine.
 
−
* [[Image:Mlogo_big.png|40px]] [[Modularisation Plug-in]] provides a mechanism for constructing and proving modular developments.
 
−
* [[Mode/FT Views]] plug-in brings modelling of modal and fault tolerance features.
 
−
* [[Team-based development]] enables Event-B models to be stored in a shared repository (e.g. SVN).
 
−
* [[Event-B Qualitative Probability User Guide | Qualitative Probability]] provides supports for reasoning about termination with probability 1 (almost-certain termination).
 
  
−
=== Animation ===
+
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.
−
* [[Image:prob_logo_small.png|16px]] [[ProB]] is an animator and model checker for the B-Method,
 
−
* [[Image:AnimB.png|50px]] [[AnimB]] is an animator for the Rodin platform,
 
−
* [[UML-B - Statemachine Animation]] provides an animation (using Pro-B) of UML-B State-machines,
 
  
−
=== Visualization ===
+
* [[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.
−
* [[Image:bms_logo_small.png|16px]] [[BMotion Studio]] a visual editor which enables the developer of a formal model to set-up easily a domain specific visualization.
 
  
−
=== Documentation ===
+
* [[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.
−
* [[Image:ProR_logo.png|32px]] [[ProR]] supports integration of natural language requirements and Event-B models.
 
−
* [[B2Latex]] allows to typeset an event-B model with latex,
 
  
−
=== Theory and Proof ===
+
==Lectures==
−
* [[Isabelle for Rodin]]: Prove proof obligations with Isabelle/HOL. Export proof obligations to Isabelle/HOL theories.
 
−
* [[Theory Plug-in|Theory Plug-in]] provides capabilities to extend the Event-B mathematical language and the Rodin proving infrastructure.
 
−
* [[Proof Purger Interface|Proof Purger]] offers to delete unused proofs.
 
−
* [[Proof Skeleton View]] displays the skeleton of existing proofs.
 
−
* [[SMT Plug-in]] provides interface for SMT solvers.
 
−
* [[Relevance Filter Plug-in]] Uses heuristics to filter hypotheses shown to the prover
 
  
−
=== Code Generation ===
+
* [[Media:iUML-BClassDiagramsLecture.pdf | UML-B Class-diagrams Lecture]] : Lecture slides on the use of UML-B Class-diagrams
−
* [http://poporo.uma.pt/favas/EventB2Java.html EventB2Java] generates JML-specified Java implementations of Event-B models. Contributions by Néstor Cataño, Tim Wahls, Camilo Rueda and Víctor Rivera.
 
−
* [http://poporo.uma.pt/favas/EventB2JML.html EventB2JML] translates Event-B machines to JML-specified Java abstract classes. Contributions by Néstor Cataño, Tim Wahls, Camilo Rueda and Víctor Rivera.
 
−
* [http://poporo.uma.pt/eventb2dafny/Home.html EventB2Dafny] translates Event-B proof-obligations into the input language of Dafny. Developed by Néstor Cataño.
 
−
* [http://users.dickinson.edu/~wahlst/eventb2sql/eventb2sql.html EventB2SQL] translates Event-B machines to Java implementations that make the state of a machine persistent by storing it in a database.
 
−
* [http://eb2all.loria.fr/ EB2ALL] (Beta Version) supports automatic code generation from Event-B to C, C++, Java and C#.
 
−
* [[Code Generation|Tasking Event-B]] supports generation of multi-tasking Java, Ada, and OpenMP C code from Event-B.
 
−
* [[B2C plugin|B2C]] translates Event-B models to C source code, which may then be compiled using external C development tools.
 
−
* [http://eventb-to-vhdl.tk/ EHDL] The plug-in enables [http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=6037401 VHDL code generation] from formal Event-B models automatically.
 
  
−
=== Experimental ===
+
* [[Media:iUML-BStatemachinesLecture.pdf | UML-B State-machines Lecture]] : Lecture slides on the use of UML-B State-machines.
−
* [[Group refinement plugin|Group Refinement]] changes the set of refinement laws for one refinement step to facilitate a case of atomicity refinement.
 
−
* [[Model Critic]] is an extension using the Epsilon scripting language to analyse Event-B models
 
−
* [[Feature Composition Plug-in]] allows the composition of Event-B features (machines|contexts) and helps the user in resolving conflicts before composition.
 
−
* [[Feature Modelling Tool]] (prototype) can be used to build feature models for product lines and configure these to generate product line members.
 
−
* [[Pattern]] allows the reusing of existing models within a development in order to save the modelling and proving effort.
 
−
* [[Image:Project diagram icon s.png]] [[Project Diagram]] displays the diagram of a Rodin project.
 
−
* [[MBT_plugin|MBT plugin]] can be used to generate test sequences covering the events of an Event-B model.
 
−
* [[Transformation patterns]] allow writing and running transformation scripts in EOL over Event-B models.
 
  
−
== Rodin Plug-in Tutorials ==
+
==Tutorials==
−
* [[UML-B Tutorial]]
+
 
−
* [[Requirements Tutorial]],
+
* [[iUML-B Class-diagrams Tutorial]] : A tutorial on the use of UML-B Class-diagrams.
−
* [[AnimB Flash Tutorial|Flash Animation Tutorial]] with animB and Adobe CS3.
+
 
−
* [http://deploy-eprints.ecs.soton.ac.uk/227/ Modularisation Tutorial]
+
* [[iUML-B State-machines Tutorial]] : A tutorial on the use of UML-B State-machines.
−
== Tips & Tricks ==
+
 
 +
==Guidelines==
 +
 
 +
* [[UML-B - Modelling a control system]] : Some guidelines on modelling styles for a control system
  
−
* [[Installing external plug-ins manually]]
 
  
 
[[Category:User documentation]]
 
[[Category:User documentation]]
 +
[[Category:UML-B]]
 
[[Category:Plugin]]
 
[[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=Rodin_Plug-ins&oldid=14397’