Compositional Verification of Timed Components using PVS
Marcel Kyas and Jozef Hooman
Appeared in: Proceedings Software Engineering 2006,
B. Biel and M. Book and V. Gruhn(eds.),
Lecture Notes in Informatics, Volume P-79,
pp. 143 - 154, 2006.
We present a general framework to support the compositional verification
of timed systems using the interactive theorem prover PVS. The framework is based on
timed traces that are an abstraction of the timed semantics of flat UML state machines.
We define a compositional proof rule for parallel composition and prove its soundness
in PVS. After composition, a hiding rule can be applied to hide internal events. The
general theories have been applied to parts of the Medium Altitude Reconnaissance
System (MARS) as deployed in the F-16 aircraft of the Royal Netherlands Air-Force.