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.
|Cite as: Ndukwu, U. and Sanders, J.W. (2009). Reasoning about a Distributed Probabilistic System. In Proc. Fifteenth Computing: The Australasian Theory Symposium (CATS 2009), Wellington, New Zealand. CRPIT, 94. Downey, R. and Manyem, P., Eds. ACS. 35-42. |
(local if available)