The need to explore new formalisms for specifying, implementing, and verifying systems is driven by the increasing complexity of systems we wish to analyze and synthesize. At the same time, there is a growing realization of the need for techniques to work in the context of incomplete knowledge. Probabilistic formalisms allow modeling incomplete knowledge of a system in the form of probability distributions and even enable some useful analysis of these systems.

This paper advances the state of the art by proposing a formalism--stochastic hybrid communicating sequential processes (SHCSP)--that can combine aspects of distributed systems, real-time physical systems, and probabilistic systems. It proposes a mechanism for combining mathematical formalisms for individual aspects into a coherent whole and delineates interactions between different aspects of the formalism. SHCSP is provided with an operational semantics that can be used for simulation. The authors also formulate sound axiomatic semantics for reasoning about properties of SHCSP processes. This is done from the ground up by first describing a logical language of assertions for describing properties and formulating sound rules of inference in the form of pre-/post-condition triples that can be used to reason about the evolution of SHCSP processes. The inference system is inspired by Hoare logic and assume-guarantee reasoning.

The material in the paper is quite dense and requires commitment in following up with the bibliography to understand the mathematical foundations of each aspect addressed in the paper: CSP, hybrid systems, and stochastic systems. The example provided in the paper is sketchy, and it is difficult to see how the rules of inference could be automated or could apply to larger examples--in particular, the compositional nature of the inference system is difficult to appreciate from the example.