Rodin Workshop 2014
5th Rodin User and Developer Workshop
June 2-3, 2014
Toulouse
http://wiki.event-b.org/index.php/Rodin_Workshop_2014
The purpose of the Rodin workshop is to bring together existing and potential users and developers of the Rodin toolset and to foster a broader community of Rodin users and developers. For Rodin users the workshop will provide an opportunity to share tool experiences and to gain an understanding of on-going tool developments. For plug-in developers the workshop will provide an opportunity to showcase their tools and to achieve better coordination of tool development effort.
Previous Rodin User and Developer Workshops were held at Abo Akademi, the University of Southampton, the University of Düsseldorf and the University of Paris-Est Créteil.
The 5th Rodin workshop will be collocated with the ABZ 2014 conference.
To attend the workshop, please register on the ABZ website.
The format will be presentations together with plenty of time for discussion. On day 1 in the morning a Tutorial will be held while the remaining 1.5 days will be devoted to tool usage and tool developments.
The Rodin Workshop is supported by the FP7 ADVANCE Project 
.
Programme
Monday 2 June 2014
| 08h45 - 09h00 | REGISTRATION |
| 09h00 - 10h30 | Practical Theory Extension Tutorial session 1 (Chair: Stefan Hallerstede) |
| Asieh Salehi, Jean-Raymond Abrial, Michael Butler | |
| 10h30 - 11h00 | BREAK |
| 11h00 - 12h30 | Practical Theory Extension Tutorial session 2 (Chair: Stefan Hallerstede) |
| Asieh Salehi, Jean-Raymond Abrial, Michael Butler [1] |
| 12h30 - 14h00 | LUNCH | |
| 14h00 - 15h20 | Tool use (Chair: John Colley) | |
| 14h00 | Modeling a Safe Interlocking Using the Event-B Theory Plug-in | |
| Thang Khuu, Laurent Voisin, Fernando Mejia | ||
| 14h20 | Unlocking the Mysteries of a Formal Model of an Interlocking System [2] | |
| Michael Leuschel, Jens Bendisposto and Dominik Hansen | ||
| 14h40 | Run-time Management of Many-core Systems using Rodin [3] | |
| Asieh Salehi, Colin Snook, Michael Butler | ||
| 15h00 | An Experiment in Modeling Satellite Flight Formation in Event-B | |
| Inna Pereverzeva, Anton Tarasyuk, Elena Troubitsyna | ||
| 15h20 - 16h00 | BREAK | |
| 16h00 - 17h20 | Tool use (Chair: Laurent Voisin) | |
| 16h00 | Developing and Proving a Complicated System Model with Rodin [4] | |
| A. V. Khoroshilov, I. V. Shchepetkov | ||
| 16h20 | Formalisation of Self-Organizing Multi-Agent Systems with Event-B and Design Patterns | |
| Zeineb Graja, Frederic Migeon, Christine Maurel, Marie-Pierre Gleizes, Ahmed Hadj Kacem | ||
| 16h40 | Generating Tests for COTS Components with Event-B and STPA | |
| Toby Wilkinson, Michael Butler, John Colley, Colin Snook | ||
| 17h00 | Towards Verified Implementation of Event-B Models in Dafny | |
| Mohammadsadegh Dalvandi, Michael Butler | ||
| 17h20 - 18h00 | Tool development (Chair: Colin Snook) | |
| 17h20 | A Practical Approach for Validation with Rodin Theories [5] | |
| Daniel Plagge, Michael Leuschel | ||
| 17h40 | Toolbox for penetration testing based on Rodin and ProB ### Requires Link ### | |
| Aymerick Savary, Marc Frappier, Jean-Louis Lanet |
Tuesday 3 June 2014
| 09h00 - 10h20 | Tool development (Chair: Jens Bendisposto) | |
| 09h00 | From Untimed Specification to Cycle-Accurate Implementation - Cyber-Physical System Model Refinement with Event-B | |
| John Colley, Michael Butler | ||
| 09h20 | EB2RC: A Rodin plug-in for visualising Event-B models and code generation | |
| Zheng Cheng, Dominique Mery, Rosemary Monahan | ||
| 09h40 | Composition Operators for Event-B. CO4EB Rodin plugin [6] | |
| Idir Ait-Sadoune, Yamine Ait- Ameur | ||
| 10h00 | CODA Update: New Features for 2014 | |
| Neil Evans, Helen Marshall, James Sharp, Michael Butler, John Colley, Colin Snook | ||
| 10h20 - 11h00 | BREAK | |
| 11h00 - 12h00 | Tool development / use (Chair: Jean-Raymond Abrial) | |
| 11h00 | Rodin Multi-Simulation Plug-in | |
| Vitaly Savicks, Michael Butler, John Colley, Jens Bendisposto | ||
| 11h20 | Code Generation – Tool Developments [7] | |
| Andy Edmunds | ||
| 11h40 | Smart Grids: Multi-Simulation, An Application [8] | |
| Brett Bicknell, Karim Kanso, Jose Reis | ||
| 12h00 - 12h20 | Teaching (Chair: Jean-Raymond Abrial) | |
| 12h00 | Formal Methods, Requirements and Software Engineering | |
| Ken Robinson | ||
| 12h20 - 14h00 | LUNCH | |
| 14h00 - 15h20 | Theory / Tool Use (Chair: Matthias Güdemann) | |
| 14h00 | Applying and Extending the Event Refinement Structure Approach to Workflow Modelling | |
| Dana Dghaym, Michael Butler, and Asieh Salehi Fathabadi [9] | ||
| 14h20 | Incorporating "operation calls" in Event-B and Rodin (by means of Guarded Events) | |
| Jean-Raymond Abrial | ||
| 14h40 | Program Development in Event-B with Proof Outlines | |
| Stefan Hallerstede | ||
| 15h00 | Responsiveness and Event-B | |
| James Sharp, John Colley, Helen Marshall, Neil Evans, Michael Butler, Colin Snook | ||
| 15h20 - 16h00 | BREAK | |
| 16h00 - 17h40 | Theory (Chair: Michael Butler) | |
| 16h00 | Towards Patterns for Statemachine Modelling under Timing Constraints | |
| Gintautas Sulskus, Michael Poppleton, Abdolbaghi Rezazadeh [10] | ||
| 16h20 | iUML-B Statemachines [11] | |
| Colin Snook | ||
| 16h40 | Event-B for Safety Analysis of Critical Systems slides model | |
| Matthias Güdemann and Marielle Petit-Doche | ||
| 17h00 | Modelling Of Systems Of Systems - An Event-B Perspective Of a VDM Project | |
| Stefan Hallerstede , Klaus Kristensen, Peter Gorm Larsen |
Organisers
Michael Butler, University of Southampton
Stefan Hallerstede, Aarhus University
Thierry Lecomte, ClearSy
Michael Leuschel, University of Düsseldorf
Alexander Romanovsky, Newcastle University
Laurent Voisin, Systerel
Marina Walden, Åbo Akademi University
