Event-B Day 2016 in Tokyo

Nov 21 2016

20F Meeting Room, National Institute of Informatics, Tokyo, Japan

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.


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 are published as a technical report at The Newcastle University.

The full versions of the following papers are published by ACM CoRR

Registration / Call for Presentations

Participation in the event is open. Please register with the form:

Registration 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).


Alexander Romanovsky (Newcastle University, UK)

Fuyuki Ishikawa (National Institute of Informatics, Japan)

Contact : f-ishikawa <AT> nii.ac.jp