A Verification Environment for I/O Automata -- Part II: Theorem Proving and Model Checking --

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 proving meta theory (HOLCF) and simplicity and efficiency for system verification (HOL).     «

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...     »