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


Publication Type:



During the last decade, testing with model-checking techniques for software-intensive systems has been developed based on the theory of model-checking. However, the main problem in using model-checking for testing industrial software systems is the potential combinatorial explosion of the state space and its limited application to models used in practice. In this thesis, we improve the current status of testing with model-checking techniques by developing a framework suitable for transforming Function Block Diagrams (FBD), a widely used model in safety-critical software applications, to a formal representation of both its functional and timing behavior. For this, we implement an automatic model-to-model transformation to timed automata. The transformation accurately reflects the data-flow characteristics of the FBD language by constructing a complete behavioral model which assumes a read-execute-write program semantics. In addition, we develop a test case generation technique based on model-checking, tailored for structural coverage of FBD programs. We de fine logic coverage for FBD programs based on the transformed timed automata model. This copes with both functional and timing behavior of an FBD program. This formal defi nition is necessary for the approach to be applicable to model-checking. We present how a model-checker can be used to generate test cases for covering an FBD program. The developed techniques have been implemented in a testing tool. To demonstrate the potential applications of our techniques, we present a framework for testing FBD programs and a case study where the tool and its methodology are applied. Based on our experiments, this method is -for the real world models provided by Bombardier Transportation AB- a useful and applicable way of generating test cases.


author = {Eduard Paul Enoiu},
title = {Model Checking-Based Software Testing for Function Block Diagrams},
month = {November},
year = {2013},
url = {}