User: Guest  Login
Document type:
Technical Report 
Author(s):
Olaf Mueller 
Title:
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...    »
 
Keywords:
embedded systems; verification; model checking; theorem proving; meta theory; I/O automata; abstraction; temporal logic 
Year:
1998 
Year / month:
1998-09-01 00:00:00 
Pages:
285