\input zb-basic
\input zb-ioport
\iteman{io-port 06084983}
\itemau{Yatake, Kenro; Aoki, Toshiaki}
\itemti{Model checking of OSEK/VDX OS design model based on environment modeling.}
\itemso{Roychoudhury, Abhik (ed.) et al., Theoretical aspects of computing -- ICTAC 2012. 9th international colloquium, Bangalore, India, September 24--27, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-32942-5/pbk). Lecture Notes in Computer Science 7521, 183-197 (2012).}
\itemab
Summary: 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.
\itemrv{~}
\itemcc{}
\itemut{}
\itemli{doi:10.1007/978-3-642-32943-2\_15}
\end