PrCCSL/Simulink Design Verifier中自治系统的形式化描述与分析
Formal Specification & Analysis of Autonomous Systems in PrCCSL/Simulink Design Verifier
摘要：
时序约束的建模和分析在汽车系统中至关重要。EAST-ADL是一种专用于安全关键型汽车嵌入式系统设计的领域特定架构语言。在大多数情况下，系统中有界数量的时间约束违反不会导致系统故障时，违反的结果是可以忽略的，称为弱硬（WH）。我们以前指定的EAST-ADL的时钟约束规约语言（CCSL）的时间约束和转换成正式的模型服从模型检验的CCSL的时间行为。以前的工作扩展在本文中包括支持概率分析的时间约束的背景下WH：概率扩展CCSL，称为PrCCSL，定义和EAST-ADL的时间约束与随机属性指定在PrCCSL。PrCCSL中扩展约束的语义被转换为可以使用SIMULINK DESIGN VERIFIER进行验证的证明目标模型。此外，提出了一组映射规则，以促进翻译的保证。我们的方法被证明在一个自主交通标志识别车辆的案例研究。
英文摘要：
Modeling and analysis of timing constraints is crucial in automotive systems. EAST-ADL is a domain specific architectural language dedicated to safety-critical automotive embedded system design. In most cases, a bounded number of violations of timing constraints in systems would not lead to system failures when the results of the violations are negligible, called Weakly-Hard (WH). We have previously specified EAST-ADL timing constraints in Clock Constraint Specification Language (CCSL) and transformed timed behaviors in CCSL into formal models amenable to model checking. Previous work is extended in this paper by including support for probabilistic analysis of timing constraints in the context of WH: Probabilistic extension of CCSL, called PrCCSL, is defined and the EAST-ADL timing constraints with stochastic properties are specified in PrCCSL. The semantics of the extended constraints in PrCCSL is translated into Proof Objective Models that can be verified using SIMULINK DESIGN VERIFIER. Furthermore, a set of mapping rules is proposed to facilitate guarantee of translation. Our approach is demonstrated on an autonomous traffic sign recognition vehicle case study.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
