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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
