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.

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.

If you are interested in giving a presentation at the Rodin workshop or have a plug-in to demonstrate, send a short abstract (1 or 2 pages PDF) to rodin@ecs.soton.ac.uk by:

• 14 April 2014.

Indicate whether it is a tool usage or tool development presentation. Plug-in presentations may be about existing developments or planned future developments. We will endeavour to accommodate all submissions that are clearly relevant to Rodin and Event-B.

Programme

Monday 2 June 2014

08h45 - 09h00	REGISTRATION
09h00 - 10h30	Practical Theory Extension Tutorial session 1
	Asieh Salehi, Jean-Raymond Abrial, Michael Butler
10h30 - 11h00	BREAK
11h00 - 12h30	Practical Theory Extension Tutorial session 2
	Asieh Salehi, Jean-Raymond Abrial, Michael Butler

12h30 - 14h00	LUNCH
14h00 - 15h20	Tool use
	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
	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
	17h20	Code Generation – Tool Developments
		Andy Edmunds
	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
	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	BREAK
11h00 - 11h40	Tool development
	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	Teaching
	11h40	Formal Methods, Requirements and Software Engineering
		Ken Robinson
12h00 - 12h20	Theory
	12h00	Responsiveness and Event-B
		James Sharp, John Colley, Helen Marshall, Neil Evans, Michael Butler, Colin Snook
12h20 - 14h00	LUNCH
14h00 - 15h20	Theory
	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	BREAK
16h00 - 17h40	Theory
	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