Abstract

As Model-based Testing (MBT) approaches mature, they become a promising prospect for Safety-critical software systems testing. It is necessary to abide by RTCA DO-178C regarding requirement coverage, structural coverage, and traceability. The satisfaction of Modified Condition/Decision Coverage (MC/DC) is a must for avionics software certification. This thesis proposes a tool design for a test generation approach that satisfies the Modified Condition/Decision Coverage (MC/DC) and addresses path feasibility issues using constraints solving. The proposed methodology has several steps. It starts by transforming Low-Level Requirements (LLR), modelled as Extended Finite State Machines (EFSM), into a data-flow graph and a control-flow graph. Then, we highlight MC/DC information on both graphs, using graph labelling, before applying SMT-constraint solving to generate an executable test suite. Throughout, we keep records of the transformation between the models to prepare for requirements traceability as per RTCA DO-178C. The approach is based on the EFSM model, meaning that the assessment of MC/DC and other structural coverage criteria are on the model under the assumptions that the predicates are the same in the code and the model, and the model is valid.