The First Asia-Pacific Conference on Quality Software (APAQS'00)
Refinement and Modular Verification with Observers
Hong Kong, China
October 30-October 31
ISBN: 0-7695-0825-1
The formal verification of properties in reactive Real-Time system is crucial, as these systems are often safety-critical ones. Refinements is a relevant operation in synchronous languages. In this paper, we argue that, in the synchronous approach to the design and implementation of reactive Real-Time system, the modular verification from the point of view of the refining program is best achieved with observers.