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

Authors: Edward Y. Chang Zohar Manna Amir Pnueli

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

BibTeX

  @InProceedings{ChangMannaPnueli-Compositionalverifi,
    author = 	 {Edward Y. Chang and Zohar Manna and Amir Pnueli},
    title = 	 {Compositional verification of real-time systems},
    booktitle =  {Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS 1994)},
    year =	 {1994},
    month =	 {July}, 
    pages =      {458--465},
    location =   {Paris, France}, 
    publisher =	 {IEEE Computer Society Press}
  }