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

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

    Research output: Chapter in Book/Report/Conference proceedingChapter

    Abstract

    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.

    Original languageEnglish
    Title of host publicationCyber-Physical System Design from an Architecture Analysis Viewpoint
    Subtitle of host publicationCommunications of NII Shonan Meetings
    PublisherSpringer Singapore
    Pages109-132
    Number of pages24
    ISBN (Electronic)9789811044366
    ISBN (Print)9789811044359
    DOIs
    Publication statusPublished - 2017 May 10

    Fingerprint

    Model checking
    Formal methods
    Testing
    NASA
    Railroad cars

    Keywords

    • Automotive systems
    • Model checking
    • Operating systems
    • Testing

    ASJC Scopus subject areas

    • Computer Science(all)
    • Engineering(all)

    Cite this

    Aoki, T., Satoh, M., Tani, M., Yatake, K., & Kishi, T. (2017). Combined model checking and testing create confidence-a case on commercial automotive operating system. In Cyber-Physical System Design from an Architecture Analysis Viewpoint: Communications of NII Shonan Meetings (pp. 109-132). Springer Singapore. https://doi.org/10.1007/978-981-10-4436-6_5

    Combined model checking and testing create confidence-a case on commercial automotive operating system. / Aoki, Toshiaki; Satoh, Makoto; Tani, Mitsuhiro; Yatake, Kenro; Kishi, Tomoji.

    Cyber-Physical System Design from an Architecture Analysis Viewpoint: Communications of NII Shonan Meetings. Springer Singapore, 2017. p. 109-132.

    Research output: Chapter in Book/Report/Conference proceedingChapter

    Aoki, T, Satoh, M, Tani, M, Yatake, K & Kishi, T 2017, Combined model checking and testing create confidence-a case on commercial automotive operating system. in Cyber-Physical System Design from an Architecture Analysis Viewpoint: Communications of NII Shonan Meetings. Springer Singapore, pp. 109-132. https://doi.org/10.1007/978-981-10-4436-6_5
    Aoki T, Satoh M, Tani M, Yatake K, Kishi T. Combined model checking and testing create confidence-a case on commercial automotive operating system. In Cyber-Physical System Design from an Architecture Analysis Viewpoint: Communications of NII Shonan Meetings. Springer Singapore. 2017. p. 109-132 https://doi.org/10.1007/978-981-10-4436-6_5
    Aoki, Toshiaki ; Satoh, Makoto ; Tani, Mitsuhiro ; Yatake, Kenro ; Kishi, Tomoji. / Combined model checking and testing create confidence-a case on commercial automotive operating system. Cyber-Physical System Design from an Architecture Analysis Viewpoint: Communications of NII Shonan Meetings. Springer Singapore, 2017. pp. 109-132
    @inbook{522fbe9f588b4e4f96d24e1e8daba21e,
    title = "Combined model checking and testing create confidence-a case on commercial automotive operating system",
    abstract = "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.",
    keywords = "Automotive systems, Model checking, Operating systems, Testing",
    author = "Toshiaki Aoki and Makoto Satoh and Mitsuhiro Tani and Kenro Yatake and Tomoji Kishi",
    year = "2017",
    month = "5",
    day = "10",
    doi = "10.1007/978-981-10-4436-6_5",
    language = "English",
    isbn = "9789811044359",
    pages = "109--132",
    booktitle = "Cyber-Physical System Design from an Architecture Analysis Viewpoint",
    publisher = "Springer Singapore",

    }

    TY - CHAP

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

    AU - Aoki, Toshiaki

    AU - Satoh, Makoto

    AU - Tani, Mitsuhiro

    AU - Yatake, Kenro

    AU - Kishi, Tomoji

    PY - 2017/5/10

    Y1 - 2017/5/10

    N2 - 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.

    AB - 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.

    KW - Automotive systems

    KW - Model checking

    KW - Operating systems

    KW - Testing

    UR - http://www.scopus.com/inward/record.url?scp=85033354084&partnerID=8YFLogxK

    UR - http://www.scopus.com/inward/citedby.url?scp=85033354084&partnerID=8YFLogxK

    U2 - 10.1007/978-981-10-4436-6_5

    DO - 10.1007/978-981-10-4436-6_5

    M3 - Chapter

    AN - SCOPUS:85033354084

    SN - 9789811044359

    SP - 109

    EP - 132

    BT - Cyber-Physical System Design from an Architecture Analysis Viewpoint

    PB - Springer Singapore

    ER -