Event-B Day 2016 in Tokyo
Event-B is a formal method for the system level modelling and analysis of dependable applications. It is supported by an open and extendable Eclipse-based toolset called Rodin, which has been developed in a series of European projects. This one day event aims to bring the community of Event-B/Rodin users and developers together to discuss new and emerging issues in applying and advancing both the Event-B method and the Rodin platform as well as address challenges that industrial takers are facing while deploying them.
Program
| 8:55-9:00 | Welcome from the organizers |
| 9:00-10:30 | Jean-Raymond Abrial (France) Formal proof of the Weak Goodstein Theorem Yamine Ait Ameur (IRIT / INPT-ENSEEIHT, France) Correct Refinement of Continuous Models Hironobu Kuruma (Hitachi, Ltd., Japan) Crossed-Project Reference for Modular Modeling |
| 10:30-10:50 | Coffee Break |
| 10:50-12:20 | Marc Frappier (Université de Sherbrooke, Canada) Generating Vulnerability Tests for Java Card Structural Constraints J Paul Gibson (Telecom Sud Paris, France) When Students Choose to Use Event-B in their Software Engineering Projects Alexei Iliasov (Newcastle University, UK) Verifying Paxos protocol in Event-B |
| 12:20-13:20 | Lunch |
| 13:20-14:50 | Tsutomu Kobayashi (The University of Tokyo, Japan) Event-B Refinement Restructuring and its Applications Thai Son Hoang (University of Southampton, UK) Theory Plug-in for Rodin 3 Mamoun Filali Amine (IRIT, France) Modeling and Verifying Event-B Transformations in Event-B |
| 14:50-15:10 | Coffee Break |
| 15:10-16:40 | Elena Troubitsyna (Abo Akademi, Finland) Towards Security-Explicit Formal Modelling of Safety-Critical Systems Paulius Stankaitis (Newcastle University, UK) Automating Verification of Event-B Models Rajiv Murali (Heriot-Watt University, UK) A Formal Approach to Use Case Driven Testing |
| 16:40-17:00 | Closing Discussion, Wrap-up |
Proceedings
Proceedings are published as a technical report at The Newcastle University.
The full versions of the following papers are published by ACM CoRR
- Paulius Stankaitis, Alexei Iliasov, David Adjepon-Yamoah, Alexander Romanovsky: Automating Verification of Event-B Models. CoRR abs/1611.02923 (2016)
- Jean-Raymond Abrial. Formal Proof of the Weak Goodstein Theorem. CoRR abs/1701.01673 (2016)
- Jean-Paul Bodeveix, Mamoun Filali, Mohamed Tahar Bhiri, Badr Siala. An Event-B framework for the validation of Event-B refinement plugins. CoRR abs/1701.00960 (2017)
- Paul Gibson. When Students Choose to Use Event-B in their Software Engineering Projects. CoRR abs/1611.10160 (2016)
- Thai Son Hoang, Laurent Voisin, Asieh Salehi, Michael Butler, Toby Wilkinson, Nicolas Beauger. Theory Plug-in for Rodin 3.x. CoRR abs/1701.08625 (2017)
Registration / Call for Presentations
Participation in the event is open. Please register with the form:
We are very much welcome participants who would like to present their work on the relevant topics. Register the title/abstract from the above link. We will contact the presenter about the acceptance of presentation.
The plan is to publish brief papers summarising the talks in the ACM CoRR repository and in the Proceedings to be submitted as a Technical Report at Newcastle University (UK).
Organizers
Alexander Romanovsky (Newcastle University, UK)
Fuyuki Ishikawa (National Institute of Informatics, Japan)
Contact : f-ishikawa <AT> nii.ac.jp