Combined Model Checking and Testing Create Confidence in Correctness of Commercial Automotive Operating System

Material type: 文書・図像類

Author: Aoki, Toshiakiほか

Publisher: 北陸先端科学技術大学院大学先端科学技術研究科情報科学系

Publication date: 2016-05-23

Material Format: Digital

Capacity, size, etc.: -

NDC: -

View All

Notes on use

Note (General)：: The safety and reliability of automotive systems are becoming a big concern in our daily life. Recently, a functional safety standard which specialize...

Search by Bookstore

Holdings of Libraries in Japan

This page shows libraries in Japan other than the National Diet Library that hold the material.

List of Cooperating Institutions and Databases

Please contact your local library for information on how to use materials or whether it is possible to request materials from the holding libraries.

other

JAIST Repository
Digital
You can check the holdings of institutions and databases with which 学術機関リポジトリデータベース（IRDB）（機関リポジトリ） is linked at the site of 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）.
JAIST Repository

Search by Bookstore

Bibliographic Record

You can check the details of this material, its authority (keywords that refer to materials on the same subject, author's name, etc.), etc.

Digital

Material Type: 文書・図像類
Title: Combined Model Checking and Testing Create Confidence in Correctness of Commercial Automotive Operating System
Author/Editor: Aoki, Toshiaki
Satoh, Makoto
Tani, Mitsuhiro
Yatake, Kenro
Kishi, Tomoji
Author Heading: Aoki, Toshiaki
Satoh, Makoto
Tani, Mitsuhiro
Yatake, Kenro
Kishi, Tomoji
Publication, Distribution, etc.: 北陸先端科学技術大学院大学先端科学技術研究科情報科学系
Publication Date: 2016-05-23
Publication Date (W3CDTF): 2016-05-23
Periodical title: Research report (School of Information Science, Graduate School of Advanced Science and Technology, Japan Advanced Institute of Science and Technology)
No. or year of volume/issue: IS-RR-2016-002
Volume: IS-RR-2016-002
Pages: 1-11
ISSN (Periodical Title): ISSN : 0918-7553
Text Language Code: eng
Subject Heading: automotive operating systems
model checking
testing
design verification
test case generation
Target Audience: 一般
Note (General): 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 paper 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 it. As a result, we acquired the confidence that the quality of the operating system is very high.
リサーチレポート（北陸先端科学技術大学院大学先端科学技術研究科情報科学系）
identifier:https://dspace.jaist.ac.jp/dspace/handle/10119/13505
Format (IMT): application/pdf
Source: https://dspace.jaist.ac.jp/dspace/bitstream/10119/13505/1/IS-RR-2016-002.pdf
https://dspace.jaist.ac.jp/dspace/bitstream/10119/13505/1/IS-RR-2016-002.pdf
Access Restrictions: 限定公開
Data Provider (Database): 国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）
https://irdb.nii.ac.jp
Original Data Provider (Database): 北陸先端科学技術大学院大学 : JAIST学術研究成果リポジトリ