TY - GEN
T1 - Verifying stochastic well-formed nets with CSL model-checking tools
AU - Cerotti, D.
AU - D'Aprile, D.
AU - Donatelli, S.
AU - Sproston, J.
PY - 2006
Y1 - 2006
N2 - 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 modelchecking 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.
AB - 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 modelchecking 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.
UR - http://www.scopus.com/inward/record.url?scp=45149113373&partnerID=8YFLogxK
U2 - 10.1109/ACSD.2006.36
DO - 10.1109/ACSD.2006.36
M3 - Conference contribution
SN - 0769525563
SN - 9780769525563
T3 - Proceedings - International Conference on Application of Concurrency to System Design, ACSD
SP - 143
EP - 152
BT - Proceedings - Sixth International Conference on Application of Concurrency to System Design, ACSD 2006
T2 - 6th International Conference on Application of Concurrency to System Design, ACSD 2006
Y2 - 28 June 2006 through 30 June 2006
ER -