User: Guest  Login
Title:

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

Document type:
Technical Report
Author(s):
Olaf Mueller
Abstract:
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...     »
Keywords:
I/O Automata; Verification; Temporal Logic; Abstraction
Year:
1999
Year / month:
1999-06-01 00:00:00
Pages:
25
 BibTeX