A Verification Environment for I/O Automata Based on Formalized Meta-Theory

This thesis deals with the computer-assisted verification of embedded systems described as Input/Output automata. We achieve contributions in two fields: the theory of untimed I/O automata and its tool support. For the latter a combination of the theorem prover Isabelle with model checking is used. Concerning the theory of I/O automata, we present a new temporal logic which considerably facilitates the usual implementation proofs between live I/O automata and serves as a property specification language. Furthermore, a new theory of abstraction is developed which allows us to combine theorem proving and model checking. Theorem proving is used to justify the reduction of the original system to a smaller model which is then analyzed automatically by model checking. The theorem prover reasons about first-order proof obligations only. For the remaining obligations translations to the model checkers $\mu$cke and STeP are given. In contrast to existing abstraction theories, the proof of both temporal properties and implementation relations can be abstracted, a methodology for treating liveness abstractions is proposed, and a formal relation to the dual concept of refinement is established. Concerning tool support, we provide a verification environment that covers both standard I/O automata theory and the aforementioned extensions. The overall guideline for its construction is reliability. Therefore, meta-theoretic notions of I/O automata such as compositionality and refinement are mechanically 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. Possibly infinite communication histories of I/O automata are formalized as lazy lists based on Scott's domain theory. This results in a generally applicable sequence model which turns out to be favorable in an elaborate comparison with alternative formalizations. In addition to the usual inductive proof principles for lazy lists we provide an infrastructure for coinduction. The practical relevance of the resulting verification environment is proven by several case studies, in particular by an industrial helicopter alarm system.     «

This thesis deals with the computer-assisted verification of embedded systems described as Input/Output automata. We achieve contributions in two fields: the theory of untimed I/O automata and its tool support. For the latter a combination of the theorem prover Isabelle with model checking is used. Concerning the theory of I/O automata, we present a new temporal logic which considerably facilitates the usual implementation proofs between live I/O automata and serves as a property specification l...     »