Reliability analysis of CSP specifications using Petri nets and Markov processes

In our research we are developing methodologies and tools to permit stochastic analyses of CSP-based system specifications. In this regard, we have been developing morphisms between CSP-based models and Petri net-based stochastic models. This process has given us insight for further refinements to the original CSP specifications (i.e., identify potential failure processes and recovery actions). In order to create systems that meet user needs in terms of cost, functionality, performance and reliability, it is essential to relate the parameters needed for reliability analysis to the user level specification