A Temporal-Logic Based Compositional Proof System for Real-Time Message Passing

摘要

We consider a model of real-time network computation in which synchronous communication events occur during (possibly overlapping) intervals along a dense time scale. A specification language for processes and networks based on real-time temporal logic is defined. We give a simple proof system for network specifications when specifications for component processes are given. The proof system is then extended for a version of real-time CSP, under the assumption that all communications take some fixed length of time. Finally, it is shown that this proof system can be modified to allow varying communication lengths. All versions of the proof system are compositional, sound, and relatively complete.