DocumentCode
2626679
Title
Refinement and modular verification with observers
Author
Merceron, Agathe ; Pinna, G. Michele
Author_Institution
Sydney Univ., NSW, Australia
fYear
2000
fDate
2000
Firstpage
216
Lastpage
225
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Quality Software, 2000. Proceedings. First Asia-Pacific Conference on
Conference_Location
Hong Kong
Print_ISBN
0-7695-0825-1
Type
conf
DOI
10.1109/APAQ.2000.883795
Filename
883795
Link To Document