Model Checking-Based Software Testing for Function Block Diagrams

The public defense of Eduard Paul Enoiu licentiate thesis in Computer Science and Engineering will take place at Mälardalen University on November 7, 2014, at 10.15 AM in room Zeta, Västerås.

Thesis Title: Model Checking-Based Software Testing for Function Block Diagrams

The examining committee consists of Professor Mohammad Reza Mousavi, Halmstad University; Professor Kristina Lundqvist, MDH; Associate Professor Andreas Ermedahl; Among the members of the examining committee, Professor Mohammad Reza Mousavi has been appointed the faculty examiner. Reserve; Professor Maria Lindén, MDH. Advisors: Paul Pettersson, Daniel Sundmark and Adnan Causevic. 

SUMMARY:

Software testing becomes more complex, more time-consuming, and more expensive. The risk that software errors remain undetected and cause critical failures increases. Consequently, in safety-critical development, testing software is standardized and it requires an engineer to show that tests fully exercise, or cover, the logic of the software. This method often requires a trained engineer to perform manual test generation, is prone to human error, and is expensive or impractical to use frequently in production. To overcome these issues, software testing needs to be performed earlier in the development process, more frequently, and aided by automated tools.

Eduard Enoiu, a Phd Student at Mälardalen University, has devised an automated test generation tool called CompleteTest that avoids many of those problems. The method implemented in the tool and described in this thesis, works with software written in Function Block Diagram language, and can provide tests in just a few seconds. In addition, it does not rely on the expertise of a researcher specialized in automated test generation and model checking. Although CompleteTest itself uses a model checker, a complex technique requiring a high level of expertise to generate tests, it provides a straightforward tabular interface to the intended users. In this way, its users do not need to learn the intricacies of using this approach such as how coverage criteria can be formalized and used by a model checker to automatically generate tests. If the technique can be demonstrated to work in production, it could detect and aid in the detection of errors in safety-critical software development, where conventional testing is not always applicable and efficient.

 Eduard conducted studies based on industrial use-case scenarios from Bombardier Transportation AB, showing how the approach can be applied to generate tests in software systems used in the safety-critical domain. To evaluate the approach, it was applied on real-world programs. The results indicate that it is efficient in terms of time required to generate tests and scales well for most of the software. There are still issues to resolve before the technique can be applied to more complex software, but Eduard and his collaborators are already working on ways to overcome them. In particular, we need to understand how its usage in practice can vary depending on human and software process factors.