Rodin Workshop 2014: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older edit
imported>Andy
imported>Andy
 
(16 intermediate revisions by 2 users not shown)
Line 39: Line 39:
| 09h00 - 10h30 || Practical Theory Extension Tutorial session 1 (Chair: Stefan Hallerstede)
| 09h00 - 10h30 || Practical Theory Extension Tutorial session 1 (Chair: Stefan Hallerstede)
|-  
|-  
| || Asieh Salehi, Jean-Raymond Abrial, Michael Butler
| || Asieh Salehi, Jean-Raymond Abrial, Michael Butler [http://wiki.event-b.org/images/Theory_RodinWorkshop_June2014.pdf]
|-  
|-  
| 10h30 - 11h00 || <b>BREAK</b>
| 10h30 - 11h00 || <b>BREAK</b>
Line 45: Line 45:
| 11h00 - 12h30 || Practical Theory Extension Tutorial session 2 (Chair: Stefan Hallerstede)
| 11h00 - 12h30 || Practical Theory Extension Tutorial session 2 (Chair: Stefan Hallerstede)
|-  
|-  
| || Asieh Salehi, Jean-Raymond Abrial, Michael Butler
| || Asieh Salehi, Jean-Raymond Abrial, Michael Butler [http://wiki.event-b.org/images/JRA1_A_sld_math.pdf]
|}
|}
{|
{|
Line 53: Line 53:
| 14h00 - 15h20 || <b>Tool use</b> (Chair: John Colley)
| 14h00 - 15h20 || <b>Tool use</b> (Chair: John Colley)
|-  
|-  
| || 14h00 || Modeling a Safe Interlocking Using the Event-B Theory Plug-in
| || 14h00 || Modeling a Safe Interlocking Using the Event-B Theory Plug-in [http://wiki.event-b.org/images/KVM_RodinWS_2014_A.pdf]
|-  
|-  
| || || Thang Khuu, Laurent Voisin, Fernando Mejia
| || || Thang Khuu, Laurent Voisin, Fernando Mejia
Line 61: Line 61:
| || || Michael Leuschel, Jens Bendisposto and Dominik Hansen  
| || || Michael Leuschel, Jens Bendisposto and Dominik Hansen  
|-  
|-  
| || 14h40 || Run-time Management of Many-core Systems using Rodin
| || 14h40 || Run-time Management of Many-core Systems using Rodin [https://dl.dropboxusercontent.com/u/45242223/RodinWS_PRiME.pdf]
|-  
|-  
| || || Asieh Salehi, Colin Snook, Michael Butler
| || || Asieh Salehi, Colin Snook, Michael Butler
|-  
|-  
| || 15h00 || An Experiment in Modeling Satellite Flight Formation in Event-B
| || 15h00 || An Experiment in Modeling Satellite Flight Formation in Event-B [http://wiki.event-b.org/images/Slides_PereverzevaInna.pdf]
|-  
|-  
| || || Inna Pereverzeva, Anton Tarasyuk, Elena Troubitsyna
| || || Inna Pereverzeva, Anton Tarasyuk, Elena Troubitsyna
Line 77: Line 77:
| || || A. V. Khoroshilov, I. V. Shchepetkov
| || || A. V. Khoroshilov, I. V. Shchepetkov
|-  
|-  
| || 16h20 || Formalisation of Self-Organizing Multi-Agent Systems with Event-B and Design Patterns
| || 16h20 || Formalisation of Self-Organizing Multi-Agent Systems with Event-B and Design Patterns [http://wiki.event-b.org/images/ZGraja-RodinWorkshop2014.pdf]
|-  
|-  
| || || Zeineb Graja, Frederic Migeon, Christine Maurel, Marie-Pierre Gleizes, Ahmed Hadj Kacem
| || || Zeineb Graja, Frederic Migeon, Christine Maurel, Marie-Pierre Gleizes, Ahmed Hadj Kacem
Line 85: Line 85:
| || || Toby Wilkinson, Michael Butler, John Colley, Colin Snook
| || || Toby Wilkinson, Michael Butler, John Colley, Colin Snook
|-  
|-  
| || 17h00 || Towards Verified Implementation of Event-B Models in Dafny
| || 17h00 || Towards Verified Implementation of Event-B Models in Dafny [http://wiki.event-b.org/images/RUDW2014dalvandi.pdf]
|-  
|-  
| || || Mohammadsadegh Dalvandi, Michael Butler
| || || Mohammadsadegh Dalvandi, Michael Butler
Line 95: Line 95:
| || || Daniel Plagge, Michael Leuschel  
| || || Daniel Plagge, Michael Leuschel  
|-
|-
| || 17h40 || Toolbox for penetration testing based on Rodin and ProB
| || 17h40 || Toolbox for penetration testing based on Rodin and ProB [http://blog.aymericksavary.fr/wp-content/uploads/2014/06/Pr%C3%A9sentation.pdf]
|-  
|-  
| || || Aymerick Savary, Marc Frappier, Jean-Louis Lanet
| || || Aymerick Savary, Marc Frappier, Jean-Louis Lanet
Line 131: Line 131:
| || || Andy Edmunds
| || || Andy Edmunds
|-
|-
| || 11h40 || Smart Grids: Multi-Simulation, An Application
| || 11h40 || Smart Grids: Multi-Simulation, An Application [https://mega.co.nz/#F!o8MwiDSa!9cU-yKsLqpLaSGKWphCh4g]
|-  
|-  
| || || Brett Bicknell, Karim Kanso, Jose Reis
| || || Brett Bicknell, Karim Kanso, Jose Reis
Line 137: Line 137:
| 12h00 - 12h20 || <b>Teaching</b>  (Chair: Jean-Raymond Abrial)
| 12h00 - 12h20 || <b>Teaching</b>  (Chair: Jean-Raymond Abrial)
|-  
|-  
| || 12h00 || Formal Methods, Requirements and Software Engineering
| || 12h00 || Formal Methods, Requirements and Software Engineering [http://wiki.event-b.org/images/KRobinsonWorkshopSlides.pdf]
|-  
|-  
| || || Ken Robinson
| || || Ken Robinson
Line 147: Line 147:
| || 14h00 || Applying and Extending the Event Refinement Structure Approach to Workflow Modelling
| || 14h00 || Applying and Extending the Event Refinement Structure Approach to Workflow Modelling
|-  
|-  
| || || Dana Dghaym, Michael Butler, and Asieh Salehi Fathabadi
| || || Dana Dghaym, Michael Butler, and Asieh Salehi Fathabadi [http://wiki.event-b.org/images/DanaRodin_2014.pdf]
|-  
|-  
| || 14h20 || [http://wiki.event-b.org/images/Abrial2RUDW2014.pdf Incorporating "operation calls" in Event-B and Rodin (by means of Guarded Events)]
| || 14h20 || [http://wiki.event-b.org/images/Abrial2RUDW2014.pdf Incorporating "operation calls" in Event-B and Rodin (by means of Guarded Events)]  
|-  
|-  
| || || Jean-Raymond Abrial
| || || Jean-Raymond Abrial
Line 169: Line 169:
| || || Gintautas Sulskus, Michael Poppleton, Abdolbaghi Rezazadeh [http://wiki.event-b.org/images/Gintas_prototype_pattern_gintautas_sulskus.pdf]
| || || Gintautas Sulskus, Michael Poppleton, Abdolbaghi Rezazadeh [http://wiki.event-b.org/images/Gintas_prototype_pattern_gintautas_sulskus.pdf]
|-  
|-  
| || 16h20 || iUML-B Statemachines
| || 16h20 || iUML-B Statemachines [http://wiki.event-b.org/images/CFS1_Rodin14_Statemachines.pdf]
|-  
|-  
| || || Colin Snook  
| || || Colin Snook  

Latest revision as of 06:13, 24 June 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.

Proceedings of the 2014 Rodin Workshop are available as a technical report from the University of Southampton.

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 [1]
10h30 - 11h00 BREAK
11h00 - 12h30 Practical Theory Extension Tutorial session 2 (Chair: Stefan Hallerstede)
Asieh Salehi, Jean-Raymond Abrial, Michael Butler [2]
12h30 - 14h00 LUNCH
14h00 - 15h20 Tool use (Chair: John Colley)
14h00 Modeling a Safe Interlocking Using the Event-B Theory Plug-in [3]
Thang Khuu, Laurent Voisin, Fernando Mejia
14h20 Unlocking the Mysteries of a Formal Model of an Interlocking System [4]
Michael Leuschel, Jens Bendisposto and Dominik Hansen
14h40 Run-time Management of Many-core Systems using Rodin [5]
Asieh Salehi, Colin Snook, Michael Butler
15h00 An Experiment in Modeling Satellite Flight Formation in Event-B [6]
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 [7]
A. V. Khoroshilov, I. V. Shchepetkov
16h20 Formalisation of Self-Organizing Multi-Agent Systems with Event-B and Design Patterns [8]
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 [9]
Mohammadsadegh Dalvandi, Michael Butler
17h20 - 18h00 Tool development (Chair: Colin Snook)
17h20 A Practical Approach for Validation with Rodin Theories [10]
Daniel Plagge, Michael Leuschel
17h40 Toolbox for penetration testing based on Rodin and ProB [11]
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 [12]
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 [13]
Andy Edmunds
11h40 Smart Grids: Multi-Simulation, An Application [14]
Brett Bicknell, Karim Kanso, Jose Reis
12h00 - 12h20 Teaching (Chair: Jean-Raymond Abrial)
12h00 Formal Methods, Requirements and Software Engineering [15]
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 [16]
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 [17]
16h20 iUML-B Statemachines [18]
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

Retrieved from ‘https://wiki.event-b.org/index.php?title=Rodin_Workshop_2014&oldid=9019’