An UPPAAL Framework for Model Checking Automotive Systems with FlexRay Protocol

Abstract

This paper introduces a method and a framework for verifying automotive system designs using model checking. The framework is based on UPPAAL, a timed model checker, and focuses on checking automotive system designs with FlexRay communication protocol, a de facto standard of automotive communication protocols. The framework is composed of FlexRay model and application model where the former is built by abstractions to the specifications of FlexRay protocol. In the framework, FlexRay model is reusable for different application models with appropriate parameter settings. To the best of our knowledge, the framework is the first attempt on model checking automotive system designs considering communication protocols. Checking of core properties including timing properties are conducted to evaluate the framework. © Springer International Publishing Switzerland 2014.