Model Checking Multi-task Software on Real-time Operating Systems

摘要

In this paper, we propose a method to verify software executed on RTOS which conforms to μITRON with a model checking tool Spin. The RTOS provides facilities such as priorities and service calls to control the execution of tasks, however, Spin does not provide them. Thus, we implemented a middleware which allows us to use the facilities and simulate the execution of the tasks in Spin. The paper shows how it is implemented and its evaluation.