Tomoya Yamaguchi and Tomoyuki Kaga and Alexandre Donze and Sanjit A. Seshia

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2016-124

June 30, 2016

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2016/EECS-2016-124.pdf

The verification and validation of industrial closed-loop automotive systems still remains a major challenge. The overall goal is to verify properties of the closed-loop combination of control software and physical plant. While current software model-checking techniques can be applied on a software component of the system, the end result is not very useful unless the interactions with the physical plant and other software components are captured. To this end, we present an industrial case study in which we combine requirement mining, software model-checking, and simulation-based verification to find issues in industrial automotive systems. Our methodology combines the the scalability of simulation-based verification of hybrid systems with the effectiveness of software model-checking at the unit level. We present two case studies: one on a publicly available Abstract Fuel Control System benchmark and another on an actual production SiLS (Software in the Loop Simulator) benchmark. Together these case studies demonstrate the practicality of the proposed methodology.

---

BibTeX citation:

@techreport{Yamaguchi:EECS-2016-124,
    Author= {Yamaguchi, Tomoya and Kaga, Tomoyuki and Donze, Alexandre and Seshia, Sanjit A.},
    Title= {Combining Requirement Mining, Software Model Checking, and Simulation-Based Verification for Industrial Automotive Systems},
    Year= {2016},
    Month= {Jun},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2016/EECS-2016-124.html},
    Number= {UCB/EECS-2016-124},
    Abstract= {  The verification and validation of industrial closed-loop automotive systems still remains a major
  challenge.  The overall goal is to verify properties of the closed-loop combination of control
  software and physical plant.  While current software model-checking techniques can be applied on a
  software component of the system, the end result is not very useful unless the interactions with
  the physical plant and other software components are captured.  To this end, we present an
  industrial case study in which we combine requirement mining, software model-checking, and
  simulation-based verification to find issues in industrial automotive systems.  Our methodology
  combines the the scalability of simulation-based verification of hybrid systems with the
  effectiveness of software model-checking at the unit level.  We present two case studies: one on
  a publicly available Abstract Fuel Control System benchmark and another on an actual production
  SiLS (Software in the Loop Simulator) benchmark.  Together these case studies demonstrate the
  practicality of the proposed methodology.},
}

EndNote citation:

%0 Report
%A Yamaguchi, Tomoya 
%A Kaga, Tomoyuki 
%A Donze, Alexandre 
%A Seshia, Sanjit A. 
%T Combining Requirement Mining, Software Model Checking, and Simulation-Based Verification for Industrial Automotive Systems
%I EECS Department, University of California, Berkeley
%D 2016
%8 June 30
%@ UCB/EECS-2016-124
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2016/EECS-2016-124.html
%F Yamaguchi:EECS-2016-124