An approach for machine-assisted verification of Timed CSP specifications

摘要

The real-time process calculus Timed CSP is capable of expressing properties such as deadlock-freedom and real-time constraints. It is therefore well-suited to model and verify embedded software. However, proofs about Timed CSP specifications are not ensured to be correct since comprehensive machine-assistance for Timed CSP is not yet available. In this paper, we present our formalization of Timed CSP in the Isabelle/HOL theorem prover, which we have formulated as an operational coalgebraic semantics together with bisimulation equivalences and coalgebraic invariants. This allows for semi-automated and mechanically checked proofs about Timed CSP specifications. Mechanically checked proofs enhance confidence in verification because corner cases cannot be overlooked. We additionally apply our formalization to an abstract specification with real-time constraints. This is the basis for our current work, in which we verify a simple real-time operating system deployed on a satellite. As this operating system has to cope with arbitrarily many threads, we use verification techniques from the area of parameterized systems for which we outline their formalization.