Software Assurance for Automotive Control Systems Using Advanced Formal Verification: An Industrial Case Study

Shin'ichi Shiraishi

Senior Research Technology R&D Division, Toyota InfoTechnology Center, USA

In the automotive domain, software and system assurance is a growing concern. In particular, software assurance is now one of the most difficult challenges because of its expanding scale and complexity. In order to tackle this problem, we tried a new software assurance approach based on advanced formal verification. In our approach, we use PVS for high-level requirements and specification and SPARK, a subset of Ada, for low-level specification and implementation.

Based on these advanced formal verification results, we can build software assurance that is difficult to rebut. We conducted a case study on a hypothetical automotive control system and verified its feasibility in the context of a realistic development scenario. This talk provides the overview of our new software assurance approach and results of the case study.

About Shin'ichi Shiraishi

Shin’ichi SHIRAISHI received his B.S., M.S., and Ph.D. degrees in Electronics Engineering from Hokkaido University, Japan, in 1997, 1999, and 2002, respectively. He is currently a Senior Researcher at Toyota InfoTechnology Center, U.S.A. Inc. His research interests include software assurance, software architecture, and modeling languages. He is a member of the IEEE.

Sponsored by

Official Media Partners

Supported by