imported>Pascal |
imported>Andy |
| Line 1: |
Line 1: |
| − | = Rodin User and Developer Workshop, University of Duesseldorf, 20-22 September 2010 = | + | = The Theory Plug-in = |
| | + | The theory plug-in is used to add mathematical extensions to Rodin. The theories are created, and deployed, and can then be used in any models in the workspace. When dealing with implementation level models, such as in Tasking Event-B, we need to consider how to translate newly added types and operators into code. We have augmented the theory interface with a Translation Rules section. This enables a user to define translation rules that map Event-B formulas to code. |
| | + | == Translation Rules== |
| | + | Figure 1 shows the interface, and some translations rules of the mapping to Ada. |
| | | | |
| | + | <div id="fig:Translation Rules"> |
| | + | <br/> |
| | + | [[Image:TheoryCGRules.png|center||caption text]] |
| | + | <center>'''Figure 1''': Translation Rules</center> |
| | + | <br/> |
| | + | </div> |
| | | | |
| | + | The translation rules are templates used for pattern matching. The meta-variables are defined and typed, and used in the rules. Event-B expressions and predicates are defined on the left hand side of the rule, and the code to be output (as text) appears on the right hand side of the matching rule. |
| | | | |
| − | ==Monday 20th September== | + | == Type Rules == |
| − | Tutorial "How to extend Rodin?" for developers (by Systerel).
| |
| | | | |
| − | The tutorial will be interactive, so please bring your laptop and keep your development environment up-to-date (Eclipse 3.6, Java 1.6, current Rodin source files). | + | The type rules section, shown in Figure 1, is where the relationship is defined, between Event-B types and the type system of the implementation. |
| | | | |
| − | 09h00 - 10h30 Creating a plug-in, Extending the database, Extending the structured editor
| + | = Adding new Types = |
| − | 10h30 - 11h00 Coffee break
| + | In the following example we wish to add a new type to Event-B, and then define its translation to code. |
| − | 11h00 - 12h30 Extending the pretty print page, providing help, extending the Event-B explorer
| |
| − | 12h30 - 14h00 Lunch break
| |
| − | 14h00 - 15h30 Extending the static checker, extending the proof obligation generator
| |
| − | 15h30 - 16h00 Coffee break
| |
| − | 16h00 - 17h00 Adding reasoners
| |
| − | | |
| − | ==Tuesday 21st September (Workshop Day 1)== | |
| − | * 09h00 - 10h30 ''Atomicity Decomposition a Technique for Structuring Refinement in Event-B'', Asieh Salehi Fathabadi, Michael Butler
| |
| − | * 09h30 - 10h00 ''Integrating astd in the Rodin platform'', Paul Amar, Marc Frappier, Cecile Lartaud, and Jeremy Milhau
| |
| − | * 10h00 - 10h30 ''Potpourri of what? One year in a DA's life'', Aryldo G. Russo Jr., Thiago C. de Sousa, Haniel Barbosa, Paulo Muniz, and David Deharbe
| |
| − | * 10h30 - 11h00 Coffee break
| |
| − | * 11h00 - 11h30 ''The ProR Requirements Engineering Platform'', Michael Jastram
| |
| − | * 11h30 - 12h00 ''A Refinement Planning Sheet'', Shin Nakajima
| |
| − | * 12h00 - 12h30 ''Refinement Plans for Reasoned Modelling'', Maria Teresa Llano, Andrew Ireland, and Gudmund Grov
| |
| − | * 12h30 - 14h00 Lunch break and tool demos
| |
| − | * 14h00 - 15h00 ''Invited Talk'', Jean-Raymond Abrial
| |
| − | * 15h00 - 15h30 ''Reflections on the teaching of System Modelling and Design'', Ken Robinson
| |
| − | * 15h30 - 16h00 Coffee break
| |
| − | * 16h00 - 16h30 ''Verification of a Byzantine Agreement Protocol using Event-B'', Roman Krenicky and Mattias Ulbrich
| |
| − | * 16h30 - 17h00 ''Code Generation with the Event-B Tasking Extension (Tool Development)'', Andy Edmunds
| |
| − | * 17h00 - 17h30 ''Modelling Recursion in Event-B'', Stefan Hallerstede
| |
| − | | |
| − | ==Wednesday 22nd September (Workshop Day 2)==
| |
| − | * 09h00 - 09h30 Using automated theory formation to discover invariants of Event-B models, Maria Teresa Llano, Andrew Ireland, Alison Pease, Simon Colton, John Charnley
| |
| − | * 09h30 - 10h00 ''Specifying and Solving Constraint Satisfaction Problems in B'', Michael Leuschel and Daniel Plagge
| |
| − | * 10h00 - 10h30 F''ault Tolerance View in Event-B Development'', Ilya Lopatkin, Alexei Iliasov, Alexander Romanovsky
| |
| − | * 10h30 - 11h00 Coffee break
| |
| − | * 11h00 - 11h30 ''Event-B models of P systems'', Florentin Ipate, Turcanu Adrian
| |
| − | * 11h30 - 11h45 ''Records'', Vitaly Savicks, Colin Snook, Michael Butler
| |
| − | * 11h45 - 12h00 ''Decomposition Tool: Development and Usage'', Renato Silva, Carine Pascal, T.S. Hoang, and Michael Butler
| |
| − | * 12h00 - 12h15 ''Sequence Refinement'', ''Modularisation Plugin'', Alexei Iliasov
| |
| − | * 12h15 - 12h30 ''Modelling Views Paradigm Support for Rodin'', Alexei Iliasov
| |
| − | * 12h30 - 14h00 Lunch break and tool demos
| |
| − | * 14h00 - 15h00 ''Invited Talk'', Joe Kiniry
| |
| − | * 15h00 - 15h30 ''A small experiment in Event-B rippling'', Gudmund Grov, Alan Bundy & Lucas Dixon
| |
| − | * 15h30 - 16h00 Coffee break
| |
| − | * 16h00 - 16h30 ''Animation of UML-B State-machines'', Vitaly Savicks, Colin Snook, Michael Butler
| |
| − | * 16h30 - 17h00 ''Addressing Extensibility Issues in Rodin and Event-B'', Issam Maamria and Michael Butler
| |
| − | | |
| − | =Registration=
| |
| − | [http://www.formal-methods.de/avocs10/registration.html Registration page]
| |
The Theory Plug-in
The theory plug-in is used to add mathematical extensions to Rodin. The theories are created, and deployed, and can then be used in any models in the workspace. When dealing with implementation level models, such as in Tasking Event-B, we need to consider how to translate newly added types and operators into code. We have augmented the theory interface with a Translation Rules section. This enables a user to define translation rules that map Event-B formulas to code.
Translation Rules
Figure 1 shows the interface, and some translations rules of the mapping to Ada.
Figure 1: Translation Rules
The translation rules are templates used for pattern matching. The meta-variables are defined and typed, and used in the rules. Event-B expressions and predicates are defined on the left hand side of the rule, and the code to be output (as text) appears on the right hand side of the matching rule.
Type Rules
The type rules section, shown in Figure 1, is where the relationship is defined, between Event-B types and the type system of the implementation.
Adding new Types
In the following example we wish to add a new type to Event-B, and then define its translation to code.
