Rigorous State-Based Methods: 8th International Conference, ABZ 2021, Ulm, Germany, June 9–11, 2021, Proceedings

Description

This book constitutes the proceedings of the 8th International Conference on Rigorous State-Based Methods, ABZ 2021, which was planned to take place in Ulm, Germany, during June 6-11, 2021. The conference changed to an online format due to the COVID-19 pandemic. The 6 full and 8 short papers included in this volume were carefully reviewed and selected from 18 submissions. The proceedings also include 3 PhD symposium contributions. They deal with state-based and machine-based formal methods, mainly Abstract State Machines (ASM), Alloy, B, TLA+, VDM, and Z. Preface Organization Contents Regular Research Articles Unbounded Barrier-Synchronized Concurrent ASMs for Effective MapReduce Processing on Streams • Zilinghan Li, Shilan He, Yiqing Du, Senén González, and Klaus-Dieter Schewe Towards ASM-Based Automated Formal Verification of Security Protocols • Chiara Braghin, Mario Lilli, and Elvinia Riccobene Verifying System-Level Security of a Smart Ballot Box • Dana Dghaym, Thai Son Hoang, Michael Butler, Runshan Hu, Leonardo Aniello, and Vladimiro Sassone Proving the Safety of a Sliding Window Protocol with Event-B • Sophie Coudert Event-B Formalization of Event-B Contexts • Jean-Paul Bodeveix and Mamoun Filali Validation of Formal Models by Timed Probabilistic Simulation • Fabian Vu, Michael Leuschel, and Atif Mashkoor Short Articles Sterling: A Web-Based Visualizer for Relational Modeling Languages • Tristan Dyer and John Baugh Extending ASMETA with Time Features • Andrea Bombarda, Silvia Bonfanti, Angelo Gargantini, and Elvinia Riccobene About the Concolic Execution and Symbolic ASM Function Promotion in CASM • Philipp Paulweber, Jakob Moosbrugger, and Uwe Zdun Towards Refinement of Unbounded Parallelism in ASMs Using Concurrency and Reflection • Fengqing Jiang, Neng Xiong, Xinyu Lian, Senén González, and Klaus-Dieter Schewe The CamilleX Framework for the Rodin Platform • Thai Son Hoang, Colin Snook, Dana Dghaym, Asieh Salehi Fathabadi, and Michael Butler Extensible Record Structures in Event-B • Asieh Salehi Fathabadi, Colin Snook, Thai Son Hoang, Dana Dghaym, and Michael Butler Formalizing and Analyzing System Requirements of Automatic Train Operation over ETCS Using Event-B • Robert Eschbach Automatic Transformation of SysML Model to Event-B Model for Railway CCS Application • Shubhangi Salunkhe, Randolf Berglehner, and Abdul Rasheeq Short Articles of the PhD-Symposium (Work in Progress) Formal Meta Engineering Event-B: Extension and Reasoning The EB4EB Framework • Peter Riviere A Modeling and Verification Framework for Security Protocols • Mario Lilli Formalizing the Institution for Event-B in the Coq Proof Assistant • Conor Reynolds Author Index