Rodin Workshop 2014: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older edit
imported>WikiSysop
No edit summary
imported>Andy
 
(33 intermediate revisions by 4 users not shown)
Line 27: Line 27:
while the remaining 1.5 days will be devoted to tool usage and tool developments.  
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.
[http://eprints.soton.ac.uk/365301/ Proceedings of the 2014 Rodin Workshop are available as a technical report from the University of Southampton. ]


The Rodin Workshop is supported by the [http://www.advance-ict.eu FP7 ADVANCE Project [[image:Logo_web.png|128px]] ].
The Rodin Workshop is supported by the [http://www.advance-ict.eu FP7 ADVANCE Project [[image:Logo_web.png|128px]] ].
Line 37: Line 37:
| 08h45 - 09h00 || <b>REGISTRATION</b>
| 08h45 - 09h00 || <b>REGISTRATION</b>
|-  
|-  
| 09h00 - 10h30 || Practical Theory Extension Tutorial session 1
| 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>
|-  
|-  
| 11h00 - 12h30 || Practical Theory Extension Tutorial session 2
| 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 51: Line 51:
| 12h30 - 14h00 || <b>LUNCH</b>
| 12h30 - 14h00 || <b>LUNCH</b>
|-  
|-  
| 14h00 - 15h20 || <b>Tool use</b>
| 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
|-  
|-  
| || 14h20 || Unlocking the Mysteries of a Formal Model of an Interlocking System
| || 14h20 || Unlocking the Mysteries of a Formal Model of an Interlocking System [http://wiki.event-b.org/images/MLeuschel_interlocking_rodin_abz14_talk_clean.pdf]
|-  
|-  
| || || 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 71: Line 71:
| 15h20 - 16h00 || <b>BREAK</b>
| 15h20 - 16h00 || <b>BREAK</b>
|-  
|-  
| 16h00 - 17h20 || <b>Tool use</b>
| 16h00 - 17h20 || <b>Tool use</b> (Chair: Laurent Voisin)
|-  
|-  
| || 16h00 || Developing and Proving a Complicated System Model with Rodin
| || 16h00 || Developing and Proving a Complicated System Model with Rodin [http://wiki.event-b.org/images/Shchepetkov-presentation.pdf]
|-  
|-  
| || || 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
|-  
|-  
| 17h20 - 18h00 || <b>Tool development</b>
| 17h20 - 18h00 || <b>Tool development</b> (Chair: Colin Snook)
|-  
|-  
| || 17h20 || A Practical Approach for Validation with Rodin Theories
| || 17h20 || A Practical Approach for Validation with Rodin Theories [http://wiki.event-b.org/images/MLeuscshel_TheorySupport_Rodin_ABZ14.pdf]
|-  
|-  
| || || 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 101: Line 101:
<b>Tuesday 3 June 2014</b>
<b>Tuesday 3 June 2014</b>
{|
{|
| 09h00 - 10h20 || <b>Tool development</b>
| 09h00 - 10h20 || <b>Tool development</b> (Chair: Jens Bendisposto)
|-  
|-  
| || 09h00 || iUML-B Statemachines
| || 09h00 || From Untimed Specification to Cycle-Accurate Implementation - Cyber-Physical System Model Refinement with Event-B
|-  
|-  
| || || Colin Snook
| || || John Colley, Michael Butler
|-  
|-  
| || 09h20 || EB2RC: A Rodin plug-in for visualising Event-B models and code generation
| || 09h20 || EB2RC: A Rodin plug-in for visualising Event-B models and code generation
Line 111: Line 111:
| || || Zheng Cheng, Dominique Mery, Rosemary Monahan
| || || Zheng Cheng, Dominique Mery, Rosemary Monahan
|-  
|-  
| || 09h40 || Composition Operators for Event-B. CO4EB Rodin plugin
| || 09h40 || Composition Operators for Event-B. CO4EB Rodin plugin [http://wiki.event-b.org/images/AITSADOUNE_Rodin2014.pdf]
|-  
|-  
| || || Idir Ait-Sadoune, Yamine Ait- Ameur
| || || Idir Ait-Sadoune, Yamine Ait- Ameur
Line 121: Line 121:
| 10h20 - 11h00 || <b>BREAK</b>
| 10h20 - 11h00 || <b>BREAK</b>
|-  
|-  
| 11h00 - 11h40 || <b>Tool development</b>
| 11h00 - 12h00 || <b>Tool development / use</b> (Chair: Jean-Raymond Abrial)
|-  
|-  
| || 11h00  || Rodin Multi-Simulation Plug-in  
| || 11h00  || Rodin Multi-Simulation Plug-in  
Line 127: Line 127:
| || || Vitaly Savicks, Michael Butler, John Colley, Jens Bendisposto  
| || || Vitaly Savicks, Michael Butler, John Colley, Jens Bendisposto  
|-  
|-  
| || 11h20 || Code Generation – Tool Developments
| || 11h20 || Code Generation – Tool Developments [http://wiki.event-b.org/images/Ae1RUDW2014presentation.pdf]
|-  
|-  
| || || Andy Edmunds
| || || Andy Edmunds
|-
| || 11h40 || Smart Grids: Multi-Simulation, An Application [https://mega.co.nz/#F!o8MwiDSa!9cU-yKsLqpLaSGKWphCh4g]
|-
| || || Brett Bicknell, Karim Kanso, Jose Reis
|-  
|-  
| 11h40 - 12h00 || <b>Teaching</b>
| 12h00 - 12h20 || <b>Teaching</b> (Chair: Jean-Raymond Abrial)
|-  
|-  
| || 11h40 || 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
|-
| 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>
| 12h20 - 14h00 || <b>LUNCH</b>
|-  
|-  
| 14h00 - 15h20 || <b>Theory / Tool Use</b>
| 14h00 - 15h20 || <b>Theory / Tool Use</b> (Chair: Matthias Güdemann)
|-  
|-  
| || 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 || 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 159: Line 157:
| || || Stefan Hallerstede
| || || Stefan Hallerstede
|-  
|-  
| || 15h00 || Smart Grids: Multi-Simulation, An Application
| || 15h00 || Responsiveness and Event-B
|-  
|-  
| || || Brett Bicknell, Karim Kanso, Jose Reis
| || || James Sharp, John Colley, Helen Marshall, Neil Evans, Michael Butler, Colin Snook
|-  
|-  
| 15h20 - 16h00 || <b>BREAK</b>
| 15h20 - 16h00 || <b>BREAK</b>
|-  
|-  
| 16h00 - 17h40 || <b>Theory</b>
| 16h00 - 17h40 || <b>Theory</b> (Chair: Michael Butler)
|-  
|-  
| || 16h00 || Towards Patterns for Statemachine Modelling under Timing Constraints
| || 16h00 || Towards Patterns for Statemachine Modelling under Timing Constraints
|-  
|-  
| || || Gintautas Sulskus, Michael Poppleton, Abdolbaghi Rezazadeh
| || || Gintautas Sulskus, Michael Poppleton, Abdolbaghi Rezazadeh [http://wiki.event-b.org/images/Gintas_prototype_pattern_gintautas_sulskus.pdf]
|-  
|-  
| || 16h20 || From Untimed Specification to Cycle-Accurate Implementation - Cyber-Physical System Model Refinement with Event-B
| || 16h20 || iUML-B Statemachines [http://wiki.event-b.org/images/CFS1_Rodin14_Statemachines.pdf]
|-  
|-  
| || || John Colley, Michael Butler
| || || Colin Snook
|-  
|-  
| || 16h40 || Event-B for Safety Analysis of Critical Systems
| || 16h40 || Event-B for Safety Analysis of Critical Systems [http://wiki.event-b.org/images/Event-B_Safety.pdf slides] [https://github.com/openETCS/model-evaluation/tree/master/model/Event_B_Systerel/Subset_026_comm_session model]
|-  
|-  
| || || Matthias Gudemann and Marielle Petit-Doche
| || || Matthias Güdemann and Marielle Petit-Doche  
|-  
|-  
| || 17h00 || Modelling Of Systems Of Systems - An Event-B Perspective Of a VDM Project
| || 17h00 || Modelling Of Systems Of Systems - An Event-B Perspective Of a VDM Project

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’