A Toolset for Validation and Verification of Automotive Control Software Using Formal Patterns

Yunja CHOI  Dongwoo KIM  

Publication
IEICE TRANSACTIONS on Information and Systems   Vol.E100-D   No.7   pp.1526-1529
Publication Date: 2017/07/01
Online ISSN: 1745-1361
DOI: 10.1587/transinf.2017EDL8042
Type of Manuscript: LETTER
Category: Software System
Keyword: 
validation,  verification,  OSEK/VDX,  patterns,  

Full Text: PDF(399.4KB)>>
Buy this Article




Summary: 
An automotive control system is a typical safety-critical embedded software, which requires extensive verification and validation (V&V) activities. This article introduces a toolset for automated V&V of automotive control system, including a test generator for automotive operating systems, a task simulator for validating task design of control software, and an API-call constraint checker to check emergent properties when composing control software with its underlying operating system. To the best of our knowledge, it is the first integrated toolset that supports V&V activities for both control software and operating systems in the same framework.