A Verification Environment for I/O Automata -- Part I: Temporal Logic and Abstraction --

I/O automata are used to specify and reason about distributed, reactive systems. In this paper we extend standard I/O automata by a theory of abstraction. The intention is to combine theorem proving and model checking. Verifying both temporal properties and implementation relations is reduced to finite-state model checking. Even for livenness proofs merely simple first-order proof obligations remain for theorem proving. Furthermore, a methodology is developed which allows an incremental improvement of abstractions, thus increasing the potential for automation. The results are based upon the first linear-time temporal logic for I/O automata. In contrast to existing logics, formulas are evaluated over sequences of alternating states and actions which may be finite. In part II of this paper the realization of the entire theory is described using the theorem prover Isabelle and different model checking tools.     «

I/O automata are used to specify and reason about distributed, reactive systems. In this paper we extend standard I/O automata by a theory of abstraction. The intention is to combine theorem proving and model checking. Verifying both temporal properties and implementation relations is reduced to finite-state model checking. Even for livenness proofs merely simple first-order proof obligations remain for theorem proving. Furthermore, a methodology is developed which allows an incremental improvem...     »