Title :
Compositional verification of real-time systems
Author :
Chang, Edward ; Manna, Zohar ; Pnueli, Amir
Author_Institution :
Dept. of Comput. Sci., Stanford Univ., CA, USA
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;
Conference_Titel :
Logic in Computer Science, 1994. LICS '94. Proceedings., Symposium on
Conference_Location :
Paris
Print_ISBN :
0-8186-6310-3
DOI :
10.1109/LICS.1994.316045
