Experiences with formal engineering: model-based specification, implementation and testing of a software bus at Neopost

M. Sijtema, G. Salaün (Editor), B. Schätz (Editor), Axel Belinfante, Mariëlle Ida Antoinette Stoelinga, L. Marinelli

  • 6 Citations

Abstract

We report on the actual industrial use of formal methods during the development of a software bus. During an internship at Neopost Inc., of 14 weeks, 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 (mdev), 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. The findings above, reported earlier by us in (Sijtema et al., 2011) [1], were well- received, also in industrially oriented conferences (Ferreira and Romanenko, 2010) [2] and [3]. In this paper, we look back on the case study, and carefully analyze its merits and shortcomings. We reflect on (1) the added benefits of model checking, (2) model completeness and (3) the quality and performance of the test process. Thus, in a second phase, after the internship, we model checked the XBus protocol—this was not done in [1] since the Neopost business process required a working implementation after 14 weeks. We used the CADP tool evaluator4 to check the behavioral requirements obtained during the development. Model checking did not uncover errors in model mdev, but revealed that model mdev was neither complete nor optimized: in particular, requirements to the so-called bad weather behavior (exceptions, unexpected inputs, etc.) were missing. Therefore, we created several improved models, checked that we could validate them, and used them to analyze quality and performance of the test process. Model checking was expensive: it took us approx. 4 weeks in total, compared to 3 weeks for the entire model-based testing approach during the internship. In the second phase, we analyzed the quality and performance of the test process, where we looked at both code and model coverage. We found that high code coverage (almost 100%) is in most cases obtained within 1000 test steps and 2 minutes, which matches the fact that the faults in the XBus were discovered within a few minutes. Summarizing, we firmly believe that the formal engineering approach is cost-effective, and produces high quality software products. Model checking does yield significantly better models, but is also costly. Thus, system developers should trade off higher model quality against higher costs.
Original languageUndefined
Pages (from-to)188-209
Number of pages22
JournalScience of computer programming
Volume80
Issue numberPart A
DOIs
StatePublished - 1 Feb 2014

Fingerprint

Model checking
Formal methods
Testing
Costs
Algebra
Servers
Simulators
Industry

Keywords

  • EWI-23994
  • CADP
  • LPS
  • LTSMIN
  • evaluator4
  • mCRL2
  • lps2torx
  • EC Grant Agreement nr.: FP7/318490
  • EC Grant Agreement nr.: FP7/2007-2013
  • EC Grant Agreement nr.: FP7/318003
  • Formal Methods
  • Formal engineering
  • Model-Based Testing
  • IOCO
  • MCL
  • METIS-303971
  • IR-88365
  • JTorX

Cite this

Sijtema, M.; Salaün, G. (Editor); Schätz, B. (Editor); Belinfante, Axel; Stoelinga, Mariëlle Ida Antoinette; Marinelli, L. / Experiences with formal engineering: model-based specification, implementation and testing of a software bus at Neopost.

In: Science of computer programming, Vol. 80, No. Part A, 01.02.2014, p. 188-209.

Research output: Scientific - peer-reviewArticle

@article{a3791ccdce7048319de7b9e64b335bbb,
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. During an internship at Neopost Inc., of 14 weeks, 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 (mdev), 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. The findings above, reported earlier by us in (Sijtema et al., 2011) [1], were well- received, also in industrially oriented conferences (Ferreira and Romanenko, 2010) [2] and [3]. In this paper, we look back on the case study, and carefully analyze its merits and shortcomings. We reflect on (1) the added benefits of model checking, (2) model completeness and (3) the quality and performance of the test process. Thus, in a second phase, after the internship, we model checked the XBus protocol—this was not done in [1] since the Neopost business process required a working implementation after 14 weeks. We used the CADP tool evaluator4 to check the behavioral requirements obtained during the development. Model checking did not uncover errors in model mdev, but revealed that model mdev was neither complete nor optimized: in particular, requirements to the so-called bad weather behavior (exceptions, unexpected inputs, etc.) were missing. Therefore, we created several improved models, checked that we could validate them, and used them to analyze quality and performance of the test process. Model checking was expensive: it took us approx. 4 weeks in total, compared to 3 weeks for the entire model-based testing approach during the internship. In the second phase, we analyzed the quality and performance of the test process, where we looked at both code and model coverage. We found that high code coverage (almost 100%) is in most cases obtained within 1000 test steps and 2 minutes, which matches the fact that the faults in the XBus were discovered within a few minutes. Summarizing, we firmly believe that the formal engineering approach is cost-effective, and produces high quality software products. Model checking does yield significantly better models, but is also costly. Thus, system developers should trade off higher model quality against higher costs.",
keywords = "EWI-23994, CADP, LPS, LTSMIN, evaluator4, mCRL2, lps2torx, EC Grant Agreement nr.: FP7/318490, EC Grant Agreement nr.: FP7/2007-2013, EC Grant Agreement nr.: FP7/318003, Formal Methods, Formal engineering, Model-Based Testing, IOCO, MCL, METIS-303971, IR-88365, JTorX",
author = "M. Sijtema and G. Salaün and B. Schätz and Axel Belinfante and Stoelinga, {Mariëlle Ida Antoinette} and L. Marinelli",
note = "Foreground=85%; Type of activity = publication; Main leader=UT; Type of audience = scientific community; Size of audience = n.a.; Countries addressed = international;",
year = "2014",
month = "2",
doi = "10.1016/j.scico.2013.04.009",
volume = "80",
pages = "188--209",
journal = "Science of computer programming",
issn = "0167-6423",
publisher = "Elsevier",
number = "Part A",

}

Experiences with formal engineering: model-based specification, implementation and testing of a software bus at Neopost. / Sijtema, M.; Salaün, G. (Editor); Schätz, B. (Editor); Belinfante, Axel; Stoelinga, Mariëlle Ida Antoinette; Marinelli, L.

In: Science of computer programming, Vol. 80, No. Part A, 01.02.2014, p. 188-209.

Research output: Scientific - peer-reviewArticle

TY - JOUR

T1 - Experiences with formal engineering: model-based specification, implementation and testing of a software bus at Neopost

AU - Sijtema,M.

AU - Belinfante,Axel

AU - Stoelinga,Mariëlle Ida Antoinette

AU - Marinelli,L.

A2 - Salaün,G.

A2 - Schätz,B.

N1 - Foreground=85%; Type of activity = publication; Main leader=UT; Type of audience = scientific community; Size of audience = n.a.; Countries addressed = international;

PY - 2014/2/1

Y1 - 2014/2/1

N2 - We report on the actual industrial use of formal methods during the development of a software bus. During an internship at Neopost Inc., of 14 weeks, 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 (mdev), 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. The findings above, reported earlier by us in (Sijtema et al., 2011) [1], were well- received, also in industrially oriented conferences (Ferreira and Romanenko, 2010) [2] and [3]. In this paper, we look back on the case study, and carefully analyze its merits and shortcomings. We reflect on (1) the added benefits of model checking, (2) model completeness and (3) the quality and performance of the test process. Thus, in a second phase, after the internship, we model checked the XBus protocol—this was not done in [1] since the Neopost business process required a working implementation after 14 weeks. We used the CADP tool evaluator4 to check the behavioral requirements obtained during the development. Model checking did not uncover errors in model mdev, but revealed that model mdev was neither complete nor optimized: in particular, requirements to the so-called bad weather behavior (exceptions, unexpected inputs, etc.) were missing. Therefore, we created several improved models, checked that we could validate them, and used them to analyze quality and performance of the test process. Model checking was expensive: it took us approx. 4 weeks in total, compared to 3 weeks for the entire model-based testing approach during the internship. In the second phase, we analyzed the quality and performance of the test process, where we looked at both code and model coverage. We found that high code coverage (almost 100%) is in most cases obtained within 1000 test steps and 2 minutes, which matches the fact that the faults in the XBus were discovered within a few minutes. Summarizing, we firmly believe that the formal engineering approach is cost-effective, and produces high quality software products. Model checking does yield significantly better models, but is also costly. Thus, system developers should trade off higher model quality against higher costs.

AB - We report on the actual industrial use of formal methods during the development of a software bus. During an internship at Neopost Inc., of 14 weeks, 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 (mdev), 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. The findings above, reported earlier by us in (Sijtema et al., 2011) [1], were well- received, also in industrially oriented conferences (Ferreira and Romanenko, 2010) [2] and [3]. In this paper, we look back on the case study, and carefully analyze its merits and shortcomings. We reflect on (1) the added benefits of model checking, (2) model completeness and (3) the quality and performance of the test process. Thus, in a second phase, after the internship, we model checked the XBus protocol—this was not done in [1] since the Neopost business process required a working implementation after 14 weeks. We used the CADP tool evaluator4 to check the behavioral requirements obtained during the development. Model checking did not uncover errors in model mdev, but revealed that model mdev was neither complete nor optimized: in particular, requirements to the so-called bad weather behavior (exceptions, unexpected inputs, etc.) were missing. Therefore, we created several improved models, checked that we could validate them, and used them to analyze quality and performance of the test process. Model checking was expensive: it took us approx. 4 weeks in total, compared to 3 weeks for the entire model-based testing approach during the internship. In the second phase, we analyzed the quality and performance of the test process, where we looked at both code and model coverage. We found that high code coverage (almost 100%) is in most cases obtained within 1000 test steps and 2 minutes, which matches the fact that the faults in the XBus were discovered within a few minutes. Summarizing, we firmly believe that the formal engineering approach is cost-effective, and produces high quality software products. Model checking does yield significantly better models, but is also costly. Thus, system developers should trade off higher model quality against higher costs.

KW - EWI-23994

KW - CADP

KW - LPS

KW - LTSMIN

KW - evaluator4

KW - mCRL2

KW - lps2torx

KW - EC Grant Agreement nr.: FP7/318490

KW - EC Grant Agreement nr.: FP7/2007-2013

KW - EC Grant Agreement nr.: FP7/318003

KW - Formal Methods

KW - Formal engineering

KW - Model-Based Testing

KW - IOCO

KW - MCL

KW - METIS-303971

KW - IR-88365

KW - JTorX

U2 - 10.1016/j.scico.2013.04.009

DO - 10.1016/j.scico.2013.04.009

M3 - Article

VL - 80

SP - 188

EP - 209

JO - Science of computer programming

T2 - Science of computer programming

JF - Science of computer programming

SN - 0167-6423

IS - Part A

ER -

Sijtema M, Salaün G, (ed.), Schätz B, (ed.), Belinfante A, Stoelinga MIA, Marinelli L. Experiences with formal engineering: model-based specification, implementation and testing of a software bus at Neopost. Science of computer programming. 2014 Feb 1;80(Part A):188-209. Available from, DOI: 10.1016/j.scico.2013.04.009