In this paper we present a logical characterization, by means of ACTL formulae, of safety requirements to be formally verified over safety critical complex systems. In this class of systems the formal verification of requirements is often hardened by state explosion problems. To deal with this problem, the characterization we propose allows the satisfiability of a safety requirement over a complex system to be derived by its satisfiability over those component subsystems that are directly involved in the given requirement. The proposed methodology has been successfully used for the formal verification of safety requirements of a particular system, that is a railway computer based signalling control system.

Formal Verification of Safety Requirements on Complex Systems

BERNARDESCHI, CINZIA;
1996-01-01

Abstract

In this paper we present a logical characterization, by means of ACTL formulae, of safety requirements to be formally verified over safety critical complex systems. In this class of systems the formal verification of requirements is often hardened by state explosion problems. To deal with this problem, the characterization we propose allows the satisfiability of a safety requirement over a complex system to be derived by its satisfiability over those component subsystems that are directly involved in the given requirement. The proposed methodology has been successfully used for the formal verification of safety requirements of a particular system, that is a railway computer based signalling control system.
1996
9783540760702
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: https://hdl.handle.net/11568/50490
 Attenzione

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

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