Specification of stochastic properties with CSP

The research in formal specification and verification of complex systems has often ignored the specification of stochastic properties of the system. We are exploring new methodologies and tools to permit stochastic analysis of CSP-based systems specifications. In doing so, we have investigated the relationship between specification models and stochastic models by translating the specification into another form that is amenable to such analyses (e.g., from CSP to stochastic Petri Nets). This process can give insight for further refinements of the original specification (i.e., identify potential failure processes and recovery actions). It does this by relating the parameters needed for reliability analysis to user level specifications which is essential for realizing systems that meet the users needs in terms of cost, functionality, performance and reliability