Ninth Annual IEEE Symposium on

Logic in Computer Science (LICS 1994)

Paper: Compositional verification of real-time systems (at LICS 1994)

Authors: Edward Chang Zohar Manna Amir Pnueli


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


    author = 	 {Edward Chang and Zohar Manna and Amir Pnueli},
    title = 	 {Compositional verification of real-time systems},
    booktitle =  {Proceedings of the Ninth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1994},
    year =	 1994,
    editor =	 {Samson Abramsky},
    month =	 {July}, 
    pages =      {458--465},
    location =   {Paris, France}, 
    publisher =	 {IEEE Computer Society Press}