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. CCS Concepts: center dot Software and its engineering - Software notations and tools ; System description languages ; System modeling languages ; Development frameworks and environments ; Software as a service orchestration system; center dot Theory of computation - Logic ; Higher order logic ; Logic and verification; center dot Computing methodologies - Concurrent computing methodologies ; Concurrent programming languages ;