Combined model checking and testing create confidence-a case on commercial automotive operating system

Toshiaki Aoki, Makoto Satoh, Mitsuhiro Tani, Kenro Yatake, Tomoji Kishi

研究成果: Chapter

抄録

The safety and reliability of automotive systems are becoming a big concern in our daily life. Recently, a functional safety standard which specializes in automotive systems has been proposed by the ISO. In addition, electrical throttle systems have been inspected by NHTSA and NASA due to the unintended acceleration problems of Toyota's cars. In light of such recent circumstances, we are researching practical applications of formal methods to ensure the high quality of automotive operating systems. An operating system which we focus on is the one conforming to the OSEK/VDX standard. This chapter shows a case study where model checking is applied to a commercial automotive operating system. In this case study, the model checking is combined with testing in order to efficiently and effectively verify the operating system. As a result, we gained the confidence that the quality of the operating system is very high.

本文言語English
ホスト出版物のタイトルCyber-Physical System Design from an Architecture Analysis Viewpoint
ホスト出版物のサブタイトルCommunications of NII Shonan Meetings
出版社Springer Singapore
ページ109-132
ページ数24
ISBN(電子版)9789811044366
ISBN(印刷版)9789811044359
DOI
出版ステータスPublished - 2017 5 10

ASJC Scopus subject areas

  • Computer Science(all)
  • Engineering(all)

フィンガープリント 「Combined model checking and testing create confidence-a case on commercial automotive operating system」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル