Model-based Development and Testing of a Software Bus

Organisation:	University of Twente (THE NETHERLANDS)
Method:	mCRL2
Tools used:	JTorX mCRL2 LTSmin CADP (Construction and Analysis of Distributed Processes)
Domain:	Distributed Systems.
Period:	2011-2014
Size:	n/a.
Description:	Neopost Inc. is one of the largest companies in the world producing supplies and services for the mailing and shipping industry, like franking and mail inserting machines, and the XBus is a software bus that supports communication between mailing devices and software clients. The XBus allows clients to send XML-formatted messages to each other over TCP (the X in XBus stands for XML), and also implements a service-discovery mechanism. That is, clients can advertise their provided services and query and subscribe to services provided by others. This report describes the development of the XBus, which consisted in two phases: a first phase in which the XBus was developed at Neopost Inc., and a second, post-case study analysis phase, where the XBus protocol was analyzed by model checking, and the quality and performance of the model-based testing process was measured. First Phase: Developing the XBus. The XBus was developed using the classical V-model, and formal methods were used during the design and testing phase. An important step in the design phase was the creation of a behavioral model Mdev of the XBus, written in the process algebra mCRL2. Model Mdev pins down the interaction between the XBus and its environment in a mathematically precise way. The model was simulated to check its validity, which greatly increased the understanding of the XBus protocol, and simplified the implementation phase. The implementation i1 of the protocol was tested, distinguishing between data and protocol behavior. Data behavior concerns the input/output behavior of a function and is static, i.e., independent of the order of the methods calls. Protocol behavior relates to the business logic of the system, i.e., the interaction between the XBus and its clients. Unit testing was used to test the data behavior and model-based testing with JTorX was used for the protocol behavior. Second Phase: Analysis. The model Mdev created during the development phase was analyzed by model checking. A series of new models with different features were created, to obtain finite instances of Mdev. The EVALUATOR 4.0 tool from CADP was used to model check the XBus requirements obtained during the first phase, which were subsequently formulated in the logic MCL. The toolsets mCRL2 and LTSmin were used to obtain, from the mCRL2 model, the LTS in the BCG (Binary Coded Graph) format on which EVALUATOR 4.0 operates. Model checking did not uncover errors in model Mdev, which is not surprising, because model Mdev had been used extensively already in simulation and model-based testing, and because of the simple structure of the model. However, model checking revealed that model Mdev was not complete. In particular, those requirements related to so-called bad weather behavior were absent: invalid or unexpected messages were not modeled, and neither were empty lists of services. Finally, the thoroughness of the testing was extensively evaluated by measuring code coverage and model coverage. This was carried out on a carefully reconstructed implementation of the XBus. The metric used was branch coverage, which measures the percentage of all branches in the control flow graph that were executed during testing. For this purpose, the code of the (reconstructed) implementation was manually instrumented. Then, the tests were derived fully automatically using JTorX by doing a random walk over (the state space of) the model. The model and code coverage were extensively analyzed from short test runs (10,000 test steps, 5-30 minutes) and long ones (250,000 test steps, 2-40+ hours), with each of the (infinite) model versions. The maximal code coverage was typically reached after 1,000 test steps, i.e., after at most two minutes of testing.
Conclusions:	The formal engineering approach has been very successful for this case study: with limited overhead, a reliable software bus with a maintainable architecture was created. This clearly shows that formal engineering is not only beneficial for large, complex and/or safety-critical systems, but also for more modest projects. During the analysis phase, it was found that, within the limits of the model, the model-based testing done during the project was rather thorough. However, it was also found that the model, used to derive these tests, was not fully complete, and a more thorough analysis of the requirements during the project would have been desirable. This could have been achieved with model checking but at a higher cost. Finally, it was experienced that model and code coverage metrics can provide valuable insight in the quality, effectiveness, and progress of the model-based testing process. Based on this experience, one can advocate that formal engineering pays off, and that investing in high-quality models is worthwhile: the quality of model-driven development lies within the quality of the model.
Publications:	[Sijtema-Belinfante-Stoelinga-Marinelli-14] M. Sijtema, A. Belinfante, M.I.A. Stoelinga, and L. Marinelli. "Experiences with Formal Engineering: Model-Based Specification, Implementation and Testing of a Software Bus at Neopost". Science of Computer Programming 80(A):188-209, February 2014. Available on-line from http://doc.utwente.nl/88365/2/paper.pdf and from the CADP Web site in PDF or PostScript
Contact:	Marielle Stoelinga Dept. of Computer Science Zilverling building Formal Methods & Tools P.O. Box 217 7500 AE Enschede THE NETHERLANDS Tel: +31 53 489 3773 (voice) +31 53 489 3767 (secretary) Email: marielle@cs.utwente.nl
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page