Model Checking-Based Software Testing for Function Block Diagrams

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.