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 DLD4,×
- 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