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. © 2012 Springer-Verlag.
CITATION STYLE
Yatake, K., & Aoki, T. (2012). Model checking of OSEK/VDX OS design model based on environment modeling. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7521 LNCS, pp. 183–197). https://doi.org/10.1007/978-3-642-32943-2_15
Mendeley helps you to discover research relevant for your work.