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.

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
10h30 - 11h00	BREAK
11h00 - 12h30	Practical Theory Extension Tutorial session 2 (Chair: Stefan Hallerstede)
	Asieh Salehi, Jean-Raymond Abrial, Michael Butler

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
		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	BREAK
16h00 - 17h20	Tool use (Chair: Laurent Voisin)
	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	Tool development (Chair: Colin Snook)
	17h20	A Practical Approach for Validation with Rodin Theories
		Daniel Plagge, Michael Leuschel
	17h40	Toolbox for penetration testing based on Rodin and ProB
		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
		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 [1]
		Andy Edmunds
	11h40	Smart Grids: Multi-Simulation, An Application
		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 Gudemann)
	14h00	Applying and Extending the Event Refinement Structure Approach to Workflow Modelling
		Dana Dghaym, Michael Butler, and Asieh Salehi Fathabadi
	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
	16h20	iUML-B Statemachines
		Colin Snook
	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