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

Marten Sijtema; Mariëlle I.A. Stoelinga; Axel Belinfante; Lawrence Marinelli

doi:10.1007/978-3-642-24431-5_10

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

Marten Sijtema
, Mariëlle I.A. Stoelinga
, Axel Belinfante
, Lawrence Marinelli

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

3 Citations (Scopus)

252 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 language	English
Title of host publication	16th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2011
Editors	Gwen Salaün, Bernhard Schätz
Place of Publication	Berlin
Publisher	Springer
Pages	117-133
Number of pages	17
ISBN (Print)	978-3-642-24430-8
DOIs	https://doi.org/10.1007/978-3-642-24431-5_10
Publication status	Published - Aug 2011
Event	16th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2011 - Trento, Italy Duration: 29 Aug 2011 → 30 Aug 2011 Conference number: 16

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Volume	6959
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Workshop

Workshop	16th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2011
Abbreviated title	FMICS
Country/Territory	Italy
City	Trento
Period	29/08/11 → 30/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

Access to Document

10.1007/978-3-642-24431-5_10

Sijtema2011experiences-authorAccepted author version, 349 KB

Cite this

Sijtema, M., Stoelinga, M. I. A., Belinfante, A., & Marinelli, L. (2011). Experiences with Formal Engineering: Model-Based Specification, Implementation and Testing of a Software Bus at Neopost. In G. Salaün, & B. Schätz (Eds.), 16th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2011 (pp. 117-133). (Lecture Notes in Computer Science; Vol. 6959). Springer. https://doi.org/10.1007/978-3-642-24431-5_10

Sijtema, Marten ; Stoelinga, Mariëlle I.A. ; Belinfante, Axel et al. / Experiences with Formal Engineering : Model-Based Specification, Implementation and Testing of a Software Bus at Neopost. 16th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2011. editor / Gwen Salaün ; Bernhard Schätz. Berlin : Springer, 2011. pp. 117-133 (Lecture Notes in Computer Science).

@inproceedings{3e9f6452c1544ba496782d03ce31220a,

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

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.",

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

author = "Marten Sijtema and Stoelinga, \{Mari{\"e}lle I.A.\} and Axel Belinfante and Lawrence Marinelli",

note = "Foreground=85\%; Type of activity = publication; Main leader=UT; Type of audience = scientific community; Size of audience = n.a.; Countries addressed = international;; 16th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2011, FMICS ; Conference date: 29-08-2011 Through 30-08-2011",

year = "2011",

month = aug,

doi = "10.1007/978-3-642-24431-5\_10",

language = "English",

isbn = "978-3-642-24430-8",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "117--133",

editor = "Gwen Sala{\"u}n and Bernhard Sch{\"a}tz",

booktitle = "16th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2011",

address = "Germany",

}

Sijtema, M, Stoelinga, MIA, Belinfante, A & Marinelli, L 2011, Experiences with Formal Engineering: Model-Based Specification, Implementation and Testing of a Software Bus at Neopost. in G Salaün & B Schätz (eds), 16th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2011. Lecture Notes in Computer Science, vol. 6959, Springer, Berlin, pp. 117-133, 16th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2011, Trento, Italy, 29/08/11. https://doi.org/10.1007/978-3-642-24431-5_10

Experiences with Formal Engineering: Model-Based Specification, Implementation and Testing of a Software Bus at Neopost. / Sijtema, Marten; Stoelinga, Mariëlle I.A.; Belinfante, Axel et al.
16th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2011. ed. / Gwen Salaün; Bernhard Schätz. Berlin: Springer, 2011. p. 117-133 (Lecture Notes in Computer Science; Vol. 6959).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Experiences with Formal Engineering

T2 - 16th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2011

AU - Sijtema, Marten

AU - Stoelinga, Mariëlle I.A.

AU - Belinfante, Axel

AU - Marinelli, Lawrence

N1 - Conference code: 16

PY - 2011/8

Y1 - 2011/8

N2 - 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.

AB - 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.

KW - METIS-279685

KW - Model-Based Testing

KW - EWI-20768

KW - EC Grant Agreement nr.: FP7/214755

KW - EC Grant Agreement nr.: FP7-ICT-2007-1

KW - IR-78451

U2 - 10.1007/978-3-642-24431-5_10

DO - 10.1007/978-3-642-24431-5_10

M3 - Conference contribution

SN - 978-3-642-24430-8

T3 - Lecture Notes in Computer Science

SP - 117

EP - 133

BT - 16th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2011

A2 - Salaün, Gwen

A2 - Schätz, Bernhard

PB - Springer

CY - Berlin

Y2 - 29 August 2011 through 30 August 2011

ER -

Sijtema M, Stoelinga MIA, Belinfante A, Marinelli L. Experiences with Formal Engineering: Model-Based Specification, Implementation and Testing of a Software Bus at Neopost. In Salaün G, Schätz B, editors, 16th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2011. Berlin: Springer. 2011. p. 117-133. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-24431-5_10

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

Abstract

Publication series

Workshop

Keywords

Access to Document

Fingerprint

Cite this