Difference between revisions of "Rodin Workshop 2014"

From Event-B
Jump to navigationJump to search
imported>WikiSysop
(Created page with "==5th Rodin User and Developer Workshop== ''June 2-3, 2014'' Toulouse http://wiki.event-b.org/index.php/Rodin_Workshop_2013 The purpose of the Rodin workshop is to bring ...")
 
imported>Andy
 
(46 intermediate revisions by 5 users not shown)
Line 5: Line 5:
 
Toulouse
 
Toulouse
  
−
http://wiki.event-b.org/index.php/Rodin_Workshop_2013
+
http://wiki.event-b.org/index.php/Rodin_Workshop_2014
  
 
The purpose of the Rodin workshop  
 
The purpose of the Rodin workshop  
Line 16: Line 16:
 
development effort.
 
development effort.
  
−
Preceding Rodin User and Developer Workshops were held at Abo Akademi, the University of
+
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.
 
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 5th Rodin workshop will be collocated with the [http://www.irit.fr/ABZ2014/ ABZ 2014 conference].
 +
 
 +
To attend the workshop, please [http://www.irit.fr/ABZ2014/regi.html 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.
 +
 
 +
[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]] ].
 +
 
 +
== Programme ==
 +
 
 +
<b>Monday 2 June 2014</b>
 +
{|
 +
| 08h45 - 09h00 || <b>REGISTRATION</b>
 +
|-
 +
| 09h00 - 10h30 || Practical Theory Extension Tutorial session 1 (Chair: Stefan Hallerstede)
 +
|-
 +
| || Asieh Salehi, Jean-Raymond Abrial, Michael Butler [http://wiki.event-b.org/images/Theory_RodinWorkshop_June2014.pdf]
 +
|-
 +
| 10h30 - 11h00 || <b>BREAK</b>
 +
|-
 +
| 11h00 - 12h30 || Practical Theory Extension Tutorial session 2 (Chair: Stefan Hallerstede)
 +
|-
 +
| || Asieh Salehi, Jean-Raymond Abrial, Michael Butler [http://wiki.event-b.org/images/JRA1_A_sld_math.pdf]
 +
|}
 +
{|
 +
|-
 +
| 12h30 - 14h00 || <b>LUNCH</b>
 +
|-
 +
| 14h00 - 15h20 || <b>Tool use</b> (Chair: John Colley)
 +
|-
 +
| || 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
 +
|-
 +
| || 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
 +
|-
 +
| || 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
 +
|-
 +
| || 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
 +
|-
 +
| 15h20 - 16h00 || <b>BREAK</b>
 +
|-
 +
| 16h00 - 17h20 || <b>Tool use</b> (Chair: Laurent Voisin)
 +
|-
 +
| || 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
 +
|-
 +
| || 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
 +
|-
 +
| || 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  [http://wiki.event-b.org/images/RUDW2014dalvandi.pdf]
 +
|-
 +
| || || Mohammadsadegh Dalvandi, Michael Butler
 +
|-
 +
| 17h20 - 18h00 || <b>Tool development</b> (Chair: Colin Snook)
 +
|-
 +
| || 17h20 || A Practical Approach for Validation with Rodin Theories [http://wiki.event-b.org/images/MLeuscshel_TheorySupport_Rodin_ABZ14.pdf]
 +
|-
 +
| || || Daniel Plagge, Michael Leuschel
 +
|-
 +
| || 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
 +
|}
 +
<b>Tuesday 3 June 2014</b>
 +
{|
 +
| 09h00 - 10h20 || <b>Tool development</b> (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 [http://wiki.event-b.org/images/AITSADOUNE_Rodin2014.pdf]
 +
|-
 +
| || || 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 - 12h00 || <b>Tool development / use</b> (Chair: Jean-Raymond Abrial)
 +
|-
 +
| || 11h00  || Rodin Multi-Simulation Plug-in
 +
|-
 +
| || || Vitaly Savicks, Michael Butler, John Colley, Jens Bendisposto
 +
|-
 +
| || 11h20 || Code Generation – Tool Developments [http://wiki.event-b.org/images/Ae1RUDW2014presentation.pdf]
 +
|-
 +
| || || Andy Edmunds
 +
|-
 +
| || 11h40 || Smart Grids: Multi-Simulation, An Application [https://mega.co.nz/#F!o8MwiDSa!9cU-yKsLqpLaSGKWphCh4g]
 +
|-
 +
| || || Brett Bicknell, Karim Kanso, Jose Reis
 +
|-
 +
| 12h00 - 12h20 || <b>Teaching</b>  (Chair: Jean-Raymond Abrial)
 +
|-
 +
| || 12h00 || Formal Methods, Requirements and Software Engineering [http://wiki.event-b.org/images/KRobinsonWorkshopSlides.pdf]
 +
|-
 +
| || || Ken Robinson
 +
|-
 +
| 12h20 - 14h00 || <b>LUNCH</b>
 +
|-
 +
| 14h00 - 15h20 || <b>Theory / Tool Use</b> (Chair: Matthias Güdemann)
 +
|-
 +
| || 14h00 || Applying and Extending the Event Refinement Structure Approach to Workflow Modelling
 +
|-
 +
| || || 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)]
 +
|-
 +
| || || 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 || <b>BREAK</b>
 +
|-
 +
| 16h00 - 17h40 || <b>Theory</b> (Chair: Michael Butler)
 +
|-
 +
| || 16h00 || Towards Patterns for Statemachine Modelling under Timing Constraints
 +
|-
 +
| || || Gintautas Sulskus, Michael Poppleton, Abdolbaghi Rezazadeh [http://wiki.event-b.org/images/Gintas_prototype_pattern_gintautas_sulskus.pdf]
 +
|-
 +
| || 16h20 || iUML-B Statemachines [http://wiki.event-b.org/images/CFS1_Rodin14_Statemachines.pdf]
 +
|-
 +
| || || Colin Snook
 +
|-
 +
| || 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 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

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 Logo web.png .

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’