User: Guest  Login
Document type:
Technical Report
Author(s):
Olaf Mueller
Title:
A Verification Environment for I/O Automata -- Part II: Theorem Proving and Model Checking --
Abstract:
We describe a verification framework for I/O automata in Isabelle. It includes a temporal logic, proof support for showing implementation relations between live I/O automata, and a combination of Isabelle with model checking via a verified abstraction theory. The underlying domain-theoretic sequence model turned out to be especially adequate for these purposes. Furthermore, using a tailored combination of Isabelle's logics HOL and HOLCF we achieve two complementary goals: expressiveness for prov...     »
Keywords:
Verification; I/O Automata; Theorem Proving; Model Checking
Year:
1999
Year / month:
1999-06-01 00:00:00
Pages:
27
 BibTeX