Formal Analysis of Non-functional Properties for a Cooperative Automotive System

TL;DR

This paper extends formal analysis methods for automotive systems by integrating energy and probabilistic constraints into EAST-ADL, enabling comprehensive verification using SDV and UPPAAL-SMC.

Contribution

It introduces a novel extension of EAST-ADL with energy and probabilistic properties and provides a translation framework for formal verification with SDV and UPPAAL-SMC.

Findings

Successful verification of energy constraints using SDV.

Probabilistic constraints verified with UPPAAL-SMC.

Case study demonstrates effectiveness of the approach.

Abstract

Modeling and analysis of nonfunctional requirements is crucial in automotive systems. EAST-ADL is an architectural language dedicated to safety-critical automotive system design. We have previously modified EAST-ADL to include energy constraints and transformed energy-aware timed (ET) behaviors modeled in SIMULINK/STATEFLOW into UPPAAL models amenable to formal verification. Previous work is extended in this paper by including support for SIMULINK DESIGN VERIFIER (SDV), i.e., the ET constraints are translated into proof objective models that can be verified using SDV. Furthermore, probabilistic extension of EAST-ADL constraints is defined and the semantics of the extended constraints is translated into verifiable UPPAAL models with stochastic semantics for formal verification. A set of mapping rules are proposed to facilitate the guarantee of translation. Verification & Validation are performed on the extended timing and energy constraints using SDV and UPPAAL-SMC. Our approach is demonstrated on a cooperative automotive system case study.