In this paper the authors 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 the authors 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
Formale Verifikation von Sicherheitsanforderungen bei komplexen Systemen
1996
10 Seiten, 4 Bilder, 12 Quellen
Conference paper
English
Formal Verification of Safety-Critical Aerospace Systems
IEEE | 2023
|Formal requirements-based programming for complex systems
Tema Archive | 2005
|Formal verification method for safety diagnosis software
Automotive engineering | 2015
|