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.

翻译：虽然车辆在过去主要通过机械方式进行控制，但随着电子控制技术和性能的进步，越来越多的嵌入式控制系统被安装和使用。汽车系统由多个供应商开发的多种组件构成。为加速嵌入式控制系统的发展，汽车系统领域正在制定诸如AUTOSAR等工业标准，包括操作系统和中间件技术的设计。作为确保汽车系统安全的关键，操作系统是众多汽车应用执行的基础软件。本文提出了一种集成化模型驱动方法用于验证汽车操作系统，该方法称为模型检验在环模型驱动测试（MCIL-MBT）。在MCIL-MBT中，我们创建了一个形式化汽车操作系统规约的模型，并通过模型检验验证这些规约。随后，利用经过验证的模型进行模型驱动测试，以确保特定操作系统的实现符合该模型。验证和测试阶段会迭代进行，直至未检测到任何缺陷。该方法已被引入一家汽车系统供应商和一家操作系统供应商。通过我们的方法，我们成功识别了传统审查和测试方法未能发现的缺陷。