Specification and Seamless Verification of Embedded Real-Time Systems - Focus on Isabelle
Maria Spichkova · mediaTUM – the media and publications repository of the Technical University Munich (Technical University Munich) · 2008
The purpose of this thesis is to create a coupling of the formal specification framework Focus in the generic theorem prover Isabelle/HOL, a logical framework based on Higher-Order Logic.The main focus of this work is on specification and verification of systems that are especially safety critical -embedded real-time systems.Isabelle/HOL is an interactive semi-automatic theorem prover and in the proofs of some system properties human time must be invested.These proofs strongly depend on the specifications of the system and the properties.By considering the framework "Focus on Isabelle", which is result of the coupling, we can influence the complexity of proofs already during the specification phase, e.g.reformulating specification to simplify the Isabelle/HOL proofs for a translated Focus specification.Thus, the specification and verification/validation methodologies are treated as a single, joined, methodology with the main focus on the specification part.This methodology uses particularly the idea of refinement-based verification, where the verification of system properties can be treated as a validation of a system specification with respect to the specification representing the properties.The key contributions of the thesis are Deep embedding of that part of the framework Focus, which is appropriate for the specification of real-time systems, into Isabelle/HOL."Focus on Isabelle" enables to validate and verify system specifications in a methodological way.I would like to thank all those people that have helped me, either directly or indirectly, with the development of this thesis.My special thanks go to my supervisor Manfred Broy.He gave me the opportunity to work in a highly qualifed research group and guided my activity in the past four years.