Model Checking of OSEK/VDX OS Design Model Based on Environment Modeling

摘要

This paper presents a model-checking experiment for a design model of a practical real-time operating system (RTOS) based on environment modeling. In previous work, we developed a tool called the environment generator to generate environments for model-checking general RTOS models in Spin. This tool takes a general model of the environments, called the environment model, as an input and generates all possible environments within the bounds of the model. Here, we applied the tool to verify the design model of an OSEK/VDX OS, the RTOS for controlling automotive systems. In this paper, we explain the details of constructing the environment models for verifying various aspects of the RTOS. We also show the results of an experiment using our tool.