Oris is a tool for qualitative verification and quantitative evaluation of reactive timed systems, which supports modeling and analysis of various classes of timed extensions of Petri Nets. As most characterizing features, Oris implements symbolic state space analysis of preemptive Time Petri Nets, which enable schedulability analysis of real-time systems running under priority preemptive scheduling; and stochastic Time Petri Nets, which enable an integrated approach to qualitative verification and quantitative evaluation. In this paper, we present the current version of the tool and we illustrate its application to two different case studies in the areas of qualitative verification and quantitative evaluation, respectively.
Oris: a Tool for Modeling, Verification and Evaluation of Real-Time Systems / G. Bucci; L. Carnevali; L. Ridi; E. Vicario. - In: INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER. - ISSN 1433-2779. - ELETTRONICO. - 12:(2010), pp. 391-403. [10.1007/s10009-010-0156-8]
Oris: a Tool for Modeling, Verification and Evaluation of Real-Time Systems
BUCCI, GIACOMO;CARNEVALI, LAURA;RIDI, LORENZO;VICARIO, ENRICO
2010
Abstract
Oris is a tool for qualitative verification and quantitative evaluation of reactive timed systems, which supports modeling and analysis of various classes of timed extensions of Petri Nets. As most characterizing features, Oris implements symbolic state space analysis of preemptive Time Petri Nets, which enable schedulability analysis of real-time systems running under priority preemptive scheduling; and stochastic Time Petri Nets, which enable an integrated approach to qualitative verification and quantitative evaluation. In this paper, we present the current version of the tool and we illustrate its application to two different case studies in the areas of qualitative verification and quantitative evaluation, respectively.File | Dimensione | Formato | |
---|---|---|---|
JSTTT10.pdf
Accesso chiuso
Tipologia:
Versione finale referata (Postprint, Accepted manuscript)
Licenza:
DRM non definito
Dimensione
925.64 kB
Formato
Adobe PDF
|
925.64 kB | Adobe PDF | Richiedi una copia |
JSTTT10-abstract.pdf
accesso aperto
Tipologia:
Altro
Licenza:
Open Access
Dimensione
16.79 kB
Formato
Adobe PDF
|
16.79 kB | Adobe PDF |
I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.