Refinement-Based Verification of Interactive Real-Time Systems

Formal specification provides a system description that is much more precise than the natural language one and it can help to solve a lot of specification problems. But even a formal specification of a system can contain mistakes or can disagree with system's requirements. To cover this, we integrate a specification framework with a verification system. Given a system, represented in a formal specification framework Focus, one can verify its properties by translating the specification to a Higher-Order Logic and subsequently using the theorem prover Isabelle/HOL. Moreover, using this approach one can validate the refinement relation between two given systems. The approach uses the idea of refinement-based verification: we see any proof about a system as the proof that a more concrete system specification is a refinement of a more abstract one. The case when one needs to prove a single property of a system specification can also be seen as a refinement relation: this property can be defined as a Focus specification itself and then one needs just show that the system specification is its refinement. The major aspects of this approach are exemplified here by a case study on telematics (electronic data transmission) gateway.