Model Checking of OSEK/VDX OS Design Model Based on Environment Modeling
Model Checking of OSEK/VDX OS Design Model Based on Environment Modeling
复制标题
DOI：
10.1007/978-3-642-32943-2_15
复制
发表时间：
2012-09
期刊：
影响因子：
--
通讯作者：
K. Yatake;Toshiaki Aoki
中科院分区：
文献类型：
--
作者：
K. Yatake;Toshiaki Aoki
本文介绍了一个基于环境建模的实时操作系统设计模型的模型检验实验。在以前的工作中，我们开发了一个称为环境生成器的工具，用于在Spin中生成模型检查通用RTOS模型的环境。该工具将环境的一般模型（称为环境模型）作为输入，并在模型范围内生成所有可能的环境。在这里，我们应用该工具来验证OSEK/VDX操作系统，用于控制汽车系统的RTOS的设计模型。在本文中，我们解释了构建环境模型验证RTOS的各个方面的细节。我们还展示了使用我们的工具的实验结果。
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.