协作式汽车系统非功能性质的形式化分析
软件工程
2018-03-20 v2
摘要
在汽车系统中，对非功能需求进行建模和分析至关重要。EAST-ADL 是一种专用于安全关键汽车系统设计的架构语言。我们此前已修改 EAST-ADL 以包含能量约束，并将 SIMULINK/STATEFLOW 中建模的能量感知定时（ET）行为转换为适用于形式化验证的 UPPAAL 模型。本文扩展了先前的工作，加入了对 SIMULINK DESIGN VERIFIER (SDV) 的支持，即将 ET 约束转换为可使用 SDV 验证的证明目标模型。此外，定义了 EAST-ADL 约束的概率扩展，并将扩展约束的语义转换为具有随机语义的可验证 UPPAAL 模型以进行形式化验证。提出了一组映射规则以促进转换的保证。使用 SDV 和 UPPAAL-SMC 对扩展的定时和能量约束进行了验证与确认。我们的方法在一个协作式汽车系统案例研究中得到了演示。
引用
@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}
}
备注
77 pages, 112 figures, technical report, reference of SAC2018 Conference