Consistency verification of safety requirements is crucial for the success of safety-critical systems, particularly railway systems. However, this task often requires significant time spent on interaction and communication between domain experts, who possess in-depth knowledge of safety requirements in a specific domain, and formal experts, who have the necessary skills to apply verification tools and techniques. To enhance time efficiency and productivity, we propose an approach to empower domain experts with formal methods for verifying safety requirements’ consistency. This involves transforming natural requirements into formal models and using formal methods for verification. The approach also localizes inconsistent requirements to provide feedback to domain experts. Communication between domain experts and formal experts can be facilitated through the pattern language SafeNL. By adopting this approach, domain experts can utilize formal verification without extensive consultation with formal experts. Two practical case studies with CASCO Signal Ltd. validate its effectiveness, practicality, as well as a significant reduction of time compared to traditional methods (at least 90% reduction). This reduction in time is primarily due to reduced communication needs and more efficient localization. Evaluations show that SafeNL is user-friendly and the approach performs well in modular systems while scalability is somewhat limited.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Empowering Domain Experts With Formal Methods for Consistency Verification of Safety Requirements


    Contributors:
    Chen, Xiaohong (author) / Zhang, Juan (author) / Jin, Zhi (author) / Zhang, Min (author) / Li, Tong (author) / Chen, Xiang (author) / Zhou, Tingliang (author)

    Published in:

    Publication date :

    2023-12-01


    Size :

    1421812 byte




    Type of media :

    Article (Journal)


    Type of material :

    Electronic Resource


    Language :

    English



    Formal verification of safety requirements on complex systems

    Bernardeschi, C. / Fantechi, A. / Gnesi, S. | Tema Archive | 1996


    JRC2014-3759 Product-Based Safety Verification Using Formal Methods

    Georgiadis, S.K. / American Society of Mechanical Engineers | British Library Conference Proceedings | 2014


    Formal methods and temporal safety requirements: A level crossing application

    Defossez, F. / Bon, P. / Collart Dutilleul, S. | Tema Archive | 2007



    Formal Verification Toolkit for Requirements and Early Design Stages

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