You are required to read and agree to the below before accessing a full-text version of an article in the IDE article repository.

The full-text document you are about to access is subject to national and international copyright laws. In most cases (but not necessarily all) the consequence is that personal use is allowed given that the copyright owner is duly acknowledged and respected. All other use (typically) require an explicit permission (often in writing) by the copyright owner.

For the reports in this repository we specifically note that

  • the use of articles under IEEE copyright is governed by the IEEE copyright policy (available at
  • the use of articles under ACM copyright is governed by the ACM copyright policy (available at
  • technical reports and other articles issued by Mälardalen University is free for personal use. For other use, the explicit consent of the authors is required
  • in other cases, please contact the copyright owner for detailed information

By accepting I agree to acknowledge and respect the rights of the copyright owner of the document I am about to access.

If you are in doubt, feel free to contact

Model Checking-Based Software Testing for Function Block Diagrams


Licentiate presentation

Start time:

2014-11-07 10:15

End time:

2014-10-07 12:15


Room Zeta, MDH, Västerås

Contact person:


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. 


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.


Eduard Paul Enoiu,