Programme

Springer LNCS Volume 10817 is available online: LNCS volume for ABZ

Tuesday 5 June

Parallel Workshops: Rodin 2018 and SETS 2018

8:30-9:00 Registration

9:00-9:30 Opening and Welcome

9:30-10:30 Invited Talk

• Michael Leuschel. Solving Set Constraints in B and Event-B: Foundations and Applications ( abstract )( slides )

10:30-11:00 Break

Rodin  2018 Workshop Programme

SETS 2018 Workshop Programme

11:00-12:20 Modelling Tools and Extensions Dana Dghaym, Thai Son Hoang, Colin Snook and Michael Butler. The eXtended Event-B Plug-in XEvent-B Paulius Stankaitis, Alexei Iliasov, Tsutomu Kobayashi, Alexander Romanovsky and Fuyuki Ishikawa. A Framework for Developing Distributed Protocols with Event-B James Snook. A New Language to Construct Algebraic Hierarchies for Event-B G. Dupont, Y. Aït-Ameur, M. Pantel, and N. K. Singh. On the use of the Theory Plug-In to define theories for differential equations 12:20-13:30 Lunch 13:30 -15:20 User Reports and Methods John Colley and Michael Butler. Using Formal Methods to demonstrate Compliance with System Requirements for DO-178C_DO-333 Giles Howard, Michael Butler, John Colley and Vladimiro Sasson. Supporting a systems-theoretic co-analysis of safety & security using Event-B & Rodin Ilya Shchepetkov. Using Refinement in Formal Development of OS Security Policy Model Martin Kubisch and Colin Snook. Security Analysis of the 'Touch And Go Assistant' for Aircraft Turn-around Keming Wang and Zheng Wang.  Modeling and Verification of Railway Level Crossing Management System Using Event-B 15:20-16:00 Break 16:00-17:40 Code Generation and Testing Alexei Iliasov. Safecap generic verification framework Mohammadsadegh Dalvandi, Asieh Salehi Fathabadi and Michael Butler. A Report on PRiME Code Generation Activities Ahmed Al-Brashdi, Michael Butler and Abdolbaghi Rezazadeh. UB2DB Rodin Plug-in for Automated Database Code Generation Tomas Fischer. Formal Model Validation through Acceptance Tests Rupert Schlick and Thorsten Tarrach. Mutation-based test-case generation for Event-B

More details can be found here 11:00-12:20 Session 1 Domenico Cantone and Alberto Policriti. Encoding Sets as Real Numbers Maximiliano Cristiá and Gianfranco Rossi Programming in Java with Restricted Intensional Sets Catherine Dubois and Sulyvan Weppe. Towards Coq Formalisation of {log} Set Constraints Resolution 12:20-13:50 Lunch 13:50 -15:30 Session 2 Alberto Casagrande, Francesco Di Cosmo and Eugenio G. Omodeo. Proof-checking and graph connectivity with AEtnaNova Domenico Cantone, Marianna Nicolosi-Asmundo and Daniele Francesco Santamaria. A set-based reasoner for the description logic DL D 4,× Olivier Hermant. Polarized Rewriting and Tableaux in B Set Theory Vincent Semeria. HilbertProofs

18:00-19:30 Guided walk around the historic city walls and vaults

19:30-22:30 Meet somewhere for dinner (Not included in the registration fee)

Wednesday 6 June

8:30-09:00 Registration

9:00-10:00 Invited Talk:

• Janet Barnes and Angela Wallenburg. Formal Methods Considered Normal ( slides )

10:00-10:30 Short Talks:

• Silvia Bonfanti, Angelo Gargantini and Atif Mashkoor. AsmetaA: Animator for Abstract State Machines
• Markus Leitz and Alexander Raschke. Formal Specification of the Semantics of Control State Diagrams

10:30-11:00 Break

11:00 – 12:30 Translation and Transformation:

• Philipp Paulweber, Emmanuel Pescosta and Uwe Zdun. CASM-IR: Uniform ASM-Based Intermediate Representation for Model Specification, Execution, and Transformation
• Tueno Fotso Steve Jeffrey, Amel Mammar, Regine Laleau and Marc Frappier. Event-B Expression and Validation of Translation Rules Between SysML/KAOS Domain Models and B System Specifications
• Sebastian Krings, Joshua Schmidt, Carola Brings, Marc Frappier and Michael Leuschel. A Translation from Alloy to B

12:30-14:00 Lunch

14:00 -15:00 Invited Talk :

• Klaus-Dieter Schewe. Distributed Adaptive Systems - Theory, Specification, Reasoning ( slides )

15:00 -15:30 Short Talks:

• Klaus-Dieter Schewe, Loredana Tec and Qing Wang. Capturing Membrane Computing by ASMs
• Inna Vistbakka, Mikhail Barash and Elena Troubitsyna. Towards Creating a DSL Facilitating Modelling of Dynamic Access Control in Event-B

15:30-16:00 Break

16:00 – 17:30: Analysis and Tests:

• Jure Kukovec, Thanh Hai Tran and Igor Konnov. Extracting Symbolic Transitions from TLA+ Specifications
• Kaiyuan Wang, Allison Sullivan, Manos Koukoutos, Darko Marinov and Sarfraz Khurshid. Systematic Generation of Non-Equivalent Expressions for Relational Algebra
• Kaiyuan Wang, Allison Sullivan, Darko Marinov and Sarfraz Khurshid. Solver-based Sketching of Alloy Models using Test Valuations

17:30 ABZ Steering Committee meeting

Thursday 7 June

9:00-10:00 Invited Talk:

• Daniel Jackson. How Bugs Led Us Astray ( slides )

10:00-10:30 Short Talks:

• John Baugh and Tristan Dyer. State-Based Formal Methods in Scientific Computation
• Julien Brunel, David Chemouil, Alcino Cunha, Thomas Hujsa, Nuno Macedo and Jeanne Tawa. Proposition of an Action Layer for Electrum

10:30-11:00 Break

11:00 – 12:30 Reals and Hybrid Systems:

• Christoph Beierle and Klaus-Dieter Schewe. Abstract State Machines with Exact Real Arithmetic
• Guillaume Dupont, Yamine Aït-Ameur, Marc Pantel and Neeraj Kumar Singh. Proof-based approach to hybrid systems development: Dynamic Logic and Event-B
• Richard Banach. Issues in Automated Urban Train Control: 'Tackling' the Rugby Club Problem

12:30-14:00 Lunch

14:00-16:00 Refinement:

• Farah Al-Shareefi, Alexei Lisitsa and Clare Dixon. Clarification of Ambiguity for the Simple Authentication and Security Layer
• Flavio Ferrarotti, Senén González, Klaus-Dieter Schewe and Jose Maria Turull Torres. Systematic Refinement of Abstract State Machines with Higher-Order Logi
• Chenyang Zhu, Michael Butler and Corina Cirstea. Refinement of Timing Constraints for Concurrent Tasks with Queue Based Scheduling
• Mohammadsadegh Dalvandi, Michael Butler, Abdolbaghi Rezazadeh and Asieh Salehi Fathabadi. Verifiable Code Generation from Scheduled Event-B Models

16:30 – 23:00 Excursion and Dinner

Friday 8 June

9:00-10:00 Invited Talk:

• Jean-Raymond Abrial. On B and Event-B: Principles, Success and Challenges ( slides )

10:00-10:30 Panel Discussion:

• 25 Years since the METEOR project started using B

10:30-11:00 Break

11:00-12:30 Hybrid ERTMS Case Study Session 1:

• Thai Son Hoang, Klaus Reichl, Michael Butler, Case Study Overview (15 mins)
• Amel Mammar, Marc Frappier, Regine Laleau and Steve Jeffrey Tueno Fotso. An Event-B Model of the ERTMS/ETCS Level 3 Standard (25 mins)
• Paolo Arcaini, Pavel Ježek and Jan Kofron. Modelling the Hybrid ERTMS/ETCS Level 3 Case Study in Spin (25 mins)
• Dominik Hansen, Michael Leuschel, Sebastian Krings, Philipp Koerner, David Schneider, Thomas Naulin, Frank Skowron and Nader Nayeri. Using a B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains (25 mins)

12:30-13:50 Lunch

13:50 -15:30 Hybrid ERTMS Case Study Session 2:

• Alcino Cunha and Nuno Macedo. Validating the Hybrid ERTMS/ETCS Level 3 Concept with Electrum (25 mins)
• Jean-Raymond Abrial. The ABZ-2018 Case Study with Event-B (25 mins)
• Dana Dghaym, Mike Poppleton and Colin Snook. Diagram-led formal modelling using iUML-B for Hybrid ERTMS Level 3 (25 mins)
• Tueno Fotso Steve Jeffrey, Marc Frappier, Regine Laleau and Amel Mammar. Modeling the Hybrid ERTMS/ETCS Level 3 Standard Using a Formal Requirements Engineering Approach (25 mins)

15:30-16:00 Break

16:00-17:15  Short Talks:

• Jinxin Chen, Wen Su and Shehroz Khan. Insulin Pump: Modular Modeling of Hybrid Systems Using Event-B
• Guillaume Bury, Simon Cruanes, David Delahaye and Pierre-Louis Euvrard. An Automation-Friendly Set Theory for the B Method
• Lilian Burdy and David Deharbe. Teaching an Old Dog New Tricks: The Drudges of the Interactive Prover in Atelier B
• Frédéric Badeau, Vincent Lacroix, Vincent Monfort, Laurent Voisin and Christophe Métayer. Modelling Dynamic Data Structures with the B Method
• Yamine Ait Ameur, Dominique Mery, Idir Ait Sadoune, Neeraj Singh, Laurent Voisin and Gibson Paul. On the importance of explicit domain modelling in refinement-based modelling design. Experiments with Event-B

17:15 Close