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]
Titolo: | Oris: a Tool for Modeling, Verification and Evaluation of Real-Time Systems | |
Autori di Ateneo: | ||
Autori: | BUCCI, GIACOMO; CARNEVALI, LAURA; RIDI, LORENZO; VICARIO, ENRICO | |
Data di pubblicazione: | 2010 | |
Rivista: | ||
Volume: | 12 | |
Pagina iniziale: | 391 | |
Pagina finale: | 403 | |
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. | |
Handle: | http://hdl.handle.net/2158/395359 | |
Appare nelle tipologie: | 1a - Articolo su rivista |
File in questo prodotto:
File | Descrizione | Tipologia | Licenza | |
---|---|---|---|---|
JSTTT10.pdf | Versione finale referata (Postprint, Accepted manuscript) | DRM non definito | Administrator Richiedi una copia | |
JSTTT10-abstract.pdf | Altro | Open Access | Accesso pubblicoVisualizza/Apri |