TY - GEN
T1 - A timing verification framework for AUTOSAR OS component development based on Real-Time Maude
AU - Zhu, Longfei
AU - Liu, Peng
AU - Shi, Jianqi
AU - Wang, Zheng
AU - Zhu, Huibiao
PY - 2013
Y1 - 2013
N2 - The AUTOSAR (AUTomotive Open System ARchitecture) 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.
AB - The AUTOSAR (AUTomotive Open System ARchitecture) 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.
UR - https://www.scopus.com/pages/publications/84886399621
U2 - 10.1109/TASE.2013.12
DO - 10.1109/TASE.2013.12
M3 - 会议稿件
AN - SCOPUS:84886399621
SN - 9780768550534
T3 - Proceedings - 2013 International Symposium on Theoretical Aspects of Software Engineering, TASE 2013
SP - 29
EP - 36
BT - Proceedings - 2013 International Symposium on Theoretical Aspects of Software Engineering, TASE 2013
T2 - 2013 International Symposium on Theoretical Aspects of Software Engineering, TASE 2013
Y2 - 1 July 2013 through 3 July 2013
ER -