Title :
Refinement and modular verification with observers
Author :
Merceron, Agathe ; Pinna, G. Michele
Author_Institution :
Sydney Univ., NSW, Australia
Abstract :
The formal verification of properties in reactive real-time systems is crucial, as these systems are often safety-critical ones. Refinement 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 systems, modular verification (from the point of view of the refining program) is best achieved with observers
Keywords :
formal verification; observers; real-time systems; safety-critical software; systems analysis; formal verification; modular verification; observers; reactive real-time systems; refinement; refining program; safety-critical systems; synchronous languages; system implementation; systems design; Automatic control; Buildings; Computer science; Environmental economics; Formal verification; Industrial electronics; Industrial plants; Logic; Real time systems; Transportation;
Conference_Titel :
Quality Software, 2000. Proceedings. First Asia-Pacific Conference on
Conference_Location :
Hong Kong
Print_ISBN :
0-7695-0825-1
DOI :
10.1109/APAQ.2000.883795
