JSD ≜ ΔCSP ⊕ TLZ — A Case Study

We present a case study in the use of JSD, a popular structural design method, as a unifying mechanism for formal notations addressing different aspects of a system design. An asynchronous variant of CSP is used to address issues relating to time-ordering of events and communication between processes, while TLZ (a hybrid of Z and TLA) addresses state-based aspects of the system design and permits the expression of timing constraints and fairness conditions. The result is a hybrid real-time design method, appropriate for particular classes of real-time systems. The novelty is that a structural design method (with simplified semantics) serves to provide various views of the design, with the benefits and proof systems of the various formal methods being maintained.