Application of Model Checking to Automotive Control Software with Slicing Technique

Masahiro Matsubara; Kohei Sakurai; Fumio Narisawa; Masushi Enshoiwa; Yoshio Yamane; Hisamitsu Yamanaka

doi:10.4271/2013-01-0436

To detect difficult-to-find defects in automotive control systems, we have proposed a modeling method with a program slicing technique. In this method, a verifier adjusts the boundaries of source code to be extracted on a variable dependence graph, in a kind of data flow. We have developed software tools for this method and achieved a 35% decrease in total verification time on model checking.

This paper provides some consideration on effective cases of the method from verification practices. There are two types of malfunction causes: one is the timing of processes (race conditions), and the other is complex logics. Each type requires different elements in external environment models. Furthermore, we propose regression verification based on the modeling method above, to further reduce verification time on model checking. The paper outlines tool extensions needed to realize regression verification.

Standards

SAE Mobilus®

Publications

News

Events

Professional Development

A World in Motion (PreK-12)

Participate with SAE

SAE Membership

Donate

Application of Model Checking to Automotive Control Software with Slicing Technique 2013-01-0436

SAE MOBILUS