A Calculus for the Specification, Design, and Verification of Distributed Concurrent Systems

A calculus for the specification and verification of distributed concurrent interactive real-time systems is introduced. Systems are specified by their interface behavior formalized by interface predicates and interface assertions. System designs in terms of architectures of distributed networks of interactive systems are constructed by concurrent composition of subsystems. The specification of system designs is calculated from the specifications of their subsystems. Verification is done by proof rules, which are based on the concepts of causality and realizability justified by the operational model in terms of generalized Moore machines, Moore machines not restricted to finite state spaces. The calculus supports interface specification and reasoning both about untimed as well as timed distributed concurrent systems. This includes the design of cyber-physical systems. Real-time is used, in particular, to specify time-sensitive behavior and to prove properties related to causality and realizability, properties that hold for all Moore machines. On this basis, a calculus is worked out and illustrated by small examples. The calculus is shown to be sound and relatively complete.