Modeling Distributed Algorithms by Abstract State Machines Compared to Petri Nets
A Universal Control Construct for Abstract State Machines
Encoding TLA+ into Many-Sorted First-Order Logic
Proving Determinacy of PharOS in TLA+
A Rigorous Correctness Proof for Pastry
Enabling Analysis for B and Event-B
A Compact Encoding of Sequential ASMs in Event-B
Proof Assisted Symbolic Model Checking for B and Event-B
On Component-based Reuse for Event-B
Using B and ProB for Data Validation Projects
Generating Event-B Specifications from Algorithm Descriptions
Formal Proofs of Termination Detection for Local Computations by Refinement-Based Compositions
How to Select the Suitable Formal Method for an Industrial Application: A Survey
Unified Syntax for Abstract State Machines
A Relational Encoding for a Clash-Free Subset of ASMs
Towards an ASM Thesis for Reflective Sequential Algorithms
A Model-based Transformation Approach to Reuse and Retarget CASM Specifications
Modeling a Discrete Wet-Dry Algorithm for Hurricane Storm Surge in Alloy
`The Tinker' for Rodin
A Graphical Tool for Event Refinement Structures in Event-B
Rodin Platform Why3 plug-in
Semi-Automated Design Space Exploration for Formal Modelling
Handling Continuous Functions in Hybrid Systems Reconfigurations: A Formal Event-B Development
UC-B: Use Case Modelling with Event-B
Interactive Model Repair by Synthesis
SysML2B: Automatic Tool for B Project Graphical Architecture Design using SysML
Mechanized Refinement of Communication Models with TLA+
A Super Industrial Application of PSGraph
The Hemodialysis Machine Case Study
How to Assure Correctness and Safety of Medical Software: The Hemodialysis Machine Case Study
Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotionStudio, and Co-simulation
Hemodialysis Machine in Hybrid Event-B
Modeling a Hemodialysis Machine using Algebraic State-Transition Diagrams and B-like Methods
Modelling the Haemodialysis Machine with Circus.