Verifying stochastic well-formed nets with CSL model-checking tools

D. Cerotti, D. D'Aprile, S. Donatelli, J. Sproston

Risultato della ricerca: Capitolo in libro/report/atti di convegnoContributo a conferenzapeer review

Abstract

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.

Lingua originaleInglese
Titolo della pubblicazione ospiteProceedings - Sixth International Conference on Application of Concurrency to System Design, ACSD 2006
Pagine143-152
Numero di pagine10
DOI
Stato di pubblicazionePubblicato - 2006
Pubblicato esternamente
Evento6th International Conference on Application of Concurrency to System Design, ACSD 2006 - Turku, Finland
Durata: 28 giu 200630 giu 2006

Serie di pubblicazioni

NomeProceedings - International Conference on Application of Concurrency to System Design, ACSD
ISSN (stampa)1550-4808

???event.eventtypes.event.conference???

???event.eventtypes.event.conference???6th International Conference on Application of Concurrency to System Design, ACSD 2006
Paese/TerritorioFinland
CittàTurku
Periodo28/06/0630/06/06

Fingerprint

Entra nei temi di ricerca di 'Verifying stochastic well-formed nets with CSL model-checking tools'. Insieme formano una fingerprint unica.

Cita questo