Paper Info
Title
Model checking of OSEK/VDX OS design model based on environment modeling
Abstract
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.
Year
DOI
Venue
2012
10.1007/978-3-642-32943-2_15
ICTAC
Keywords
Field
DocType
general model,design model,possible environment,model checking,environment generator,vdx os,environment modeling,environment model,automotive system,model-checking experiment,vdx os design model,general rtos model
Model checking,Computer science,Object graph,OSEK,Real-time operating system,Automotive systems,Object Constraint Language,Embedded system
Conference
Citations 
PageRank 
References 
5
0.49
12
Authors
2
Name
Order
Citations
PageRank
Kenro Yatake1234.59
Toshiaki Aoki25716.68