This paper presents the experience of modeling land transportation domain in the formal framework of Event-B. Well-specified requirements are crucial for good software design; they depend on the understanding of the domain. Thus, domain engineering becomes an essential activity. The possibility to have a formal model of a domain, consistent with the use of formal methods for developing critical software working within it, is an important issue. Safety-critical domains, like transportation, exhibit interesting features, such as high levels of nondeterminism, complex interactions, stringent safety properties, and multifaceted timing attributes. The formal representation of these features is a challenging task. The possibility of utilizing Event-B as a domain engineering tool is explored. It is shown how the problems faced during this exercise are tackled. Special attention is devoted to the issue of the validation of the model, in particular with a technique based on the animation of specifications. Event-B is mature enough to be an effective tool to model domains except in some areas, temporal properties mainly, where more work is still needed.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Utilizing Event-B for domain engineering: a critical analysis


    Additional title:

    Einsatz von Element-B für das Domain-Engineering: Eine kritische Analyse


    Contributors:


    Publication date :

    2011


    Size :

    17 Seiten, 6 Bilder, 47 Quellen




    Type of media :

    Conference paper


    Type of material :

    Print


    Language :

    English




    Vehicle recording system utilizing event detection

    SCHUMACHER DARREN | European Patent Office | 2023

    Free access

    VEHICLE RECORDING SYSTEM UTILIZING EVENT DETECTION

    SCHUMACHER DARREN | European Patent Office | 2020

    Free access

    Critical Event Reporting Tool (CERT)

    D. A. Wiegmann / T. L. von Thaden | NTIS | 2001


    Measuring Critical Charges For Single-Event Upsets

    Buehler, Martin G. / Blaes, Brent R. | NTRS | 1988


    Final Arrangements for Racecar Engineering Event

    British Library Online Contents | 1998