Abstract - Formal methods based on state-space enumeration, such as Timed Automata and Time Petri Nets (TPN), have been proposed for designing and validating reactive real-time systems. The great expressiveness of these methods is coun- terbalanced by the increased complexity of the analysis, which may grow exponentially. Furthermore, the enumer- ated state-space needs to be inspected to identify critical behaviors with respect to sequencing and timing require- ments. This naturally leads to the implementation of tools supporting the different stages of the development process. In this paper we present Oris, an environment for build- ing, simulating, analyzing and validating complex real time systems specified in terms of an extended TPN formalism, named Preemptive Time Petri Nets. Oris includes not only the state-space enumeration engine, but also a number of modules which ease user interaction, and make it usable also by a designer with no specific experience in formal modelling.

ORIS: A TOOL FOR STATE-SPACE ANALYSIS OF REAL-TIME PREEMPTIVE SYSTEMS / G. BUCCI; L. SASSOLI; E. VICARIO. - STAMPA. - (2004), pp. 70-79. ((Intervento presentato al convegno QEST 2004 tenutosi a ENSCHEDE.

ORIS: A TOOL FOR STATE-SPACE ANALYSIS OF REAL-TIME PREEMPTIVE SYSTEMS

BUCCI, GIACOMO;VICARIO, ENRICO
2004

Abstract

Abstract - Formal methods based on state-space enumeration, such as Timed Automata and Time Petri Nets (TPN), have been proposed for designing and validating reactive real-time systems. The great expressiveness of these methods is coun- terbalanced by the increased complexity of the analysis, which may grow exponentially. Furthermore, the enumer- ated state-space needs to be inspected to identify critical behaviors with respect to sequencing and timing require- ments. This naturally leads to the implementation of tools supporting the different stages of the development process. In this paper we present Oris, an environment for build- ing, simulating, analyzing and validating complex real time systems specified in terms of an extended TPN formalism, named Preemptive Time Petri Nets. Oris includes not only the state-space enumeration engine, but also a number of modules which ease user interaction, and make it usable also by a designer with no specific experience in formal modelling.
QEST 2004
ENSCHEDE
G. BUCCI; L. SASSOLI; E. VICARIO
File in questo prodotto:
File Dimensione Formato  
Abstract Quest 2004.rtf

accesso aperto

Tipologia: Altro
Licenza: Open Access
Dimensione 7.97 kB
Formato RTF
7.97 kB RTF Visualizza/Apri
QEST04.pdf

accesso aperto

Tipologia: Altro
Licenza: Open Access
Dimensione 1.02 MB
Formato Adobe PDF
1.02 MB Adobe PDF Visualizza/Apri

I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/2158/18239
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact