DocumentCode
1995764
Title
Compositional verification of real-time systems
Author
Chang, Edward ; Manna, Zohar ; Pnueli, Amir
Author_Institution
Dept. of Comput. Sci., Stanford Univ., CA, USA
fYear
1994
fDate
4-7 Jul 1994
Firstpage
458
Lastpage
465
Abstract
Presents a compositional proof system for the verification of real-time systems. Real-time systems are modeled as timed transition modules, which explicitly model interaction with the environment and may be combined using composition operators. Composition rules are devised such that the correctness of a system may be determined from the correctness of its components. These proof rules are demonstrated on Fischer´s mutual exclusion algorithm, for which mutual exclusion and bounded response are proven
Keywords
formal verification; real-time systems; temporal logic; Fischer´s mutual exclusion algorithm; bounded response; composition operators; composition rules; compositional proof system; compositional verification; environmental interaction modelling; metric temporal logic; proof rules; real-time system; system correctness; timed transition modules; Computer science; Contracts; Logic; Real time systems; Specification languages; Timing; Vocabulary;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1994. LICS '94. Proceedings., Symposium on
Conference_Location
Paris
Print_ISBN
0-8186-6310-3
Type
conf
DOI
10.1109/LICS.1994.316045
Filename
316045
Link To Document