Automated Verification of AADL-Specifications Using UPPAAL
Automated Verification of AADL-Specifications Using UPPAAL
复制标题
DOI：
10.1109/hase.2012.22
复制
发表时间：
2012-10
期刊：
影响因子：
--
通讯作者：
Andreas Johnsen;K. Lundqvist;P. Pettersson;Omar Jaradat
中科院分区：
文献类型：
--
作者：
Andreas Johnsen;K. Lundqvist;P. Pettersson;Omar Jaradat
体系结构分析和设计语言（AADL）用于表示安全至关重要和实时嵌入式系统的架构设计决策。由于这些决策对开发过程的影响深远，因此在整个过程中，建筑设计故障可能会产生重大恶化的影响。因此，自动化的故障避免建筑设计决策，有可能在提高最终产品的可靠性的同时，显着降低开发成本。为了在开发AADL中指定的系统时提供自动故障避免的手段，已经开发了一种形式的验证技术，以确保AADL规范的完整性和一致性及其与最终产品的符合性。该方法要求AADL的语义被形式化和实施。我们使用语义锚定的方法来通过一组定时自动机构建体的一组转换规则来用AADL子集的正式和实现的语义做出贡献。此外，使用主要汽车制造商开发的安全至关重要的燃油级系统的案例研究，将验证技术（包括转换规则）进行验证。
The Architecture Analysis and Design Language (AADL) is used to represent architecture design decisions of safety-critical and real-time embedded systems. Due to the far-reaching effects these decisions have on the development process, an architecture design fault is likely to have a significant deteriorating impact through the complete process. Automated fault avoidance of architecture design decisions therefore has the potential to significantly reduce the cost of the development while increasing the dependability of the end product. To provide means for automated fault avoidance when developing systems specified in AADL, a formal verification technique has been developed to ensure completeness and consistency of an AADL specification as well as its conformity with the end product. The approach requires the semantics of AADL to be formalized and implemented. We use the methodology of semantic anchoring to contribute with a formal and implemented semantics of a subset of AADL through a set of transformation rules to timed automata constructs. In addition, the verification technique, including the transformation rules, is validated using a case study of a safety-critical fuel-level system developed by a major vehicle manufacturer.