A Timing Verification Framework for AUTOSAR OS Component Development based on Real-Time Maude

作者：Zhu, Longfei^*; Liu, Peng; Shi, Jianqi; Wang, Zheng; Zhu, Huibiao

来源：7th International Symposium on Theoretical Aspects of Software Engineering (TASE), United Kingdom, 2013-07-01 to 2013-07-03.

DOI：10.1109/TASE.2013.12

• Automatic verification
• Automotive applications
• Fault propagation
• Open system architecture
• Protection mechanisms
• Timing behaviors
• Timing properties
• Timing verification

The AUTOSAR (AUTomotive Open System ARchilecture) is an open standard in automotive industry, aiming at unifying the methodology of the automotive software development. It is drawing increasing attention because of its great concern about the safety of automotive electronics. The safety of automotive electronics greatly depends on the Operating System (OS) components, which fully implement the functionality part of automotive applications. However, taking the complex timing protection mechanism of AUTOSAR OS and random occurrences of interrupt requests (IRs) into consideration, it is hard for the developers to design and configure the OS components correctly or even reconcilably. In this paper, we focus on the timing properties and propose an automatic verification framework, in which developers could analyze the timing behaviors and devise the OS components configuration. Furthermore, three important timing properties are expressed and can be verified in our framework, namely, schedulability, non-fault-propagation, and consistency. As a reduced version of AUTOSAR OS and auxiliary analysis modules have been implemented based on Real-Time Maude, developers could easily employ the tool to experiment with different configurations of OS components.

• 出版日期2013
• 单位北京控制工程研究所; 华东师范大学