Mechanical Verication of Parameterized Real-Time Systems

Real-time systems often have to cope with an unbounded number of
components. For example, real-time operating system schedulers have to
be able to manage an arbitrarily large number of threads. This makes
verification hard because standard verification techniques for finite
system models (e.g. model checking) can at most be employed for
particular instances. There exist approaches that employ verification
techniques for the (automatic) verification of special sub-classes of
(mostly untimed) parameterized systems. However, there exist no
comprehensive and mechanized approaches to deal with general
parameterized real-time systems with complex system topologies.

To overcome this problem, we have developed a framework for the
mechanized verification of parameterized real-time systems. At the core
of our framework, we employ the process algebra Timed CSP. We have
developed a formalization of the operational semantics of Timed CSP
together with the notion of bisimulation equivalences in the
Isabelle/HOL theorem prover. With that, we can verify real-time
specifications with machine assistance. Additionally, to enable
automatic verification of finite instances, we have enriched the
framework by possibilities to transform  Timed CSP specifications into
the input language of the FDR2 refinement checker and the UPPAAL model
checker. We applied our framework the real-time operating system
scheduler of the BOSS operating system to demonstrate the effectiveness
of our framework for the comprehensive verification of parameterized
real-time systems.

In this talk, I will mainly address our overall framework and the
formalization of Timed CSP in the Isabelle/HOL theorem prover.