Application of Model Checking to Automotive Control Software with Slicing Technique

Paper #:
  • 2013-01-0436

Published:
  • 2013-04-08
DOI:
  • 10.4271/2013-01-0436
Citation:
Matsubara, M., Sakurai, K., Narisawa, F., Enshoiwa, M. et al., "Application of Model Checking to Automotive Control Software with Slicing Technique," SAE Technical Paper 2013-01-0436, 2013, https://doi.org/10.4271/2013-01-0436.
Pages:
7
Abstract:
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.
Access
Now
SAE MOBILUS Subscriber? You may already have access.
Buy
Select
Price
List
Download
$27.00
Mail
$27.00
Members save up to 40% off list price.
Share
HTML for Linking to Page
Page URL

Related Items

Training / Education
2018-02-05
Article
2016-11-15
Technical Paper / Journal Article
2010-09-28
Training / Education
2018-07-16
Video
2017-03-26
Book
2014-01-01