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.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Formal verification of safety requirements on complex systems


    Additional title:

    Formale Verifikation von Sicherheitsanforderungen bei komplexen Systemen


    Contributors:
    Bernardeschi, C. (author) / Fantechi, A. (author) / Gnesi, S. (author)


    Publication date :

    1996


    Size :

    10 Seiten, 4 Bilder, 12 Quellen



    Type of media :

    Conference paper


    Type of material :

    Print


    Language :

    English





    Formal Verification of Safety-Critical Aerospace Systems

    Paul, Saswata / Cruz, Elkin / Dutta, Airin et al. | IEEE | 2023


    Formal requirements-based programming for complex systems

    Rash, J.L. / Hinchey, M.G. / Rouff, C.A. | Tema Archive | 2005


    Formal Verification Toolkit for Requirements and Early Design Stages

    Badger, Julia M. / Miller, Sheena Judson | NTRS | 2011


    Formal verification method for safety diagnosis software

    Narisawa,F. / Matsubara,M. / Nishi,M. et al. | Automotive engineering | 2015