TY - GEN
T1 - Modeling and verification of AUTOSAR OS and EMS application
AU - Peng, Yunhui
AU - Huang, Yanhong
AU - Su, Ting
AU - Guo, Jian
PY - 2013
Y1 - 2013
N2 - AUTOSAR, derived from OSEK/VDX, is the most popular industrial standard in the automotive electric development. It is challenging to manually verify or validate the correctness and safety of AUTOSAR Operating System (OS) as well as mission-critical or real-time applications built on it. In this paper, we adopt timed CSP to describe and reason about the Schedule Table, a new task scheduling mechanism in AUTOSAR. We also employ timed CSP to model AUTOSAR OS and a realtime application, i.e., the Engine Management System (EMS), based on the Schedule Table mechanism, and verify some safety properties. In addition, we simulate and verify our models in Process Analysis Toolkit (PAT). The result indicates that both AUTOSAR OS and EMS application conform to the specifications and requirements.
AB - AUTOSAR, derived from OSEK/VDX, is the most popular industrial standard in the automotive electric development. It is challenging to manually verify or validate the correctness and safety of AUTOSAR Operating System (OS) as well as mission-critical or real-time applications built on it. In this paper, we adopt timed CSP to describe and reason about the Schedule Table, a new task scheduling mechanism in AUTOSAR. We also employ timed CSP to model AUTOSAR OS and a realtime application, i.e., the Engine Management System (EMS), based on the Schedule Table mechanism, and verify some safety properties. In addition, we simulate and verify our models in Process Analysis Toolkit (PAT). The result indicates that both AUTOSAR OS and EMS application conform to the specifications and requirements.
UR - https://www.scopus.com/pages/publications/84886396125
U2 - 10.1109/TASE.2013.13
DO - 10.1109/TASE.2013.13
M3 - 会议稿件
AN - SCOPUS:84886396125
SN - 9780768550534
T3 - Proceedings - 2013 International Symposium on Theoretical Aspects of Software Engineering, TASE 2013
SP - 37
EP - 44
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 -