Automated Compositional Proofs for Real-Time Systems

We present a framework for formally proving that the composition of the behaviors of the dierent parts of a complex, real-time system ensures a desired global speci cation of the overall system. The framework is based on a simple compositional rely/guarantee circular inference rule, plus a methodology concerning the integration of the dierent parts into a whole system. The reference specication language is the TRIO metric linear temporal logic. The novelty of our approach with respect to existing compositional frameworks | most of which do not deal explicitly with real-time requirements | consists mainly in its generality and abstraction from any assumptions about the underlying computational model and from any semantic characterizations of the temporal logic language used in the specication. Moreover, the framework deals equally well with continuous and discrete time. It is supported by a tool, implemented on top of the proof-checker PVS, to perform deduction-based verication through theoremproving of modular real-time axiom systems. As an example of application, we show the verication of a real-time version of the old-fashioned but still relevant \benchmark" of the dining philosophers problem.