Analysis of real-time concurrent systems models based on CSP using Stochastic Petri nets

This paper addresses the real-time and reliability analysis of models for concurrent systems. Such models define independent entities that cooperate by explicit communication. Communications represent visible actions which, if they do not occur or are delayed beyond their deadline, will cause a failure to occur. This approach converts a formal functional system description into the information needed to predict its behavior as a function of observable parameters (i.e., topology, fault-tolerance, deadlines, communications and failure categories). The CSP-based models are translated into Stochastic Petri nets (SPNs) using our tool CSPN (CSP-to-Stochastic Petri Nets).(1) CSPN uses algorithms which codify the canonical translations between essential CSP constructs and SPNs. The term "CSP-based" is used to distinguish between the exact notation of Hoare's original CSP and our textual representations which ate similar to I occam2. The CSP-based t grammar preserve the structural properties of the original model. Consideration of other CSP properties (e.g., traces, refusal sets, livelock, etc.) are nor precluded, however they are not considered here. A basic example is provided to illustrate the link between failure behavior and model characteristics (i.e., derivation of timing failure probability and reliability predictions as they would affect the cost for implementing a candidate model specification).