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 IMP_concur with Isabelle/HOL-CSP
Level: L3 / M1
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.
In this internship, overall aim is to provide a simple programming-language like Front-End to this process-algebra, thus giving it a semantics in terms HOL-CSP. The simple programming language is called IMP_concur (so a concurrent variant of the well-known IMP-language); its abstract and concrete syntax is defined as follows:
datatype com = SKIP
| assign V E⇩a⇩r⇩i⇩t⇩h ("LOCAL _ := _" [90,90]80)
| seq com com (infixl ";" 78)
| cond E⇩b⇩o⇩o⇩l com com ("IF (_)/ THEN (_)/ ELSE (_)/" [0,0,79]79)
| while E⇩b⇩o⇩o⇩l com com ("WHILE (_)/ DO (_)" [0,80]80)
| lock MV
| unlock MV
| send SV E⇩a⇩r⇩i⇩t⇩h ("_ ↪ _" [90,90]80)
| rec V SV ("_ ↩_" [90,90]80)
This Isabelle/HOL definition also generates a concrete syntax in which we can write IMP_concur programs like:
LOCAL ''a'' := E ;
IF A THEN SKIP ELSE lock 3;
4 ↪ (λσ. σ ''a'' + 1);
''a''↩ 4;
WHILE (λσ. True) DO unlock 3
There are actually two ways give semantics to IMP_concur. First, a direct implementation into HOL-CSPm should be attempted [3,4,5]. Second, a translation to a more automata-oriented format called ProcOmata [6] should be attempted - the latter has advantages wrt. to automated proof-methods over CSP-like languages.
This results in the following
Workplan
- Learning via examples CSP and CSP Refinement.
- Learning to use the functional API of the Isabelle system.
- Designing and implementing a translation scheme to HOL-CSPm.
- Designing and implementing a translation scheme to ProcOmata.
Required Skills
- Good functional programming skills
- Basic Knowledge about typed lambda-calculus
- Basic Knowledge in Logics and Formal Semantics
Achieved Skills
- Knowledge in compiler construction, typed lambda-calculus, ...
- Some knowledge over process algebras and the theory of concurrency.
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. [3] B. Ballenghien, S. Taha, B. Wolff : HOL-CSP Version 2.0 [4] B. Ballenghien, S. Taha, B. Wolff : HOL-CSPM - Architectural operators for HOL-CSP [5] B. Ballenghien and B. Wolff. An Operational Semantics in Isabelle/HOL-CSP. ITP 2024.
LNCS 15373
[6] B. Ballenghien, B. Wolff. A Theory of Proc-Omata - and Proof Methods for Process Architectures. ICTAC 2024,
LIPIcs 309.
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.