Sep 13, 2011: Mariëlle Stoelinga and Axel Belinfante: Experience from Practice: Formal Engineering the XBus at Neopost

September 13, 2011Experience from Practice: Formal Engineering the XBus at Neopost
Room: Zi 5126Mariëlle Stoelinga and Axel Belinfante

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.