imported>WikiSysop |
|
| Line 1: |
Line 1: |
| − | ==5th Rodin User and Developer Workshop==
| + | General diagram for the sluice controller example |
| − | | |
| − | ''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 [http://www.irit.fr/ABZ2014/ ABZ 2014 conference].
| |
| − | | |
| − | The format will be presentations together with plenty of time for discussion.
| |
| − | On day 1 in the morning a Demonstrator and Developer Tutorial will be held
| |
| − | while the remaining 1.5 days will be devoted to tool usage and tool developments.
| |
| − | | |
| − | Proceedings of the 2014 Rodin Workshop will be made available as a technical report.
| |
| − | | |
| − | The Rodin Workshop is supported by the [http://www.advance-ict.eu FP7 ADVANCE Project [[image:Logo_web.png|128px]] ].
| |
| − | | |
| − | | |
| − | == Programme ==
| |
| − | | |
| − | <b>Monday 2 June 2014</b>
| |
| − | {|
| |
| − | | 08h45 - 09h00 || <b>REGISTRATION</b>
| |
| − | |-
| |
| − | | 09h00 - 10h30 || Practical Theory Extension Tutorial session 1
| |
| − | |-
| |
| − | | || Asieh Salehi, Jean-Raymond Abrial, Michael Butler
| |
| − | |-
| |
| − | | 10h30 - 11h00 || <b>BREAK</b>
| |
| − | |-
| |
| − | | 11h00 - 12h30 || Practical Theory Extension Tutorial session 2
| |
| − | |-
| |
| − | | || Asieh Salehi, Jean-Raymond Abrial, Michael Butler
| |
| − | |}
| |
| − | {|
| |
| − | |-
| |
| − | | 12h30 - 14h00 || <b>LUNCH</b>
| |
| − | |-
| |
| − | | 14h00 - 15h20 || <b>Tool use</b>
| |
| − | |-
| |
| − | | || 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
| |
| − | |-
| |
| − | | || || Michael Leuschel, Jens Bendisposto and Dominik Hansen
| |
| − | |-
| |
| − | | || 14h40 || Run-time Management of Many-core Systems using Rodin
| |
| − | |-
| |
| − | | || || 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 || <b>BREAK</b>
| |
| − | |-
| |
| − | | 16h00 - 17h20 || <b>Tool use</b>
| |
| − | |-
| |
| − | | || 16h00 || Developing and Proving a Complicated System Model with Rodin
| |
| − | |-
| |
| − | | || || 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 || <b>Tool development</b>
| |
| − | |-
| |
| − | | || 17h20 || Code Generation – Tool Developments
| |
| − | |-
| |
| − | | || || Andy Edmunds
| |
| − | |-
| |
| − | | || 17h40 || Toolbox for penetration testing based on Rodin and ProB
| |
| − | |-
| |
| − | | || || Aymerick Savary, Marc Frappier, Jean-Louis Lanet
| |
| − | |}
| |
| − | <b>Tuesday 3 June 2014</b>
| |
| − | {|
| |
| − | | 09h00 - 10h20 || <b>Tool development</b>
| |
| − | |-
| |
| − | | || 09h00 || iUML-B Statemachines
| |
| − | |-
| |
| − | | || || Colin Snook
| |
| − | |-
| |
| − | | || 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
| |
| − | |-
| |
| − | | || || 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 || <b>BREAK</b>
| |
| − | |-
| |
| − | | 11h00 - 11h40 || <b>Tool development</b>
| |
| − | |-
| |
| − | | || 11h00 || A Practical Approach for Validation with Rodin Theories
| |
| − | |-
| |
| − | | || || Daniel Plagge, Michael Leuschel
| |
| − | |-
| |
| − | | || 11h20 || Rodin Multi-Simulation Plug-in
| |
| − | |-
| |
| − | | || || Vitaly Savicks, Michael Butler, John Colley, Jens Bendisposto
| |
| − | |-
| |
| − | | 11h40 - 12h00 || <b>Teaching</b>
| |
| − | |-
| |
| − | | || 11h40 || Formal Methods, Requirements and Software Engineering
| |
| − | |-
| |
| − | | || || Ken Robinson
| |
| − | |-
| |
| − | | 12h00 - 12h20 || <b>Theory</b>
| |
| − | |-
| |
| − | | || 12h00 || Responsiveness and Event-B
| |
| − | |-
| |
| − | | || || James Sharp, John Colley, Helen Marshall, Neil Evans, Michael Butler, Colin Snook
| |
| − | |-
| |
| − | | 12h20 - 14h00 || <b>LUNCH</b>
| |
| − | |-
| |
| − | | 14h00 - 15h20 || <b>Theory</b>
| |
| − | |-
| |
| − | | || 14h00 || Incorporating "operation calls" in Event-B and Rodin (by means of Guarded Events)
| |
| − | |-
| |
| − | | || || Jean-Raymond Abrial
| |
| − | |-
| |
| − | | || 14h20 || Program Development in Event-B with Proof Outlines
| |
| − | |-
| |
| − | | || || Stefan Hallerstede
| |
| − | |-
| |
| − | | || 14h40 || Applying and Extending the Event Refinement Structure Approach to Workflow Modelling
| |
| − | |-
| |
| − | | || || Dana Dghaym, Michael Butler, and Asieh Salehi Fathabadi
| |
| − | |-
| |
| − | | || 15h00 || Smart Grids: Multi-Simulation, An Application
| |
| − | |-
| |
| − | | || || Brett Bicknell, Karim Kanso, Jose Reis
| |
| − | |-
| |
| − | | 15h20 - 16h00 || <b>BREAK</b>
| |
| − | |-
| |
| − | | 16h00 - 17h40 || <b>Theory</b>
| |
| − | |-
| |
| − | | || 16h00 || Towards Patterns for Statemachine Modelling under Timing Constraints
| |
| − | |-
| |
| − | | || || Gintautas Sulskus, Michael Poppleton, Abdolbaghi Rezazadeh
| |
| − | |-
| |
| − | | || 16h20 || From Untimed Specification to Cycle-Accurate Implementation - Cyber-Physical System Model Refinement with Event-B
| |
| − | |-
| |
| − | | || || John Colley, Michael Butler
| |
| − | |-
| |
| − | | || 16h40 || Event-B for Safety Analysis of Critical Systems
| |
| − | |-
| |
| − | | || || Matthias Gudemann 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
| |
