Combining Requirement Mining, Software Model Checking, and Simulation-Based Verification for Industrial Automotive Systems

Tomoya Yamaguchi, Tomoyuki Kaga, Alexandre Donzé, and Sanjit A. Seshia. Combining Requirement Mining, Software Model Checking, and Simulation-Based Verification for Industrial Automotive Systems. In Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD), October 2016.
Extended tech report version available here.

Download

[pdf] 

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 presents 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

@InProceedings{yamaguchi-fmcad16,
  Author = {Tomoya Yamaguchi and Tomoyuki Kaga and Alexandre Donz{\'{e}} and Sanjit A. Seshia},
  Title = {Combining Requirement Mining, Software Model Checking, and Simulation-Based Verification for Industrial Automotive Systems},
  booktitle = {Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD)},
  month = "October",
  year = {2016},
  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 presents 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.},
  wwwnote = {Extended tech report version available <a href="https://www.eecs.berkeley.edu/Pubs/TechRpts/2016/EECS-2016-124.html">here</a>.}  
}