Verisoft Repository

In the Verisoft project, the formal pervasive verification of four exemplary computer systems, three of which come from the industrial sector, is attempted. The layers, which are considered, range from the gate-level hardware over system software to communicating and distributed applications.

The Verisoft Repository allows to concurrently develop the many individual results that contribute to the overall verification results and to manage them in a tractable manner.

In the repository, the artefacts developed by the project partners are being collected as modules and related to each other via dependencies. Modules include documentations, specifications, implementations, proofs, and tools for development and verification.

In the end, the repository must be self-contained: the set of modules for a given computer system under verification must allow

  • to build an executable implementation of that system and
  • to prove its top-level correctness.

Currently, substantial parts of the Verisoft theories and systems have been imported into the Verisoft repository and the repository is being used for further development.

At this location, portions of the internal Verisoft repository that appear sufficiently stable and do not contain confidential data of industry partners, will be published.

Publications

Note: most of the theories included in the publications below are based on version 2005 of the interactive theorem prover Isabelle. The page Isabelle 2005 Installation gives some helpful advice on how to install this version of Isabelle with current versions of Poly/ML and ProofGeneral.

  • vlibolos-trunk-r31831.tar.gz (4.0M) — Towards Pervasive Verification of a Small Automotive Computer System (23 December 2010)

    This release focuses on proofs about the real-time operating system OLOS that has been developed within Subproject 6: Automotive. OLOS features time-triggered scheduling, process separation, buffered communication, and drivers for the automotive bus controller that allows several OLOS systems to communicate with each other. Applications running under OLOS can communicate via system calls that update or read a message buffer, i.e., an application visible data structure of the operating system. In particular, the release comprises two results: First, it contains the refinement proof of the OLOS implementation showing that the implementation meets the formal OLOS specification. Second, it contains the pervasive verification of a system-call library, which allows user processes implemented in a C variant to access OLOS functionality. When both results are combined, it is possible to justify that properties about user processes proven at an abstract C programming model indeed hold at the implementation level of the operating system and the compiled processes.

  • vlibvamos-trunk-r31570.tar.gz (5.2M) — Verification Results about the Correctness of a Microkernel and its User Processes (1 September 2010)

    This release contains proofs about the general-purpose microkernel VAMOS and the user processes running on top of it. The VAMOS microkernel has been developed within Subproject 2: Academic System. In essence, the release presents two refinement proofs: In a first step, the implementation of the VAMOS microkernel is linked with an abstract specification model. In a second step, this kernel specification with its explicit, deterministic scheduling is further abstracted to a concurrent process system with non-deterministic but temporally fair scheduling. In combination, both results form the formal foundation of a verification approach for system-level concurrent C programs.

  • volos-trunk-r29950.tar.gz (3.5M) — Implementation Correctness of the Real-Time Operating System OLOS (3 December 2009)

    This release focuses on the code level verification of real-time operating system OLOS, used within Subproject 6: Automotive. OLOS features time-triggered scheduling, process separation, buffered communication, and drivers for the automotive bus controller that allows several OLOS systems to communicate with each other. Applications running under OLOS can communicate via system calls that update or read a message buffer, i.e., an application visible data structure of the operating system.

    Note: this release is also contained in the newer release vlibolos-trunk-r31831.tar.gz above.

  • vvamos-trunk-r28405.tar.gz (3.8M) — Fairness and Implementation Correctness of a Microkernel Scheduler (16 June 2009)

    This release contains two verification results for the microkernel VAMOS, which have been developed within Subproject 2: Academic System. In particular, the release presents a refinement proof for the VAMOS scheduler, which links the implementation with an abstract specification model, as well as a fairness proof, which is based on this abstract specification.

    Note: this release is also contained in the newer release vlibvamos-trunk-r31570.tar.gz above.

  • C0compilerCombined-trunk-r22114.tar.gz (5.7M) — Verification of a C0 Compiler (21 February 2008)

    This release extends the compiler verification from the previous release by a proof that the generated assembly code simulates the original C0 program, i.e. that both have the same behavior.
    Additionally contained in this release are an assembler and a simulator for the VAMP architecture.

  • vc0compiler-trunk-r19956.tar.gz (4.0M) — Code-Level Verification of a C0 Compiler (19 October 2007)

    This release contains the code-level verification of a compiler for the programming language C0. C0 is a subset of C and the main implementation language for software in Verisoft. The compiler itself is implemented in C0. The verification of this compiler implementation is done in a Hoare-logic-based interactive software verification environment for the theorem proving environment Isabelle. The correctness theorem theorem shows that the compiler implementation generates code as specified by the code generation function in Isabelle/HOL. In a later publication we will additionally publish a proof that the code generation function in Isabelle/HOL is correct.
    Additionally contained in this release are a formal small-steps semantics of C0 and a formal semantics of VAMP assembler, the source and target languages of the C0 compiler.

    Note: this release is also contained in the newer release C0compilerCombined-trunk-r22114.tar.gz (5.7M) above.

  • vemail-trunk-r15868.tar.gz (3.6M) — Code-Level Verification of an Email Client (18 May 2007)

    This release contains the code-level verification of the email client of Subproject 2: Academic System relative to the services provided by the simple operating system (SOS) and applications for signing and email transfer. The implementation language is the C-like programming language C0. The verification is done in a Hoare-logic-based interactive software verification environment for the theorem proving environment Isabelle.

  • vString-4-r11594.tar.gz (1.8M) — Code-Level Verification of a String Library (14 Dec 2006)

    This release contains the code-level verification of a doubly-linked list library and a string library; the implementation language is the C-like programming language C0. The verification is done in a Hoare-logic-based interactive software verification environment for the theorem proving environment Isabelle, which is also included.

    Note: this release is also contained in the newer release C0compilerCombined-trunk-r22114.tar.gz (5.7M) above.

 
Revision 23 Dec 2010