Real-time critical systems require extensive analysis. The potentially large damages caused by failures of real-time critical systems justify the use of expensive verification techniques, such as timed reachability analysis. Unfortunately the costs of timed reachability analysis inhibits its systematic application at the early stages of development, when long verification sessions could slow down the development process. Moreover, the large reachability space built for proving temporal properties reduces the size of specification for which timed reachability analysis can be applied. In this paper we show how reachability analysis of the non temporized underlying petri net can reduce the size of timed reachability analysis. In this way, timed reachability analysis can be used for analyzing industrial-size safety critical systems, paying an acceptable overhead

A Non-Temporized Approach for Temporized Analysis

1998

Abstract

Real-time critical systems require extensive analysis. The potentially large damages caused by failures of real-time critical systems justify the use of expensive verification techniques, such as timed reachability analysis. Unfortunately the costs of timed reachability analysis inhibits its systematic application at the early stages of development, when long verification sessions could slow down the development process. Moreover, the large reachability space built for proving temporal properties reduces the size of specification for which timed reachability analysis can be applied. In this paper we show how reachability analysis of the non temporized underlying petri net can reduce the size of timed reachability analysis. In this way, timed reachability analysis can be used for analyzing industrial-size safety critical systems, paying an acceptable overhead
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS 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/11582/1523
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact