Verifying Stochastic Well-formed Nets with CSL Model-Checking Tools

Model-checking algorithms for continuous stochastic logic (CSL) properties have been introduced to facilitate the verification of stochastic systems against a variety of formally-defined performance indices. In this paper, we consider the application of CSL model-checking methods and tools to stochastic well-formed nets (SWN), a colored extension of stochastic Petri nets (SPN). Our approach is to connect an existing tool for the description and performance analysis of SWN, called GREATSPN, to two model-checking tools for CSL properties, namely PRISM and MRMC. We illustrate our approach using a simple example of resource usage. As a by-product of the implementation of the model translation from GREATSPN to PRISM, a method for unfolding SWN models into SPN models has been implemented, as a standalone, re-usable component