Difference between revisions of "Rodin Workshop 2013"

From Event-B
Jump to navigationJump to search
imported>Stefan
imported>WikiSysop
Line 6: Line 6:
  
 
http://wiki.event-b.org/index.php/Rodin_Workshop_2013
 
http://wiki.event-b.org/index.php/Rodin_Workshop_2013
−
 
−
Event-B is a formal method for system-level modelling and analysis. The
 
−
Rodin Platform is an Eclipse-based toolset for Event-B that provides
 
−
effective support for modelling and automated proof. The platform is open
 
−
source and is further extendable with plug-ins. A range of plug-ins have
 
−
already been developed including ones that support animation, model
 
−
checking and UML-B.
 
  
 
Preceding Rodin User and Developer Workshops were held at the University of
 
Preceding Rodin User and Developer Workshops were held at 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 fourth workshop will be collocated with the conference iFM 2013:
+
The fourth Rodin workshop will be collocated with the conference iFM 2013:
  
 
http://www.it.abo.fi/iFM2013/
 
http://www.it.abo.fi/iFM2013/
  
−
While much of the development and use of Rodin takes place within EU
+
Registration for the Rodin 2013 Workshop is open:
−
FP7 Projects (RODIN, DEPLOY, ADVANCE), there is a growing group of users
+
http://www.it.abo.fi/iFM2013/rodin_registration.php
−
and plug-in developers outside these projects. The purpose of this workshop  
+
 
 +
The purpose of this workshop  
 
is to bring together existing and potential users and developers of the Rodin  
 
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.
 
toolset and to foster a broader community of Rodin users and developers.
−
 
 
For Rodin users the workshop will provide an opportunity to share tool
 
For Rodin users the workshop will provide an opportunity to share tool
 
experiences and to gain an understanding of on-going tool developments.
 
experiences and to gain an understanding of on-going tool developments.
Line 32: Line 25:
 
development effort.
 
development effort.
  
−
The format will be presentations together with plenty of time for discussion.
+
==Programme==
−
On day 1 in the morning a Demonstrator and Developer Tutorial will be held
+
 
−
while the remaining 1 1/2 days will be devoted to tool usage and tool developments.
+
 
 +
===Monday 10 June===
 +
 
 +
====14:00 - 15:30 Tutorials====
 +
 
 +
* Colin Snook: ''UML-B tutorial''
 +
 
 +
* Jens Bendisposto: ''ProB Tutorial''
 +
 
 +
 
 +
===Tuesday 11 June===
 +
 
 +
====09:00 - 10:30 Session 1====
 +
 
 +
*Yuliya Prokhorova, Elena Troubitsyna, Linas Laibinis: ''Supporting Formal Modelling in Event-B with Safety Cases''
 +
 
 +
*Tsutomu Kobayashi, Fuyuki Ishikawa, and Shinichi Honiden: ''Systematic Planning of Refinement in Event-B''
 +
 
 +
*Colin Snook, Michael Butler: ''iUML-B Diagram Developments''
 +
 
 +
*Neil Evans, Neil Grant, Helen Marshall, James Sharp1 Michael Butler, John Colley, Andy Edmunds, Colin Snook: ''The Co-Design Architecture (CODA) Methodology and Plug-in Tool, Progress Update''
 +
 
 +
====10:30 - 11:00 Break====
 +
 
 +
====11:00 - 12:30 Session 2====
 +
                 
 +
* Laurent Voisin and Minh-Thang Khuu: ''Domain Specific Event-B Modeling''
 +
 
 +
* Ulyana Tikhonova, Maarten Manders, Mark van den Brand, Suzana Andova, and Tom Verhoeff: ''Event-B for Defining the Dynamic Semantics of a DSL''
 +
 
 +
* Jens Bendisposto, Philipp Korner and Michael Leuschel: ''Parallel Model Checking of B Specifications''
 +
 
 +
* Sebastian Krings, Jens Bendisposto, Ivaylo Dobrikov and Michael Leuschel: ''B Constrained''
 +
 
 +
====12:30 - 13:30 Lunch====
 +
 
 +
====13:30 - 14:30 Session 3====
 +
                 
 +
* Invited Talk
 +
 
 +
====14:30 - 15:15 Session 4====
 +
 
 +
* Thai Son Hoang: ''Generic Instantiation and Tool Support''
 +
 
 +
* Alexei Iliasov, Linas Laibinis, Elena Troubitsyna, Alexander Romanovsky: ''Support for Indexed Modules in Event-B''
 +
 
 +
====15:15 - 15:45 Break====
 +
 
 +
====15:45 - 17:15 Session 5====
 +
 
 +
* Andy Edmunds: ''Developments in Code Generation Tools for Event-B''
 +
 
 +
* Sergey Ostroumov , Leonidas Tsiopoulos , Juha Plosila , Kaisa Sere: ''Derivation of Structural VHDL from Component-Based Event-B Models''
 +
 
 +
* Vitaly Savicks, Michael Butler, Jens Bendisposto, John Colley: ''Co-simulation of Event-B and Continuous Models in Rodin''
  
−
If you are interested in giving a presentation at the Rodin workshop or
+
* Adisak Intana, Michael R. Poppleton, and Geoff V. Merrett: ''Proof-based formal methods for WSN development with Simulation Approach''
−
have a plug-in to demonstrate, send a short abstract (1 or 2 pages PDF)
 
−
to rodin@ecs.soton.ac.uk by
 
−
11 April 2013.
 
  
−
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.
 
  
−
''Organisers:''
+
==Organisers==
  
 
Michael Butler, University of Southampton
 
Michael Butler, University of Southampton

Revision as of 04:15, 13 May 2013

4th Rodin User and Developer Workshop

June 10-11, 2013

Turku, Finland

http://wiki.event-b.org/index.php/Rodin_Workshop_2013

Preceding Rodin User and Developer Workshops were held at the University of Southampton, the University of Düsseldorf and the University of Paris-Est Créteil. The fourth Rodin workshop will be collocated with the conference iFM 2013:

http://www.it.abo.fi/iFM2013/

Registration for the Rodin 2013 Workshop is open: http://www.it.abo.fi/iFM2013/rodin_registration.php

The purpose of this 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.

Programme

Monday 10 June

14:00 - 15:30 Tutorials

  • Colin Snook: UML-B tutorial
  • Jens Bendisposto: ProB Tutorial


Tuesday 11 June

09:00 - 10:30 Session 1

  • Yuliya Prokhorova, Elena Troubitsyna, Linas Laibinis: Supporting Formal Modelling in Event-B with Safety Cases
  • Tsutomu Kobayashi, Fuyuki Ishikawa, and Shinichi Honiden: Systematic Planning of Refinement in Event-B
  • Colin Snook, Michael Butler: iUML-B Diagram Developments
  • Neil Evans, Neil Grant, Helen Marshall, James Sharp1 Michael Butler, John Colley, Andy Edmunds, Colin Snook: The Co-Design Architecture (CODA) Methodology and Plug-in Tool, Progress Update

10:30 - 11:00 Break

11:00 - 12:30 Session 2

  • Laurent Voisin and Minh-Thang Khuu: Domain Specific Event-B Modeling
  • Ulyana Tikhonova, Maarten Manders, Mark van den Brand, Suzana Andova, and Tom Verhoeff: Event-B for Defining the Dynamic Semantics of a DSL
  • Jens Bendisposto, Philipp Korner and Michael Leuschel: Parallel Model Checking of B Specifications
  • Sebastian Krings, Jens Bendisposto, Ivaylo Dobrikov and Michael Leuschel: B Constrained

12:30 - 13:30 Lunch

13:30 - 14:30 Session 3

  • Invited Talk

14:30 - 15:15 Session 4

  • Thai Son Hoang: Generic Instantiation and Tool Support
  • Alexei Iliasov, Linas Laibinis, Elena Troubitsyna, Alexander Romanovsky: Support for Indexed Modules in Event-B

15:15 - 15:45 Break

15:45 - 17:15 Session 5

  • Andy Edmunds: Developments in Code Generation Tools for Event-B
  • Sergey Ostroumov , Leonidas Tsiopoulos , Juha Plosila , Kaisa Sere: Derivation of Structural VHDL from Component-Based Event-B Models
  • Vitaly Savicks, Michael Butler, Jens Bendisposto, John Colley: Co-simulation of Event-B and Continuous Models in Rodin
  • Adisak Intana, Michael R. Poppleton, and Geoff V. Merrett: Proof-based formal methods for WSN development with Simulation Approach


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_2013&oldid=8948’