A compositional proof system for real-time systems based on explicit clock temporal logic

摘要

To specify timing properties of real-time systems, the authors consider explicit clock temporal logic. Programs are written in an Occam-like real-time language. A proof system is provided to formally verify that a program satisfies a specification expressed in the real-time version of temporal logic. The proof system is compositional, sound, and relatively complete.