HOL-Bee: Implementing B-Method Support in Isabelle/HOL
Description
The B-Method has been proposed by Jean-Raymond Abrial as a formal program development method based on refinement[1]. More recent implementations like Rhodin from an open-source project suffer from numerous limitations and ad-hoc implementations of the prover components. Commercial implementations, in contrast, albeit intensively used in the European railways industry, are out of reach for common users and researchers.
Based on an implementation of the Z-Mathematical Toolkit underlying [2,3] it is possible to work out refinement support for the B-Method inside the Isabelle/HOL Eco-System, i.e. provers and IDE included. A first prototype is available.
The aim for this stage is to enlarge the prototype and to generate more aspects of the refinement, i.e. concrete proof-obligations from the B-Machine models (which are basically Labelled Transition Systems.) This task boils essentially down to implement a generator to certain formulas in the typed lambda-calculus underlying Isabelle/HOL. Developing first proof support for this kind of generated formulas can be addressed in a later stage of this internship.
Work Plan
- Understanding the B-Method library and completing an existing port from Isabelle2007
- completing the front-end with the features that generate abstraction predicates
- Developing a Suite of smaller examples for testing
Required Skills
- good functional programming skills
- interest in compiler construction
- knowledge in theorem proving desirable, but not necessary
Bibliography
[1] Abrial JR. The B-Book: Assigning Programs to Meanings. Cambridge: Cambridge University Press; 1996. doi:10.1017/CBO9780511624162
[2] David Basin, Hironobu Kuruma, Kunihiko Miyazaki, Kazuo Takaragi and Burkhart Wolff: Verifying a Signature Architecture - A Comparative Case Study. In: Formal Aspects of Computing (FAC), 19 (1), pages 63-91, Springer. DOI 10.1007/s00165-006-0012-5, 2007.
[3] Makarius Wenzel, Burkhart Wolff: Building Formal Method Tools in the Isabelle/Isar Framework. TPHOLs 2007: 352-367
Generation of Executable Code from HOL-CSP Processes
Description
The theory of Communicating Sequential Processes going back to Hoare and Roscoe is still today one of the reference theories for concurrent specification and computing. in Isabelle/HOL of the denotational semantics of the Failure/Divergence Model of CSP was undertaken; in particular, this model can cope with infinite alphabets, in contrast to model-checking approaches limited to finite ones. In this paper, we extend this theory to a significant degree by taking advantage of more powerful automation of modern Isabelle version, which came even closer to recent developments in the semantic foundation of CSP.
In prior work, CSP has been presented as conservative embedding in Isabelle/HOL; a theory that provides the definitions of the denotational semantics of the CSP operators and derives algebraic rules from these. It ia a characteristic feature of resulting theory Isabelle/HOL-CSP [1] that one can model and reason over processes with an infinite type that can be arbitrarily defined in HOL. A framework for semi-automated refinement proofs has also been provided [2].
For example, process specifications can be written in:
datatype 'a channel = left 'a | right 'a | mid 'a | ack
definition SYN :: "('a channel) set"
where "SYN ≡ (range mid) ∪ {ack}"
definition COPY :: "('a channel) process"
where "COPY ≡ (μ COPY. left`?`x → right`!`x → COPY)"
definition SEND :: "('a channel) process"
where "SEND ≡ (μ SEND. left`?`x → mid`!`x → ack → SEND)"
definition REC :: "('a channel) process"
where "REC ≡ (μ REC. mid`?`x → right`!`x → ack → REC)"
definition SYSTEM :: "('a channel) process"
where "SYSTEM ≡ ((SEND ⟦ SYN ⟧ REC) \\ SYN)"
and refinement relations be proven via a conventional fix point induction:
lemma "COPY ⊑ SYSTEM" proof ... qed
The purpose of this work is to use code-generation techniques of the Isabelle system in order to generate efficient procedures that generate concrete random traces for a large set HOL-CSP processes.
How to proceed:
The proposed approach consists in adapting the techniques described in [4] to Isabelle/HOL-CSP. There, a theory Interaction Trees is developed in Isabelle/HOL that is used to produce a verification and simulation framework for state-rich process languages. A core theory and verification techniques for Interaction Trees, use them to give a semantics to the CSP and Circus languages, and formally link our new semantics with the failures-divergences semantic model.
Workplan:
- Study of [4]
- Integrate this in HOL-CSP either by a translation on the SML level or by establishing a link between them and Isabelle/HOL-CSP (which is the preferred route)
- Developing an example suite for testing.
Bibliography
[1] Safouan Taha, Burkhart Wolff and Lina Ye:
Isabelle/HOL-CSP, 2019.
[2] Safouan Taha, Burkhart Wolff and Lina Ye:
The Isabelle/HOL-CSP Refinement Toolkit, 2020.
[3] Safouan Taha, Burkhart Wolff and Lina Ye:
Philosophers may dine - definitively !, PDF, iFM, Oct 2019.
[4] Simon Foster, Chung-Kil Hur, Jim Woodock:
Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL. CONCUR 2021: 20:1-20:18
[5] A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 2005.
Connecting Isabelle/C with Isabelle/Clean
Description
Isabelle/C is a framework for C code in C11 syntax deeply integrated into the Isabelle/PIDE development environment. Our framework provides an abstract interface for verification back-ends to be plugged-in independently. Thus, various techniques such as deductive program verification or whitebox testing can be applied to the same source, which is part of an integrated Isabelle/PIDE document model. Semantic back-ends are free to choose the supported C fragment and its semantics. In particular, they can differ on the chosen memory model or the specification mechanism for framing conditions. Isabelle/C supports semantic annotations of C sources in the form of comments. Annotations serve to locally controlled back-end settings, and can express the term focus to which an annotation refers. Both the logical and the syntactic context are available when semantic annotations are evaluated. As a consequence, a formula in an annotation can refer both to HOL or C variables. (See also the Isabelle Club Meeting for more details).
Clean is based on a simple execution model for an imperative target language. It strives for a type-safe notion of program-variables, an incremental construction of the typed state-space, support of incremental verification, and open-world extensibility of new type definitions being intertwined with the program definitions. Clean offers conditionals and loops supporting C-like control-flow operators such as break and return. Direct recursion of procedures is also supported. Clean’s design strives for extreme simplicity. It is geared towards symbolic execution and proven correct verification tools. Isabelle/Clean [2] provides the underlying libraries of this package.
Isabelle/Clean is intended to serve as demonstrator semantic backend for Isabelle/C, or for the test-generation techniques. The purpose of this stage is to write a translation --- based on existing infrastructure --- from the C11-AST's generated inside Isabelle/C to the lambda-terms underlying the Isabelle/Clean representation, thus using Isabelle/Clean as a semantic backend of Isabelle/C.
Proceeding
Implementing for each syntactic category in the C11 AST's via C11 library-routines a translation to the individual programming constructs supported by Clean. The implementation language is SML directly supported in the Isabelle programming environment. SML pattern-matching and various SML libraries will help at the task.
Bibliography
[1] Frédéric Tuong and Burkhart Wolff:
Deeply Integrating C11 Code Support into Isabelle/PIDE, FiDE, 2019.
[2] Frédéric Tuong and Burkhart Wolff:
The Isabelle/Clean Theory, 2019-21.
[3] Frederic Tuong and Burkhart Wolff:
Isabelle/C
Required Skills
- good functional programming skills
- interest in compiler construction
- no knowledge in theorem proving necessary
Generation of Simulations of Autonomes Car Scenarios in HOL-CSP
Description
In prior work, it has been shown that autonomous car scenarios can be modelled in Isabelle/HOL-CSP [1] for proving safety properties of these systems [2].
The purpose of this work is to use code-generation techniques of the Isabelle system in order to generate efficient procedures that generate concrete random runs out of HOL-CSP Car scenarios.
Bibliography
[1] Safouan Taha, Burkhart Wolff and Lina Ye:
Isabelle/HOL-CSP, 2019, The Isabelle/HOL-CSP Refinement Toolkit, 2020.
[2] Safouan Taha, Burkhart Wolff:
Modelling and Proving Safety in Autonomous Cars Scenarios in HOL-CSP.
SystemX Technical Report, Oct 2021.