Reasoning about a Distributed Probabilistic System

Reasoning about a distributed system that exhibits a combination of probabilistic and temporal behaviour does not seem to be easy with current techniques. The reason is the interaction between probability and abstraction (local block), made worse by remote synchronisation. The formalism of process algebra has not so far provided much insight, and so the alternative of shared-variable concurrency has been explored. In this paper the recently proposed language ptsc (for probability, time and shared-variable concurrency) is extended by constructs for interleaving and local block. Both enhance a designer's ability to modularise a design; the latter also permits a design to be compared with its more abstract specification, by concealing appropriately chosen design variables. Laws of the extended language are studied and applied in a case study consisting of a faulty register-transfer-level design.