Abstract State Machines, Alloy, B, TLA, VDM, and Z

Front Matter ....Pages I-XIV
Front Matter ....Pages 1-1
 ABZ Languages and Tools in Industrial-Scale Application  (Janet Barnes, Jonathan Hammond, Angela Wallenburg, Thomas Wilson)....Pages 3-15
 Distributed Adaptive Systems  (Klaus-Dieter Schewe, Flavio Ferrarotti, Loredana Tec, Qing Wang)....Pages 16-30
 On B and Event-B: Principles, Success and Challenges  (Jean-Raymond Abrial)....Pages 31-35
Front Matter ....Pages 37-37
 CASM-IR: Uniform ASM-Based Intermediate Representation for Model Specification, Execution, and Transformation  (Philipp Paulweber, Emmanuel Pescosta, Uwe Zdun)....Pages 39-54
 Event-B Expression and Verification of Translation Rules Between SysML/KAOS Domain Models and B System Specifications  (Steve Jeffrey Tueno Fotso, Amel Mammar, Régine Laleau, Marc Frappier)....Pages 55-70
 A Translation from Alloy to B  (Sebastian Krings, Joshua Schmidt, Carola Brings, Marc Frappier, Michael Leuschel)....Pages 71-86
Front Matter ....Pages 87-87
 Extracting Symbolic Transitions from TLA\(^{+}\) Specifications  (Jure Kukovec, Thanh-Hai Tran, Igor Konnov)....Pages 89-104
 Systematic Generation of Non-equivalent Expressions for Relational Algebra  (Kaiyuan Wang, Allison Sullivan, Manos Koukoutos, Darko Marinov, Sarfraz Khurshid)....Pages 105-120
 Solver-Based Sketching of Alloy Models Using Test Valuations  (Kaiyuan Wang, Allison Sullivan, Darko Marinov, Sarfraz Khurshid)....Pages 121-136
Front Matter ....Pages 137-137
 Abstract State Machines with Exact Real Arithmetic  (Christoph Beierle, Klaus-Dieter Schewe)....Pages 139-154
 Proof-Based Approach to Hybrid Systems Development: Dynamic Logic and Event-B  (Guillaume Dupont, Yamine Aït-Ameur, Marc Pantel, Neeraj Kumar Singh)....Pages 155-170
 Issues in Automated Urban Train Control: ‘Tackling’ the Rugby Club Problem  (Richard Banach)....Pages 171-186
Front Matter ....Pages 187-187
 Clarification of Ambiguity for the Simple Authentication and Security Layer  (Farah Al-Shareefi, Alexei Lisitsa, Clare Dixon)....Pages 189-203
 Systematic Refinement of Abstract State Machines with Higher-Order Logic  (Flavio Ferrarotti, Senén González, Klaus-Dieter Schewe, José María Turull-Torres)....Pages 204-218
 Refinement of Timing Constraints for Concurrent Tasks with Scheduling  (Chenyang Zhu, Michael Butler, Corina Cirstea)....Pages 219-233
 Verifiable Code Generation from Scheduled Event-B Models  (Mohammadsadegh Dalvandi, Michael Butler, Abdolbaghi Rezazadeh, Asieh Salehi Fathabadi)....Pages 234-248
Front Matter ....Pages 249-249
 The Hybrid ERTMS/ETCS Level 3 Case Study  (Thai Son Hoang, Michael Butler, Klaus Reichl)....Pages 251-261
 Modeling the Hybrid ERTMS/ETCS Level 3 Standard Using a Formal Requirements Engineering Approach  (Steve Jeffrey Tueno Fotso, Marc Frappier, Régine Laleau, Amel Mammar)....Pages 262-276
 Modelling the Hybrid ERTMS/ETCS Level 3 Case Study in Spin  (Paolo Arcaini, Pavel Ježek, Jan Kofroň)....Pages 277-291
 Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains  (Dominik Hansen, Michael Leuschel, David Schneider, Sebastian Krings, Philipp Körner, Thomas Naulin et al.)....Pages 292-306
 Validating the Hybrid ERTMS/ETCS Level 3 Concept with Electrum  (Alcino Cunha, Nuno Macedo)....Pages 307-321
 The ABZ-2018 Case Study with Event-B  (Jean-Raymond Abrial)....Pages 322-337
 Diagram-Led Formal Modelling Using iUML-B for Hybrid ERTMS Level 3  (Dana Dghaym, Michael Poppleton, Colin Snook)....Pages 338-352
 An Event-B Model of the Hybrid ERTMS/ETCS Level 3 Standard  (Amel Mammar, Marc Frappier, Steve Jeffrey Tueno Fotso, Régine Laleau)....Pages 353-366
Front Matter ....Pages 367-367
 AsmetaA: Animator for Abstract State Machines  (Silvia Bonfanti, Angelo Gargantini, Atif Mashkoor)....Pages 369-373
 Formal Specification of the Semantics of Control State Diagrams  (Markus Leitz, Alexander Raschke)....Pages 374-379
 Capturing Membrane Computing by ASMs  (Klaus-Dieter Schewe, Loredana Tec, Qing Wang)....Pages 380-385
 Towards Creating a DSL Facilitating Modelling of Dynamic Access Control in Event-B  (Inna Vistbakka, Mikhail Barash, Elena Troubitsyna)....Pages 386-391
 State-Based Formal Methods in Scientific Computation  (John Baugh, Tristan Dyer)....Pages 392-396
 Proposition of an Action Layer for Electrum  (Julien Brunel, David Chemouil, Alcino Cunha, Thomas Hujsa, Nuno Macedo, Jeanne Tawa)....Pages 397-402
 Insulin Pump: Modular Modeling of Hybrid Systems Using Event-B  (Wen Su, Jinxin Chen, Shehroz Khan)....Pages 403-408
 An Automation-Friendly Set Theory for the B Method  (Guillaume Bury, Simon Cruanes, David Delahaye, Pierre-Louis Euvrard)....Pages 409-414
 Teaching an Old Dog New Tricks  (Lilian Burdy, David Deharbe)....Pages 415-419
 Modelling Dynamic Data Structures with the B Method  (Frédéric Badeau, Vincent Lacroix, Vincent Monfort, Laurent Voisin, Christophe Métayer)....Pages 420-424
 On the Importance of Explicit Domain Modelling in Refinement-Based Modelling Design. Experiments with Event-B  (Yamine Aït-Ameur, Idir Ait-Sadoune, P. Casteran, Paul Gibson, K. Hacid, S. Kherroubi et al.)....Pages 425-430
Back Matter ....Pages 431-432