Verification of Distributed Systems using I/O Automata

[Isabelle logo]

The aim of this project is to build a verification environment for distributed, reactive systems. Systems are specified as I/O automata and verified by a combination of the theorem prover Isabelle with the model checkers STeP or µcke [7]. For a detailed description of the entire framework see Müller's Phd thesis [6]. The proof scripts are part of the Isabelle online theory library and are distributed with Isabelle. Go to subdirectory HOLCF/IOA.

The environment allows to verify both temporal properties and implementation relations between I/O automata. A new temporal logic is introduced (TLS) - similar to TLA - which is implemented via a generic temporal logic [5]. As a result, general liveness can be handled.

In order to combine theorem proving with model checking a new abstraction theory is developed and embedded in Isabelle which allows to abstract both implementation relations and temporal properties [5]. Via an oracle, abstract temporal properties are delegated to STeP, abstract implementation relations to µcke. There are additional rules which facilitate the abstraction of liveness properties.

The overall guideline for the environment is its reliability. Therefore, a definitional embedding is chosen. As a consequence, meta-theoretic notions of I/O automata such as compositionality and refinement are also verified in Isabelle. Nevertheless, a practicable environment for system verification is obtained. This is due to a new methodology for Isabelle's logics HOL and HOLCF, which allows the user of the framework to employ the simpler logic HOL, whereas meta-theoretic investigations gain from the more expressive HOLCF [4].

Possibly infinite communication histories of I/O automata are formalized in HOLCF as lazy lists based on Scott's domain theory [4]. This results in a generally applicable sequence model which turns out to be favorable in an elaborate comparison with alternative formalizations [3]. In addition to the usual inductive proof principles for lazy lists an infrastructure for coinduction is provided. The practical relevance of the resulting verification environment has been proven by several case studies already.

Papers

  1. Tobias Nipkow, Konrad Slind. I/O Automata in Isabelle/HOL. In Types for Proofs and Programs, LNCS 996, 1995, 101-119.
  2. Olaf Müller and Tobias Nipkow, Combining Model Checking and Deduction for I/O Automata. In TACAS'95, Proc. of the 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1019, 1995, 1-16.
  3. Marco Devillers, David Griffioen, and Olaf Müller, Possibly Infinite Sequences in Theorem Provers: A Comparative Study. In TPHOL'97, Proc. of the 10th International Workshop on Theorem Proving in Higher Order Logics,LNCS 1275, 1997, 89-104.
  4. Olaf Müller and Tobias Nipkow, Traces of I/O Automata in Isabelle/HOLCF. In TAPSOFT'97, Proc. of the 7th International Joint Conference on Theory and Practice of Software Development, LNCS 1214, 1997, 580-595.
  5. Olaf Müller, I/O Automata and Beyond - Temporal Logic and Abstraction in Isabelle. In TPHOL'98. Proc. of the 11th International Workshop on Theorem Proving in Higher Order Logics,LNCS 1479, 1998, 331-348.
  6. Olaf Müller, A Verification Environment for I/O Automata Based on Formalized Meta-Theory, PhD thesis, Technische Universität München, 1998.
  7. Tobias Hamberger, Integrating Theorem Proving and Model Checking in Isabelle/IOA, Technical Report, Technische Universität München, 1999. Also as PDF file.

    Related Work

    Funding

    IOA was part of the KorSys project funded by the BMBF.