loading...
Verifying Stochastic Well-formed Nets with CSL Model-Checking Tools
Turku, Finland June 28-June 30
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ACSD.2006.36Sixth International Conference on App ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
D. Cerotti, Universita di Torino, Torino, Italy
D. D?Aprile, Universita di Torino, Torino, Italy
S. Donatelli, Universita di Torino, Torino, Italy
J. Sproston, Universita di Torino, Torino, Italy
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.
Citation:
D. Cerotti, D. D?Aprile, S. Donatelli, J. Sproston, "Verifying Stochastic Well-formed Nets with CSL Model-Checking Tools," acsd, pp.143-152, Sixth International Conference on Application of Concurrency to System Design (ACSD'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.