The public defense of Eduard Paul Enoius licentiate thesis (IDT)

Datum: 2014-11-07
Tid: 10.15
Plats: Mälardalen University, room Zeta, Västerås

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.

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

Subtitle: Tool-supported automatic test generation enables more efficient industrial control software testing.

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.

The Licentiate thesis has serial number 182.


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 software development, testing control software is standardized and it requires a tester to show that tests fully exercise, or cover, the logic of the software. This method often requires a trained tester 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 a licentiate thesis, works with Function Block Diagram software, 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 software errors in train control software, 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, they need to understand how its usage in practice can vary depending on human and software process factors.