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.
Citation:
Agathe Merceron, G. Michele Pinna, "Refinement and Modular Verification with Observers," apaqs, pp.216, The First Asia-Pacific Conference on Quality Software (APAQS'00), 2000 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||