Model-Based Testing Directed by Structural Coverage and Functional Requirements

Safety-critical systems verification is required to be developed under stringent standard and certification. Formal models are built as an abstraction of the system in upstream design phases. This article presents a new model-based testing process intended for verification of models with respect to functional requirements, as part of the "CONNEXION" French nuclear I and C methodology project. Based on the functional requirements of the system, a functional test suite is generated and executed on the model of the system. Then the structural coverage of the test suite is measured. Regardless of the coverage metrics, the unit of coverage measurement on the model is defined as a structural unit (SU). Assuming the existence of uncovered structural units, a reachability check on every SU is performed by model checking, to verify if this SU can be executed by any test. For reachable SU, the model checker generates test data to cover this SU and possibly others. These test data need to be combined with functional requirements to construct new test representing functionally realistic scenarios. Unreachable SU are recorded for further analysis since they can be suspected to be dead code or even a bug. The possibility that the model checker can stop its execution without providing an answer to the reachability check is also considered. The process is designed in particular for a system composed of sub-systems modeled in different languages, as one case study proposed in "CONNEXION". Application of our process to this case study is enabled by the unique modeling and verification tool box provided by partners of the project.