Towards an Isabelle Theory for distributed, interactive systems : the untimed case

RWTH Publications (RWTH Aachen)

Abstract

This report describes a specification and verification framework for distributed interactive systems.The framework encodes the untimed part of the formal methodology FOCUS [BS01] in the proof assistant Isabelle [Pau90] using domain-theoretical concepts.The key concept of FOCUS, the stream data type, together with the corresponding prefix-order, is formalized as a pointed complete partial order.Furthermore, a high-level API is provided to hide the explicit usage of domain theoretical concepts by the user in typical proofs.Realizability constraints for modeling component networks with potential feedback loops are implemented.Moreover, a set of commonly used functions on streams are defined as least fixed points of the corresponding functionals and are proven to be prefix-continuous.

Authors 7

1. Jens Christoph Bürger Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen

2. Hendrik Kausch Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen

3. Deni Raco Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen

4. Jan Oliver Ringert Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen

5. Bernhard Rumpe⋆ Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen

6. Sebastian Stüber Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen

7. Marc Wiartalla Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen