Automatic test case generation in model based software design to achieve higher reliability

Model based design methodology is increasingly being used in the development of software for embedded controllers for safety class applications. SCADE Suite is a set of tools that support model based design of software for embedded systems. The model validation activity in SCADE involves model simulation guided by set of test cases that are based on system requirements (Functional or blackbox) and structural coverage criteria like MC/DC (Whitebox). However, systematically devising a test case based on such criterion is not easy and often the designer is required to analyze the model to design a test sequence, which will meet the required criteria. In this paper, we demonstrate the use of a technique based on model checking to automate the generation of such test cases for SCADE models. For automatic test case generation, the tool SAL-ATG was used that can generate the test cases for the models developed in SAL specification language. MCIDC coverage criterion was adopted for generating the test goals to be covered by generated test cases.