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.