Formal Model-Based Test for AUTOSAR Multicore RTOS

AUTOSAR multicore RTOS is a safety-critical concurrent system, for which high quality is required. A conformance test is important to ensure the quality of the software, but the conventional test is low in coverage and high in cost. In this paper, we present a formal model-based test for multicore RTOS that supports AUTOSAR specifications. First, we developed a formal model. With the model, we developed a test case generator, from which an entire test suite can be extracted. Moreover, we proposed a test program generator, with which optimal executable test programs can be generated fully automatically. Both of the generators are assisted with model checking on the formal model. Bug analysis also becomes easy. Our method demonstrated its advantage over conventional testing by finding 33 test cases for three system service calls, whereas a conventional test carried out by a development team found only 10 test cases. Our method can improve the coverage of the test, clearly saving in cost and development time. It is expected to significantly improve the testing of the AUTOSAR multicore RTOS.