An LTS Library with Functions for Test-Generation
Level: L3
Contact: B. Wolff (wolff@lmf.cnrs.fr)
Description
Labelled Transition Systems (LTS) [4,5] are a Graph-like data-structure consisting of Nodes and Transitions that may be labelled with additional information. They were used to denote, for example, control-flow-graphs (CFG’s), data-flow-graphs (DFGs), game theory, abstractions of operational executions, and in particular concurrent executions.
The aim for this stage is to enlarge an existing library of LTS’s in SML running inside the Isabelle system. Particular emphasis is put on bisimulation algorithms, i.e. concrete procedures establishing trace-inclusions on automata, and algorithms implementing coverage criteria known from testing such as “allStates”, “allTransitions” and “allPath(k)”. Developing first proof support for this kind of generated formulas can be addressed in a later stage of this internship.
This project stands in the context of the Isabelle/HOL-CSP/FDR project [3,5,6], implemented in Isabelle/HOL[1,2], which links a theory on concurrency with the FDR4 model-checker. By this tool-chain, it is possible to generate for a model of a concurrent system in CSP and the conceptual Programming language IMP_CSP the corresponding LTS’s in the above-mentioned library and to produce Test-traces from these models.
Workplan
- Understanding the existing library and constructing a work-setup inside Isabelle
- Implementing the new core functionality
- Developing a Suite of smaller examples for testing
Required Skills
- functional programming skills
- interest in compiler construction
- knowledge in concurrency and programming semantics desirable, but not necessary
Bibliography
[1] Thomas Genet, Joergen Villadsen : Isabelle: An introduction.
[2] Isabelle/HOL and the Isabelle Archive of Formal Methods: Overview and General AFP Entry and Isabelle on Wikipedia.
[3] Makarius Wenzel, Burkhart Wolff: Building Formal Method Tools in the Isabelle/Isar Framework. TPHOLs 2007: 352-367
[4] Labelled Transition System. Labelled Transition Systems. And: slides.
[5] Benoit Ballenghien, Tianwen Gu et Burkhart Wolff: Certifying FDR4 Checks by HOL-CSP Proofs. Submitted.
[6] HOL-CSP 2.0: The GIT for the Isabelle/HOL-CSP project. Git - Link.
[7] A.W. Roscoe. Theory and Practice of Concurrency. Prentice Hall, 1997.
[8] A.W. Roscoe. Understanding Concurrent Systems. Springer-Verlag, Berlin, Heidelberg, 1st edition, 2010.
Generation of Simulations of Autonomes Car Scenarios in HOL-CSP
Level: M1/M2
Contact: B. Wolff, A. Durier
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.
A HOL-CSP Case-Study : Analysing the Plain-Old-Telephone Protocol
Contact: B. Wolff, A. Durier, Benoit Ballenghien
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. This theory has been presented in Isabelle/HOL based on the denotational semantics of the Failure/Divergence Model of CSP ... The "Plain Old Telephone Service" is a standard medium-size example for architectural modeling of a concurrent system ...
The goal of this stage is a formal analysis of deadlock- and life lock properties of this protocol via interactive proof in Isabelle/HOL.
Connecting Isabelle/C with Isabelle/AutoCorres
Level: M1 / M2
Contact: B. Wolff
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. The purpose of this stage is to develop a translation from C11-AST's generated in Isabelle/C to a semantic backend called AutoCorres, a complex execution model of the C ;language executed on ARM processors.
This ambitious project is actually a re-implementation and integration of existing prototypes: there is actually a Isabelle/C/AutoCorres version based on Isabelle2021 which is functional enough to serve as reference. However, AutoCorres exists meanwhile as a much more recent and self-contained AFP submission (see here), and the technologies inside Isabelle/C to compile the C11-AST's to a semantic backend have also dramatically improved. Since the long-term goal is a submission of Isabelle/C together with the AutoCorres backend, a re-implementation is necessary.