Experiences with Formal Engineering: Model-Based Specification, Implementation and Testing of a Software Bus at Neopost

Marten Sijtema, Mariëlle Ida Antoinette Stoelinga, Axel Belinfante, Lawrence Marinelli

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    3 Citations (Scopus)
    77 Downloads (Pure)

    Abstract

    We report on the actual industrial use of formal methods during the development of a software bus. At Neopost Inc., we developed the server component of a software bus, called the XBus, using formal methods during the design, validation and testing phase: We modeled our design of the XBus in the process algebra mCRL2, validated the design using the mCRL2-simulator, and fully automatically tested our implementation with the model-based test tool JTorX. This resulted in a well-tested software bus with a maintainable architecture. Writing the model, simulating it, and testing the implementation with JTorX only took 17% of the total development time. Moreover, the errors found with model-based testing would have been hard to find with conventional test methods. Thus, we show that formal engineering can be feasible, beneficial and cost-effective.
    Original languageEnglish
    Title of host publication16th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2011
    EditorsGwen Salaün, Bernhard Schätz
    Place of PublicationBerlin
    PublisherSpringer
    Pages117-133
    Number of pages17
    ISBN (Print)978-3-642-24430-8
    DOIs
    Publication statusPublished - Aug 2011
    Event16th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2011 - Trento, Italy
    Duration: 29 Aug 201130 Aug 2011
    Conference number: 16

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume6959
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Workshop

    Workshop16th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2011
    Abbreviated titleFMICS
    CountryItaly
    CityTrento
    Period29/08/1130/08/11

    Keywords

    • METIS-279685
    • Model-Based Testing
    • EWI-20768
    • EC Grant Agreement nr.: FP7/214755
    • EC Grant Agreement nr.: FP7-ICT-2007-1
    • IR-78451

    Fingerprint Dive into the research topics of 'Experiences with Formal Engineering: Model-Based Specification, Implementation and Testing of a Software Bus at Neopost'. Together they form a unique fingerprint.

    Cite this