  While vehicles have primarily been controlled through mechanical means in
years past, an increasing number of embedded control systems are being
installed and used, keeping pace with advances in electronic control technology
and performance. Automotive systems consist of multiple components developed by
a range of vendors. To accelerate developments in embedded control systems,
industrial standards such as AUTOSAR are being defined for automotive systems,
including the design of operating system and middleware technologies. Crucial
to ensuring the safety of automotive systems, the operating system is
foundational software on which many automotive applications are executed. In
this paper, we propose an integrated model-based method for verifying
automotive operating systems; our method is called Model-Checking in the Loop
Model-Based Testing (MCIL-MBT). In MCIL-MBT, we create a model that formalizes
specifications of automotive operating systems and verifies the specifications
via model-checking. Next, we conduct model-based testing with the verified
model to ensure that a specific operating system implementation conforms to the
model. These verification and testing stages are iterated over until no flaws
are detected. Our method has already been introduced to an automotive system
supplier and an operating system vendor. Through our approach, we successfully
identified flaws that were not detected by conventional review and testing
methods.
