You are here: HomeABZ 2016Program

Programme ABZ 2016

Monday, May 23

Rodin Workshop 2016

09:00 - 10:30Workshop Session 1A: RODIN Workshop 1
Meta-Predicates for Rodin - Sebastian Krings
A Rodin plug-in for constructing reusable schematic lemmas - Alexei Iliasov, Paulius Stankaitis, David Adjepon-Yamoah, and Alexander Romanovsky
Event-B Specification Templates for Defining Domain Specific Languages - Ulyana Tikhonova
10:30 - 11:00Break
11:00 - 12:30Workshop Session 2A: RODIN Workshop 2
Towards Modular Development in Event-B - Thai Son Hoang, Hironobu Kuruma, and Michael Butler
Crossed-Project Reference for Managing Model Variations - Hironobu Kuruma and Thai Son Hoang
SliceAndMerge: A Rodin Plug-in for Refactoring Refinement Structure of Event-B Machines - Tsutomu Kobayashi, Aivar Kripsaar, Fuyuki Ishikawa and Shinichi Honiden
12:30 - 14:00Lunch
14:00 - 15:30Workshop Session 3A: RODIN Workshop 3
Rodin in the field of railway system engineering - Tomas Fischer
Building Event-B Interlocking Theories: Lessons Learned using the Theory Plug-in - Yoann Guyot, Renaud De Landtsheer, and Christophe Ponsard
Theory plug-in for Rodin 3.x - Thai Son Hoang, Asieh Salehi, Michael Butler, and Laurent Voisin
15:30 - 16:00Break
16:00 - 17:30Workshop Session 4A: RODIN Workshop 4
Extending Code Generation to Support Platform-Independent Event-B Models - Asieh Salehi, Michael Butler, and Colin Snook
Using Rodin and BMotionStudio for Public Engagement - Dana Dghaym, Asieh Salehi and Colin Snook
Translating SCXML Statecharts to iUML-B State-machines - Karla Morris and Colin Snook

Tutorial Session 2016

09:00 - 10:30Tutorial Session 1B: Tutorial 1
The Formalisation of the Business Process Modelling and Notation - Bernhard Thalheim, Felix Kossak
10:30 - 11:00Break
11:00 - 12:30Tutorial Session 2B: Tutorial 1 (cont.)
The Formalisation of the Business Process Modelling and Notation - Bernhard Thalheim, Felix Kossak
12:30 - 14:00Lunch
14:00 - 15:30Tutorial Session 3B: Tutorial 2
Modelling Hybrid and Cyberphysical Systems the Hybrid Event-B Way - Richard Banach
15:30 - 16:00Break
16:00 - 17:30Tutorial Session 4B: Tutorial 2 (cont.)
Modelling Hybrid and Cyberphysical Systems the Hybrid Event-B Way - Richard Banach

Tuesday, May 24

ABZ Session 1: B / Event-B

Session Chair: Stephan Merz

09:00 - 10:30Proof Assisted Symbolic Model Checking for B and Event-B - Sebastian Krings and Michael Leuschel
Handling continuous functions in hybrid systems reconfigurations : a formal Event-B development (Short Paper) - Guillaume Babin, Yamine Ait Ameur, Neeraj Singh and Marc Pantel
'The Tinker' for Rodin (Short Paper) - Yibo Liang, Yuhui Lin and Gudmund Grov
A Graphical Tool for Event Refinement Structures in Event-B (Short Paper) - Dana Dghaym, Matheus Garay Trindade, Michael Butler and Asieh Salehi Fathabadi
10:30 - 11:00Break

ABZ Session 2: Analysis with B and Event-B

Session Chair: Yamine Ait Ameur

11:00 - 12:30Enabling Analysis for B and Event-B - Ivaylo Dobrikov and Michael Leuschel
Formal Proofs of Termination Detection for Local Computations by Refinement-Based Compositions - Maha Boussabbeh, Mohamed Tounsi, Mohamed Mosbah and Ahmed Hadj Kacem
Generating Event-B Specifications from Algorithm Descriptions - Joy Clark, Jens Bendisposto, Stefan Hallerstede, Dominik Hansen and Michael Leuschel
12:30 - 14:00Lunch

ABZ Session 3: Mini Symposium on the Occasion of the 70th Birthday of Egon Börger

Session Chair: Klaus-Dieter Schewe

14:00 - 16:00Laudatio - Uwe Glässer, Vincenzo Gervasi, Elvinia Riccobene
Keynote: Comparing Abstract State Machine Models with Petri Nets for Distributed Algorithms - Egon Börger
16:00 - 16:30Break

ABZ Session 4: Mini Symposium on the Occasion of the 70th Birthday of Egon Börger (cont.)

Session Chair: Elvinia Riccobene

16:30 - 18:00A Universal Control Construct for Abstract State Machines - Michael Stegmaier, Marcel Dausend, Alexander Raschke and Matthias Tichy
Unified Syntax for Abstract State Machines (Short Paper) - Paolo Arcaini, Silvia Bonfanti, Marcel Dausend, Angelo Gargantini, Atif Mashkoor, Alexander Raschke, Elvinia Riccobene, Patrizia Scandurra and Michael Stegmaier
A Relational Encoding for a Clash-Free Subset of ASMs (Short Paper) - Gidon Ernst, Gerhard Schellhorn, Jörg Pfähler and Wolfgang Reif
Towards an ASM Thesis for Reflective Sequential Algorithms (Short Paper) - Flavio Ferrarotti, Loredana Tec and José María Turull Torres

ABZ Steering Committee Meeting

18:15 - 19:00ABZ Steering Committee Meeting (Open to everyone)

Wednesday, May 25

ABZ Session 5: Hybrid / Cyberphysical Systems

Session Chair: Michael Butler

09:00 - 10:30Keynote: How to Brew Your Own Hybrid / Cyberphysical Formalism - Richard Banach
10:30 - 11:00Break

ABZ Session 6: Formal Methods and Applications

Session Chair: Dominique Méry

11:00 - 13:00On Component-based Reuse for Event-B - Andrew Edmunds, Colin Snook and Marina Waldén
How to Select the Suitable Formal Method for an Industrial Application: A Survey - Felix Kossak and Atif Mashkoor
A super industrial application of PSGraph (Short Paper) - Yuhui Lin, Gudmund Grov, Colin O'Halloran and Priiya G
Modeling a Discrete Wet-Dry Algorithm for Hurricane Storm Surge in Alloy (Short Paper) - John Baugh and Alper Altuntas
SysML2B: automatic tool for B project graphical architecture design using SysML (Short Paper) - David Mentré
13:00 - 14:30Lunch
14:30 - 23:00Excursion, Conference Dinner

Thursday, May 26

ABZ Session 7: TLA+

Session Chair: Michael Leuschel

09:00 - 10:30Encoding TLA+ into Many-Sorted First-Order Logic - Stephan Merz and Hernán Vanzetto
A Rigorous Correctness Proof for Pastry - Noran Azmy, Stephan Merz and Christoph Weidenbach
Proving Determinacy of PharOS in TLA+ - Selma Azaiez, Damien Doligez, Jael Kriener, Matthieu Lemerre and Stephan Merz
10:30 - 11:00Break

ABZ Session 8: Mini Symposium on B / Event-B in Industry

Session Chair: Gudmund Grov

11:00 - 12:30     Keynote: Atelier B Has Turned Twenty - Thierry Lecomte
12:30 - 14:00Lunch

ABZ Session 9: Mini Symposium on B / Event-B in Industry (cont.)

Session Chair: Loredana Tec

14:00 - 15:30Keynote: Modeling Safety Critical Railway Applications - an Industrial Experience - Klaus Reichl
15:30 - 16:00Break

ABZ Session 10: B, Event-B

Session Chair: Colin Snook

16:00 - 17:30Using B and ProB for Data Validation Projects - Dominik Hansen, David Schneider and Michael Leuschel
Semi-Automated Design Space Exploration for Formal Modelling (Short Paper) - Gudmund Grov, Andrew Ireland, Maria Teresa Llano Rodriguez, Peter Kovacs, Simon Colton and Jeremy Gow
Rodin Platform Why3 plug-in (Short Paper) - Alexei Iliasov, Paulius Stankaitis and Alexander Romanovsky
UC-B: Use Case Modelling with Event-B (Short Paper) - Rajiv Murali, Andrew Ireland and Gudmund Grov

Friday, May 27

ABZ Session 11: Case Study Track 1

Session Chair: Miklós Biró

09:00 - 10:30The Hemodialysis Machine Case Study - Atif Mashkoor
How to assure correctness and safety of medical software: the Hemodialysis Machine Case Study - Paolo Arcaini, Silvia Bonfanti, Angelo Gargantini and Elvinia Riccobene
Modelling the Haemodialysis Machine with Circus - Andrew Butterfield and Artur Oliveira Gomes
10:30 - 11:00Break

ABZ Session 12: Case Study Track 2

Session Chair: Atif Mashkoor

11:00 - 12:30Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotionStudio, and Co-simulation - Thai Son Hoang, Colin Snook, Lukas Ladenberger and Michael Butler
Hemodialysis Machine in Hybrid Event-B - Richard Banach
Modeling a Hemodialysis Machine using Algebraic State-Transition Diagrams and B-like Methods - Thomas Fayolle, Marc Frappier, Frederic Gervais and Regine Laleau
12:30 - 14:00Lunch

ABZ Session 13: Formal Methods Integration

Session Chair: Flavio Ferrarotti

14:00 - 15:30A compact encoding of sequential ASMs in Event-B - Michael Leuschel and Egon Börger
Interactive Model Repair by Synthesis (Short Paper) - Joshua Schmidt, Sebastian Krings and Michael Leuschel
Mechanized Refinement of Communication Models with TLA+ (Short Paper) - Florent Chevrou, Aurélie Hurault and Philippe Queinnec
A Model-based Transformation Approach to Reuse and Retarget CASM Specifications (Short Paper) - Philipp Paulweber and Uwe Zdun