ABZ 2024 – 10th International Conference on Rigorous State Based Methods
Workshop Program
June, 25th
Conference Room: Room 5
Time
Talk
Topic
Session Chair: Laurent Voisin
09:00 - 09:30
What's new in Rodin 3.9 and the Theory plug-in
Guillaume Verdier, Laurent Voisin, Idir Ait-Sadoune
Guillaume Verdier, Laurent Voisin, Idir Ait-Sadoune
Rodin Workshop
09:30 - 10:00
Semantics formalisation: Some experience with the Theory Plug-in
Thai Son Hoang, Laurent Voisin, Colin Snook, Karla Vanessa Morris Wright, Michael Butler
Thai Son Hoang, Laurent Voisin, Colin Snook, Karla Vanessa Morris Wright, Michael Butler
Rodin Workshop
10:00 - 10:30
Validation of Domain and Meta Models: From Event-B Theories to Practice
Michael Leuschel, Yamine Ait-Ameur, Guillaume Dupont, Peter Riviere, Neeraj Kumar Singh
Michael Leuschel, Yamine Ait-Ameur, Guillaume Dupont, Peter Riviere, Neeraj Kumar Singh
Rodin Workshop
10:30 - 11:00
Coffee break
Session Chair: Son Thai Hoang
11:00 - 11:30
Developing the UML-B modelling tools
Colin Snook
Colin Snook
Rodin Workshop
11:30 - 12:00
Correct-by-Construction Synthesis of Sequential Algorithms
Dominique Cansell, Neeraj Kumar Singh
Dominique Cansell, Neeraj Kumar Singh
Rodin Workshop
12:00 - 12:30
Schemata of Recursive Functions and Iterative Algorithms
Dominique Cansell
Dominique Cansell
Rodin Workshop
12:30 - 14:00
Lunch break
Session Chair: David Geleßus
14:00 - 14:30
Validation of Domain and Meta Models: From Event-B Theories to Practice
Michael Leuschel
Michael Leuschel
IVOIRE Workshop
14:30 - 15:00
IVOIRE Project: Results and Insights
Atif Mashkoor
Atif Mashkoor
IVOIRE Workshop
15:00 - 15:30
Validation Obligations in Practice
Fabian Vu
Fabian Vu
IVOIRE Workshop
15:30 - 16:00
Coffee break
Session Chair: Fabian Vu
16:00 - 16:30
An Exercise in Multi-modeling
Jean-Pierre Jacquot
Jean-Pierre Jacquot
IVOIRE Workshop
16:30 - 17:00
Validation Obligations Manager
David Geleßus
David Geleßus
IVOIRE Workshop
17:00 - 17:30
What Should I Verify?
Marie Farrell
Marie Farrell
IVOIRE Workshop
17:30 - 18:00
Discussion and conclusion
IVOIRE Workshop
19:00 - 21:00
Welcome Reception (conference venue)
Conference Program
June, 26th
Conference Room: Room 5
Time
Talk
Topic
Session Chair: Elvinia Riccobene
09:00 - 09:15
Welcome Opening
09:15 - 10:15
Formal Methods and Tools applied in the railway domain
ABZ and other state-based formal methods and tools are successfully applied to the development of safety-critical systems for decades now, in particular in the transport domain, without a single language or tool emerging as the dominant solution for system design. Formal methods are highly recommended by the current safety standards in the railway industry, but railway engineers often lack the knowledge to transform their semi-formal models into formal models, with a precise semantics, to serve as input to formal methods tools. We share the results of performing empirical studies in the railway domain, including usability analyses of formal methods tools involving railway practitioners. We discuss, in particular with respect to railway systems and their modelling, our experiences in applying rigorous state-based methods and tools to a variety of case studies, for which we interacted with a number of companies from the railway domain. We report on lessons learned from these experiences and provide pointers to drive future research towards facilitating further synergies between - on the one hand - researchers and developers of ABZ and other state-based formal methods and tools, and - on the other hand - practitioners from the railway industry.Keynote
10:15 - 10:45
Coffee break
Session Chair: Michael Leuschel
10:45 - 11:15
Formal Modeling and Analysis of Apache Kafka in Alloy 6
Apache Kafka is a distributed, fault-tolerant and highly available open-source technology that utilizes the publish-subscribe communication model to stream large volumes of data. It is widely being used in various domains such as finance, entertainment, online education, and e-commerce for real-time data processing and analytics. This paper demonstrates an application of Alloy 6 - the latest version of Alloy with built-in temporal logic operators - to modeling and analysis of a complex distributed system like Kafka. The architecture and key operations of Kakfa are modeled, and its various properties, including fault-tolerance, data availability, service availability, consistency, and recoverability, are verified using the Alloy Analyzer. The result of the analysis provides insights into how Kafka maintains the properties that it claims to have, and the circumstances under which these properties may be violated.Modeling
11:15 - 11:45
Event-B Development of Modelling Human Intervention Request in Self-Driving Vehicle Systems
In the design of autonomous systems, seamless integration with human operators is crucial, particularly when humans are considered as a fail-safe for intervening in hazardous situations. This study presents an Event-B intervention timing pattern designed to include human drivers' responses when they act as fallback mechanisms in Self-Driving Vehicle (SDV) systems. The proposed pattern outlines specific timings for driver interventions following alerts from SDVs, offering a clear set of expectations and conditions for human drivers during these critical takeover instances. The usability of this pattern is demonstrated through a case study, highlighting its importance for situations that require interventions. Ultimately, it sheds light on the operational aspects of SDVs, ensuring a safe and orderly transition from automated to manual control.Modeling
11:45 - 12:05
An Event-B Formal Model for Access Control and Resource Management of Serverless Apps
Cloud computing technologies help developers build scalable distributed apps. Serverless architecture, or Function as a Service (FaaS), which separates app businesses into multiple functions, is one of the cloud-native architectures that has gained popularity. Those functions can be developed and deployed independently without provisioning in?frastructure. Despite the considerable advantages and increasing popularity of cloud?native apps, developers face many challenges when building their cloud?native applications. To ensure the robustness and security of cloud-native apps and protect crucial resources, the design and implementation of functions and associated access control systems play a pivotal role. In this paper, we have employed formal methods and tools to develop a set of patterns to help cloud-native application developers to design robust serverless apps. We have used Event-B and its associated toolset, Rodin, to construct these formal patterns and demonstrated how these patterns can be used in practical case studies.Modeling/Industrial
12:05 - 12:20
Designing Exception Handling using Event-B
Exception handling is a well-known error recovery approach employed to improve robustness of software. While programming languages offer exception handling for responding to detected failures, the design of exception handling is a complex task that needs designers’ insights and domain expertise to identify exceptions and recover from them to put the system back in a safe state. The challenge is to ensure that a complex closed system including controller and its environment remain in a safe state while undertaking abnormal state changes in the controller as part of its exception recovery process. Formal methods supporting excep- tion handling can address this complexity, by addressing it in the abstract design stages utilising mathematical modelling and proofs. Event-B is a state-based formal method for modelling and verifying the consistency of discrete systems. However it lacks support for explicit handling of exceptions. In this paper, we use UML-B state machines to support the identification and handling of exceptions, followed by verification of exception handler recovery mechanisms using the built-in model checker and prover in the Event-B toolset. We also discuss an implementation of the modelled exception handling in the 'C' programming language as a first stage towards automatic code generation of exception handlers.Modeling/Verification
12:30 - 14:00
Lunch break
Session Chair: Guillaume Dupont
14:00 - 14:30
Alloy Goes Fuzzy
Humans are good at understanding subjective or vague statements which, however, are hard to express in classic logic. Fuzzy logic is an evolution of classic logic that can cope with vague terms by handling degrees of truth and not just the crisp values true and false. Logic is the formal basis of computing, enabling the formal design of systems supported by tools such as model checkers and theorem provers. This paper shows how a model checker such as Alloy can evolve to handle both classic and fuzzy logic, enabling the specification of high-level quantitative relational models in the fuzzy domain. In particular, the paper showcases how QAlloy-F (a conservative, general-purpose quantitative extension to standard Alloy) can be used to tackle fuzzy problems, namely in the context of validating the design of fuzzy controllers. The evaluation of QAlloy-F against examples taken from various classes of fuzzy case studies shows the approach to be feasible.Theory Extension
14:30 - 15:00
Transpilation of Petri-nets into B: Shallow and Deep Embeddings
Petri-nets and their variants (Place/Transition nets, High-Level Petri Nets, etc) are widely used in the development of safety critical-systems. Their success is related to three major aspects: a formal semantics, a graphical syntax and the availability of verification tools. In our previous work we presented a new vision for the semantic definition of Petri-nets applying a Formal Model-Driven Engineering (FMDE) built on the B method. The approach is powered by Meeduse, a language workbench that we developed in order to formally instrument executable Domain-Specific Languages (xDSLs) by applying a deep embedding technique and the B method. However, because of the abstract nature of the underlying formal models, our deep embedding is suitable for the validation and verification activities at the design stage but not sufficient to generate code for target platforms. This paper advances our previous work with a shallow embedding technique taking benefit of the B method tools in order to safely synthesize executable Petri-net controllers that can be embedded in target platforms.Theory Extension
15:00 - 15:20
Property Ownership Formal Modelling Using Event-B and iUML-B
This paper introduces a novel approach to formal modelling and verification of ownership, addressing safety concerns in property transfer processes.The Event-B formal method, graphically represented using iUML-B notation, is used to establish a robust framework for modeling and verifying ownership systems. The verified Event-B model refines and enhances user requirements at the design stage before system implementation. The research focuses on property ownership within the legal framework of the Kingdom of Saudi Arabia, specifically property sales. The research uncovers that, despite conscientious efforts to scrutinise user requirements, the formal model development exposes limitations and inadequacies in the initial specifications. The verification process introduces essential requirements to mitigate potential fraudulent activities, enhancing the security and dependability of ownership claims.Modeling/Industrial
15:20 - 15:35
A Modeling and Verification Framework for Ethereum Smart Contracts
Blockchain has shown to be a versatile technology with applications ranging from financial services and supply chain management to healthcare, identity verification, and beyond. Thanks to the usage of smart contracts, blockchain can streamline and automate complex processes, eliminating the need for intermediaries and reducing administrative overhead. Smart contracts often handle valuable assets and execute critical functions, making them attractive targets for attackers. Thus, the need for secure and reliable smart contracts is crucial. The long-term research we present aims to face the problem of safety and security assurance of smart contracts at design time. We are investigating the usage of the Abstract State Machine (ASM) formal method for the specification, validation, and verification of Ethereum smart contracts. We provide (i) a set of ASM libraries that simplify smart contracts modeling, (ii) models of malicious contracts to be used to check the robustness of a contract against some given attacks, (iii) patterns of properties to be checked to guarantee the operational correctness of the contract and its adherence to certain predefined properties.Modeling/Verification
15:35 - 16:05
Coffee break
Session Chair: Angelo Gargantini
16:05 - 16:15
The Mechanical Lung Ventilator Case Study
This paper introduces the ABZ 2024 Case Study: Mechanical Lung Ventilator (MLV), inspired by the Mechanical Ventilator Milano developed during COVID-19. The case study reports the specification of the Mechanical Lung Ventilator used to ventilate patients who are not able to breathe on their own or need ventilation support. Expected contributions to the case study include, among others, modeling, validation and verification, management of temporal behavior, modeling of the graphical user interface or automatically generating executable source code.Case Study
16:15 - 16:45
Real-Time CCSL: Application to the Mechanical Lung Ventilator
This case-study paper reports on our experience in modelling the mechanical lung ventilator using the Clock Constraint Specification Language (CCSL). CCSL captures the causal and temporal behaviour of a system by specifying constraints on logical clocks. Logical clocks are integer counters where the occurrence of an event, a tick, advances the counter and marks the advance in time. In this framework, chronometric clocks become logical clocks just with a special external meaning. Encoding chronometric clocks as counters may result in verification inefficiency and hard-to-read specifications. The paper introduces in the language some real-time constructs to directly encode phenomena like clock drift, skew and jitter. This makes patterns explicit in turn enabling optimizations. To realize these optimizations, we alter the internal symbolic representation of clock constraints. We also introduce an explicit notion of parameters and intervals. While for some constraints it mainly consists of adding syntactic sugar and pre-processing facilities, we believe it improves the readability. We illustrate the new constructs on the mechanical lung ventilator system. We start with a purely logical specification, we point at the sources of inefficiencies and then we discuss the benefits of the extensions on specific parts.Case Study
16:45 - 17:15
An Event-B Model of a Mechanical Lung Ventilator
In this paper, we present a formal Event-B model of the Mechanical Lung Ventilator (MLV), the case study provided by the ABZ’24 conference. This system aims at helping patients maintain good breathing by providing mechanical ventilation. For this purpose, two modes are possible: Pressure Controlled Ventilation (PCV) and Pressure Support Ventilation (PSV). In the former mode, respiratory cycles are completely defined by the patient that is able to start breathing on its own. In the latter mode, the respiratory cycle is constant and controlled by the ventilator. Let us note that it is possible to move from a given mode to the other depending on the breathing capabilities of the patient under ventilation. In this paper, we illustrate the use of a correct-by-construction approach, the Event-B formal method and its refinement process, for the formal modeling and the verification of such a complex and critical system. The development of the formal models has been achieved under the Rodin platform that provides us with automatic and interactive provers used to verify the correctness of the models. We have also validated the built Event-B models using the ProB animator/model checker.Case Study
18:00 - 19:30
Tour Città Alta
19:30 - 24:00
Dinner in Città Alta - Restaurant "Da Franco"
June, 27th
Conference Room: Room 5
Time
Talk
Topic
Session Chair: Yamine Ait-Ameur
09:15 - 10:15
Getting Electronic Payments Right
EMV is the international protocol standard for smartcard payments and is used in billions of payment cards worldwide. Despite the standard’s advertised security, various issues have been previously uncovered, deriving from logical flaws that are hard to spot in EMV’s lengthy and complex specification, running over 2,000 pages. We have formalized various models of EMV in Tamarin, a symbolic model checker for cryptographic protocols. Tamarin was extremely effective in finding critical flaws, both known and new. For example, we discovered multiple ways that an attacker can use a victim's EMV card (e.g., Mastercard or Visa Card) for high-valued purchases without the victim's supposedly required PIN. Said more simply, the PIN on your EMV card is useless! We report on this, as well as follow-up work with an EMV consortium member on verifying the latest, improved version of the protocol, the EMV Kernel C-8. Overall our work provides evidence that security protocol model checkers like Tamarin have an essential role to play in developing real-world payment protocols and that they are up to this challenge.Keynote
10:15 - 10:45
Coffee break
Session Chair: Wolf Zimmermann
10:45 - 11:15
From Concept to Code: Unveiling a Tool for Translating Abstract State Machines into Java Code
Formal methods play a crucial role in modeling and quality assurance, but to be deployed on real systems, formal specifications need to be translated into implementation. Manually converting formal models into code poses challenges such as increased costs, limitations in specification reuse, and the potential for introducing errors. To overcome these limitations, Model-Driven Engineering (MDE) approaches enable developers to generate software code automatically. This paper proposes the Asmeta2Java tool for the automatic translation of formal Asmeta specifications into executable Java code. The designers start at an abstract level and perform refinement steps and verification activities. At the end, they automatically generate the code by applying the model-to-code transformation. Moreover, a process to validate and evaluate the transformation is presented.Tools
11:15 - 11:45
Loose Observation in Event-B
Refinement of Event-B machines is based on changing internal variables to obtain different data representations. One approach is expressed only in terms of internal variables. In the extreme case it permits refining a machine by any other by choosing the gluing invariant ``true''. The other one is based on relating external variables that can be refined functionally, so that properties expressed in terms of external variables are preserved. In practice, the first approach is used and gluing invariants are suitably chosen to achieve a meaningful relationship between refined machines. The second approach is based on the idea of observing a machine in terms of its external variables. It is more complicated, restrictive and not commonly used. In this paper we propose a different approach to observing Event-B machines that is more constraining than the first approach but less complicated and restrictive than the second approach. We extend Event-B refinement by permitting introducing new events and eliminating old events. The concept of observation is made more flexible by permitting non-observation of certain states as well as observing sets of values related to a states. Although this complicates relating observed fixed points and traces of machines, the proof obligations remain uncomplicated.Theory Extension
11:45 - 12:15
Modal Extensions of the Logic of Abstract State Machines
Based on the logic of non-deterministic Abstract State Machines (ASMs) we define a modal extension MLASM by first introducing multi-step predicates and then adding quantification over the number of steps. We show that liveness conditions such as invariance, conditional and unconditional progress, and persistence on all or some runs of an ASM can be expressed in this logic. While MLASM is too powerful to preserve the completeness of the logic of ASMs, we show the existence of a complete fragment, which still contains the interesting liveness conditions. We demonstrate the usefulness of this complete fragment by an example concerning mutual exclusion.Theory Extension
12:15 - 12:30
Semantics Formalisation -- From Event-B Contexts to Theories
The Event-B modelling language has been used to formalise the semantics of other modelling languages such as Time Mobility (TIMO) or State Chart XML (SCXML). Typically, the syntactical elements of the languages are captured as Event-B contexts while the semantical elements are formalised in Event-B machines. An alternative for capturing a modelling language's semantics is to use the Theory plug-in to build datatypes capturing the syntactical elements of the language and operators to represent the various semantical aspects of the language. This paper draws on our experience to compare the two approaches in both modelling and reasoning features.Theory Extension
12:30 - 14:00
Lunch break
Session Chair: Silvia Bonfanti
14:00 - 14:30
Modelling the mechanical lung ventilation system using TASTD
For the ABZ2024 conference, the proposed case study consists of modelling the adaptive outdoor mechanical lung ventilation system. The mechanical lung ventilator is intended to provide ventilation support for patients that are in intensive therapy and that require mechanical ventilation. The system under study is made up of two main software components: the graphical user interface (GUI) and the controller, this paper introduces a model for the controller part of the software system using Timed Algebraic State-Transition Diagrams (TASTD). TASTD is an extension of Algebraic State-Transition Diagrams (ASTD) providing timing operators to express timing constraints. The specification makes extensive use of the TASTD modularity capabilities, thanks to its algebraic approach, to model the behaviour of different sensors and actuators separately. We validate our specification using the cASTD compiler, which translates the TASTD specification into a C++ program. This generated program can be executed in simulation mode to manually update the system clock to check timing constraints. The model is executed on the test sequences provided with the case study. The advantages of having modularisation, orthogonality, abstraction, hierarchy, real-time, and graphical representation in one notation are highlighted with the proposed model.Case Study
14:30 - 15:00
Modelling and Analysing a Mechanical Lung Ventilator in mCRL2
We model the Mechanical Lung Ventilator (MLV) in the process algebra mCRL2. The functional requirements of the MLV are formalised in the modal mu-calculus, and we use model checking to analyse whether these requirements hold true of our model. Our formalisation of the MLV and its requirements reveal a few subtle imprecisions and unclarities in the informal document and we analyse their impact.Case Study
15:00 - 15:30
FRETting and Formal Modelling: A Mechanical Lung Ventilator
In this paper, we use NASA's Formal Requirements Elicitation Tool (FRET) and the Event-B formal method to model and verify the requirements for the ABZ 2024 case study which is a mechanical lung ventilator. We use the FRET requirements to guide the development of a formal design model in Event-B. We provide details about the artefacts produced and reflect on our experience of using these tools in this case study. We focus on the functional and controller requirements for this system, as given in the case study documentation. This paper provides a first step towards using Event-B as part of a FRET-guided verification workflow in a large case study.Case Study
15:30 - 16:00
Coffee break
Session Chair: Alexander Raschke
16:00 - 16:30
The Meaning of Self-Modifying Programs for Sequential Machines
We propose a definition of a class of reflective Abstract State Machines (ASMs) that extends the class of Parallel Guarded Assignments (PGAs), a subclass of single-agent sequential ASMs, and can serve as ground model for refinements of reflectivity in concrete programming languages.Theory Extension
16:30 - 16:45
Using Symbolic Execution to Transform Turbo Abstract State Machines into Basic Abstract State Machines
This paper introduces a transformation method that uses symbolic execution to eliminate sequential composition (''seq'') rules from turbo ASM rules by translating them into equivalent rules without ''seq''. Under some circumstances ''iterate'' rules can also be eliminated. The material presented here is work in progress. A prototype implementation of the transformation is publicly available.Tools
16:45 - 17:00
Multi-model animation with Jeb
A challenge posed by model-based formal methods such as Event-B is the validation of the models. This has been recognized and some tools have been created to provide modelers with means to animate models and to explore their behaviour through graphical display. These tools are quite effective on standalone models but lack the ability to connect to other external models. CPS systems fall under this category, as well as systems built of components interacting through a communication network. In the context of Jeb, an animation tool for Event-B models based on JavaScript, we explore the possibility of connecting models through Websockets. The paper presents a simple protocol to connect simulations. Using an example inspired by the Lung Ventilator case study, it shows how the implementation expands JeB functionality without modifying its core.Tools
17:00 - 17:15
Meta-Programming Event-B: Advancing Tool Support and Language Extensions
Transforming models based on their textual representation is a cumbersome task. This is particularly the case for Event-B, where the predominant representation is a set of XML files. As a consequence, tool support is lacking, even for minor refactoring operations. The contribution of this paper extends the lisb library with a front and backend based on Event-B. The aim is to bring benefits, that have been demonstrated for classical B, such as an easily transformable data representation of formal specifications as well as creation of custom DSLs and tooling, to Event-B. We see great benefits of such a meta-programming approach for formal specifications and advocate that similar mechanisms will be sensible extensions to the expressiveness of formal methods. Ultimately, our work facilitates language extensions (e.g., re-introducing if-then-else constructs to Event-B which generate multiple events or a proper macro system to avoid code duplication) and tool support (e.g., refactoring tools or automatic refinement).Tools
17:15 - 17:45
PC meeting
19:30 - 24:00
Social Dinner in Città Alta - Restaurant "Circolino"
June, 28th
Conference Room: Room 5
Time
Talk
Topic
Session Chair: Patrizia Scandurra
09:00 - 10:00
What happens when the Government starts encouraging the use of formal methods?
Over the past decade, US Government R&D RFPs have gone from never mentioning formal methods to frequently mandating formal methods. What's more, several recent White House reports have explicitly called out formal methods. For example, the 2016 NIST Interagency Report ''Dramatically Reducing Software Vulnerabilities: Report to the White House Office of Science and Technology Policy'' calls out formal methods as one of five key technical approaches critical to fulfilling the goals set forth in the US Government's 2016 Federal Cybersecurity R&D Strategic Plan. More recently, in February 2024 the Office of the National Cyber Director (ONCD) published the report ''Back to the Building Blocks: A Path Toward Secure and Measurable Software'' in response to President Biden's National Cybersecurity Strategy and in alignment with Executive Order 14028 on Improving the Nation's Cybersecurity, issued in 2021. Its abstract states: “In this report, the case is made that the technical community is well-positioned to drive progress on both strategic goals. First, in order to reduce memory safety vulnerabilities at scale, creators of software and hardware can better secure the building blocks of cyberspace. This report focuses on the programming language as a primary building block, and explores hardware architecture and formal methods as complementary approaches to achieve similar outcomes. Second, in order to establish accurate cybersecurity quality metrics, advances can be made to address the hard and complex research problem of software measurability. This report explores how such metrics can shift market forces to improve cybersecurity quality across the ecosystem. In essence, the US Government is now strongly recommending that nationally critical systems are written in safe programming languages, models and implementations of critical components must be formally assured, and that code should run on security-centric hardware architectures.'' This talk reflects upon this evolution over the past ten years from my point of view as a PI of dozens of major formal methods-centric R&D programs for the Government and industry. Why has there been such an uptick in interest? What are the R&D challenges that lie ahead? How might we, as a community, prioritize R&D activities for transition? What can the ABZ community learn from this arc? What's next?Keynote
10:00 - 10:30
An Analysis of the Impact of Field-Value Instance Navigation in Alloy’s Model Finding
The use of SAT-based model finding for specification analysis is a crucial characteristic of Alloy, and a main reason of its success as a language for software specification. When a property of a specification is analyzed and deemed satisfiable, the user usually explores instances of the corresponding satisfiability, in order to understand the analysis outcome. The order in which instances are obtained during exploration can impact the efficiency and effectiveness with which specification analysis is carried out. This has been observed by various researchers, and different instance exploration strategies have been proposed, besides the standard SAT-solver driven strategy implemented with the Alloy Analyzer. In this paper, we concentrate on a strategy recently proposed in the literature, that we refer to as ''field-value'' driven, and has been implemented in the tool HawkEye. The tool allows the user to interactively guide instance exploration, by enforcing constraints requiring fields to contain (resp., do not contain) specific values. We design an experiment involving faulty Alloy specifications featuring combinations of over constraints and under constraints, and perform a user study to analyze the impact of this instance exploration strategy, in comparison with the standard SAT-solver driven exploration. The study focuses on HawkEye’s facility of interactive instance querying and how it may favor users, in its current realization, during Alloy model analysis and debugging. We perform an assessment of the evaluation, and summarize some of the reasons that may diminish the impact of field-value exploration in model finding.Education
10:30 - 11:00
Coffee break
Session Chair: Regine Laleau
11:00 - 11:15
Event-B as DSL in Isabelle and HOL
The proof assistant Isabelle/HOL is made available inside a flexible system framework allowing for logically safe extensions, which comprise both theories as well as implementations for code-generation, documentation, and specific support for a variety of formal methods. Following the techniques in [23] and the theoretical groundwork in [5], we show the major milestones for the implementation of a B-Tool and the resulting refinement method inside the Isabelle/HOL platform. The pro- totype HOL-B provides IDE support, documentation support, a theory for the Z-Mathematical Toolkit underlying the B-Method, and a gener- ated denotational semantics for the B-Machine concept implemented as specification construct in Isabelle/HOL. Extended by more automated proof machinery geared to refinements, HOL-B can serve as a more portable, flexible and extensible tool for Event-B that may profit from the large Isabelle/HOL libraries providing Algebra and Analysis theories.Verification
11:15 - 11:30
ThoR: An Alloy5-based DSL for Interactive Theorem Proving in Coq
The steep learning curve associated with interactive theorem proving poses a significant entry barrier for the learner. While the Alloy specification language has simplified the introduction to and application of formal methods, transitioning to interactive theorem proving, such as with Coq, remains daunting due to the inherent complexity of formal reasoning and the sophisticated tooling required. We introduce ThoR, an extension for the Coq proof assistant that incorporates an Alloy-based domain-specific language: Specifications, propositions and proofs are formulated in an Alloy-like syntax. This reduces tool and language complexity, and makes interactive theorem proving more accessible. The implementation is based on Coq’s syntax extension capabilities and the mathematical components library (mathcomp). This paper reports on work in progress. It contributes an approach for the embedding of Alloy into Coq based on a set-theoretic interpretation, a proof calculus for Alloy with soundness by construction, a prototypical implementation and its validation via a simple token ring example.Verification
11:30 - 11:45
Verifying HyperLTL properties in Event-B
The study presented in this paper is motivated by the verification of properties related to hardware architectures, namely timing anomalies that qualify a counter-intuitive timing behaviour. They are avoided by a monotonicity property which is an Hyper-LTL property. We present how to prove some classes of Hyper-LTL properties with Event-B.Verification
11:45 - 12:00
Small Step Incremental Verification of Compilers
Previously, we introduced the idea of agile compiler development, i.e., starting from an initial compiler for the most simple program of a language and extending it in small versions, each introducing a new language concept. Following this idea, in this paper, we propose an approach for incrementally verifying the dynamic semantics specified with abstract state machines~(ASMs), such that definitions of previous versions must not be altered in subsequent versions. As a result, the compiler can be verified incrementally without revising the proofs of previous versions. As our first step, in this paper, we formalize and verify the memory mapping of the initial versions with ASMs and discuss their extensibility for the next increments. We plan to demonstrate this approach through the agile implementation and verification of a Sather-K compiler generating MIPS assembly language.Verification
Session Chair: Philipp Körner
12:15 - 12:30
From Event-B to Lambdapi
B, Event-B and TLA+ are development languages based on set theory. Dedukti/Lambdapi is a logical framework based on the λΠ- calculus modulo in which many theories and logics can be expressed. In the context of ICSPA (ANR project), Lambdapi will be used to ex- change models and proofs between the set theory-based formal methods B, Event-B and TLA+. They will rely on the encoding of the respective set theories in Lambdapi. Our current work focuses on translating the mathematical language of Event-B and proof trees obtained with the Rodin platform for Event-B.Doctoral Symposium
12:30 - 12:45
Proof Construction and Checking on Evolving Abstract State Machines
Abstract State Machines (ASMs) are widely used in the formalization and verification of the semantics of software or hardware. However, tools for assisting this process for evolving specifications are still lacking. With evolving we denote adding extensions without refactoring. We want to create a tool assisting in the verification of evolving specifications. Our approach is to translate ASM specifications into the language of an existing proof checker, construct the proofs as far as possible automatically, and check the proofs with the proof checker. Further, we want proofs of evolvable specifications also to be evolvable. This paper gives a brief overview of the approach and discusses the first step of this work, namely the translation of ASM specifications into the language of an existing proof checker, with consideration of automation possibilities.Doctoral Symposium
12:45 - 13:00
Closing session
13:00 - 14:00
Lunch break and greetings