A Machine-checked User-Manual for Isabelle/DOF
Contact: B. Wolff, Idir Ait-Sadoune
Description
Isabelle/DOF is a framework inside the Isabelle/HOL allowing to write technical reports, scientific papers, deliverables for certification processes, etc, so generally speaking: for documents that contain both formal and informal content. The linking between both is notoriously difficult, especially if both the formal and informal content is evolving during development. Roughly similar to Javadoc, Doxygen or ocamldoc, Isabelle/DOF allows for the integration of a kind of semantic macros (called antiquotations) into texts, λ-terms or code:
Text-Element with Antiquotations
Corresponding pdf-Fragment
Isabelle/DOF extends the set of these antiquotations by a more general mechanism to *define* them via an ontology. For example, it is possible to define a domain ontologie from a software-engineering standard providing concepts like "definitions of a term", "requirements", "model-elements" and "test-results", etc. In a document conform to this ontology, a text element can be "tagged" as "safety_requirement" via:
text*[a::safety_requirement]<The doors may only be opened when the train completely stopped.>
Later on, we can refer to this requirement via
text <As required by @{requirement a}, the safety function
@{thm OpenDoor_def} can rely on the fact that the speed @{term "v"} is
@{term "0::real[m/s]}.>
The latter term is actually typechecked with respect of an algebra representing SI-measurements inside the Isabelle type-system.
Many features in Isabelle/DOF allow for writing even scientific papers and generating the LaTeX in a quality sufficient for conference [1,2,3]and journal publications [4,5]. While a Reference Manual describing the features on a technical level exists Isabelle/DOF User Manual vs. 1.1 (see the git for more recent versions), but this document is feature-oriented and not solution oriented as writers of documents need to find fast. Many LaTeX-snippets in the internet show how problem-oriented examples can substantially increase the usability of an advanced typesetting system.
The purpose of this stage is to develop another Isabelle/DOF document which is a true "User Manual" in this sense. The result should be a generated .pdf and html - document organized in a "HowTo" - style for users, albeit still mechanically checked and tested against the (continuously evolving since under development) Isabelle/DOF system.
This results in the following
Workplan
- Identify a number of common Howto-scenarios (a catalogue of LaTeX snippets might be a starting point)
- Produce a number of equivalent snippets in Isabelle/DOF
- Development of a unit-test-infrastucture
- Test of the generation against different LaTeX - styles (LLNCS, LIPICS, ...)
Required Skills
- Good functional programming skills
- Skills in using LaTeX
- An Interest in advanced document modelling and processing
- Good and critic sense for communication to end-users
Bibliography
[1] Achim D. Brucker, Burkhart Wolff: Using Ontologies in Formal Developments Targeting Certification. IFM 2019: 65-82
[2] Achim D. Brucker, Idir Aït-Sadoune, Nicolas Méric, Burkhart Wolff: Using Deep Ontologies in Formal Software Engineering. ABZ 2023: 15-32
[3] Safouan Taha, Burkhart Wolff and Lina Ye:
Philosophers may dine - definitively !, PDF, iFM, Oct 2019.
[4] Achim D. Brucker, Idir Aït-Sadoune, Nicolas Méric, Burkhart Wolff: Modeling and analysing Cyber-Physical Systems in HOL-CSP. Robotics Auton. Syst. 170: 104549 (2023)
[5] Achim D. Brucker, Idir Aït-Sadoune, Nicolas Méric, Burkhart Wolff: Order-Sorted Polymorphisc Ontologies with an Application to Formal Software Engineering. submitted to SCP 2024.
[6] Achim D. Brucker, Idir Aït-Sadoune, Nicolas Méric, Burkhart Wolff:
The Isabelle/DOF development git. 2024
Connecting Isabelle/HOL-CSP with FDR4
Level: L3
Contact: Burkhart Wolff, Benoit Ballenghien
Description:
HOL-CSP and its extension CSPm is a powerful proof-environment based on Isabelle/HOL and the process algebra 'Communicating Sequential Processes' developed by Tony Hoare and Bill Roscoe in the 90ies[1,2]. In particular, HOL-CSP can model and reason over processes with infinite event structures, so dense time, physical states, algebraic structures, etc. Isabelle/HOL-CSP is therefore strong in in general proofs over process-architecture and general properties of process patterns.
FDR4 is a model-checker that provides automated proofs for process-refinements for finite event structures. it excels with highly automated proofs over processes in a fairly expressive process description language called CSPM. Ho=wever, it is a research question if and to what extent HOL-CSP can be combined with FDR4, and to what extent finite proofs can be generalized to infinite event structures.
In this internship, the technical question is addressed how to make collaborate the Isabelle system with FDR. As a prerequisite, the internal presentation of FDR4, a so-called "Labelled Transition System" (LTS) representing CSP processes must be converted into a JSON format that can be read by Isabelle. For this purpose, an internal FDR4 API must be extended by functions that convert the internal LTS data-structure into a JSON output file.
This results in the following
Workplan
- Studying the FDR4 API's
- Learning via examples CSP and CSP Refinement
- Identifying concepts of LTS's used in FDR and finding ways of their representation
- Implementing a bridge between Isabelle and FDR
Required Skills
- Good programming skills (functional and C++)
- Basic Knowledge in Logics and Formal Semantics
Achieved Skills
- Knowledge in compiler construction, lambda-calculus, ...
- Some knowledge over process algebras
Bibliography
[1] A.W. Roscoe. Theory and Practice of Concurrency. Prentice Hall, 1997. [2] A.W. Roscoe. Understanding Concurrent Systems. Springer-Verlag, Berlin, Heidelberg, 1st edition, 2010.
Generation of Simulations of Autonomes Car Scenarios in HOL-CSP
Contact: B. Wolff, S. Taha
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, S. Taha
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/Clean
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 Clean, a simple execution model for an imperative target language.