Benutzer: Gast  Login
Dokumenttyp:
Technical Report 
Autor(en):
Olaf Mueller 
Titel:
A Verification Environment for I/O Automata Based on Formalized Meta-Theory 
Abstract:
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...    »
 
Stichworte:
embedded systems; verification; model checking; theorem proving; meta theory; I/O automata; abstraction; temporal logic 
Jahr:
1998 
Jahr / Monat:
1998-09-01 00:00:00 
Seiten/Umfang:
285