Formal Analysis of Non-functional Properties for a Cooperative Automotive System
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.
Cite
@article{arxiv.1803.06075,
title = {Formal Analysis of Non-functional Properties for a Cooperative Automotive System},
author = {Eun-Young Kang and Li Huang and Dongrui Mu},
journal= {arXiv preprint arXiv:1803.06075},
year = {2018}
}
Comments
77 pages, 112 figures, technical report, reference of SAC2018 Conference