We describe a methodology for the construction of real-time tasking sets, which smoothly integrates a formal approach in both development and verification processes of the software life cycle. In the design stage, a timeline schema is used to specify concurrent processes with their dependencies and their expected temporal parameters. The schema is automatically translated into an equivalent preemptive Time Petri Net, which supports verification of the process architecture with respect to timeliness and sequencing requirements through state space analysis. The specification model drives the implementation stage enabling a disciplined coding of the process architecture on top of conventional primitives of a real-time operating system. At the same time, the preemptive Time Petri Net specification and the results of its state space analysis support functional testing enabling the construction of a time-sensitive Oracle and providing a metrics for coverage analysis. Computational experience in the Linux RTAI environment is reported to demonstrate the capability of the method to be effectively integrated in a practical approach.

Casting Preemptive Time Petri Nets in the Development Life Cycle of Real-Time Software / L. Carnevali; L. Sassoli; E. Vicario. - STAMPA. - (2007), pp. 291-300. (Intervento presentato al convegno Euromicro Conference on Real Time Systems (ECRTS) tenutosi a Pisa, Italia nel July 2007) [10.1109/ECRTS.2007.86].

Casting Preemptive Time Petri Nets in the Development Life Cycle of Real-Time Software

CARNEVALI, LAURA;SASSOLI, LUIGI;VICARIO, ENRICO
2007

Abstract

We describe a methodology for the construction of real-time tasking sets, which smoothly integrates a formal approach in both development and verification processes of the software life cycle. In the design stage, a timeline schema is used to specify concurrent processes with their dependencies and their expected temporal parameters. The schema is automatically translated into an equivalent preemptive Time Petri Net, which supports verification of the process architecture with respect to timeliness and sequencing requirements through state space analysis. The specification model drives the implementation stage enabling a disciplined coding of the process architecture on top of conventional primitives of a real-time operating system. At the same time, the preemptive Time Petri Net specification and the results of its state space analysis support functional testing enabling the construction of a time-sensitive Oracle and providing a metrics for coverage analysis. Computational experience in the Linux RTAI environment is reported to demonstrate the capability of the method to be effectively integrated in a practical approach.
2007
Proceedings of the 19th Euromicro Conference on Real Time Systems (ECRTS 2007)
Euromicro Conference on Real Time Systems (ECRTS)
Pisa, Italia
July 2007
L. Carnevali; L. Sassoli; E. Vicario
File in questo prodotto:
File Dimensione Formato  
ECRTS07.pdf

Accesso chiuso

Tipologia: Versione finale referata (Postprint, Accepted manuscript)
Licenza: Tutti i diritti riservati
Dimensione 7.74 MB
Formato Adobe PDF
7.74 MB Adobe PDF   Richiedi una copia

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

Utilizza questo identificatore per citare o creare un link a questa risorsa: https://hdl.handle.net/2158/432197
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 0
social impact