AADL功能行为扩展：HBA在嵌入式系统架构中的层次建模与验证

架构分析与设计语言(Architecture Analysis and Design Language, AADL) 是一种专门设计用来描述复杂嵌入式系统体系结构的高级建模工具。它在安全关键系统的设计与验证过程中发挥着重要作用，因为它能够以清晰、结构化的方式刻画系统组件的行为和交互。AADL的核心特性是通过行为附件的形式，采用状态机模型来表达组件的内部行为，这有助于理解和控制系统的动态特性。 然而，在实际工业界应用中，特别是在处理复杂系统时，如层级结构丰富的系统，AADL的行为附件可能无法充分捕捉和表达这种层次性。原有的行为附件设计可能不支持直接表示层次自动机，这在处理组件功能行为的组织和层次关系时存在局限。为了解决这个问题，研究人员提出了AADL行为附件的层次化扩展(Hierarchical Behavior Attachment, HBA)。 HBA的主要贡献包括：首先，定义了一个形式化的语法，明确了行为附件的新规则和结构，以便在保留AADL原有优点的基础上，增加对层次结构的支持。其次，定义了HBA的操作语义，即行为附件如何与AADL体系结构模型协同工作，以体现层次关系和组件间的依赖关系。 为了便于形式化验证和模型分析，研究者还开发了一套将HBA转换为时间自动机(Timing Automata, TA)的规则，使得HBA模型可以导入到模型检测工具UPPAAL等工具中，进行精确的静态和动态分析。这一步骤对于确保系统的正确性和性能至关重要，尤其是在安全性要求极高的嵌入式系统中。 最后，通过一个实际案例研究，研究者验证了HBA的有效性和实用性。案例中的系统展示了如何使用HBA进行设计，以及如何通过形式化验证确保其满足预期的行为和性能要求。这个案例进一步证明了HBA作为AADL扩展的价值，能够更好地支持工业界复杂嵌入式系统的建模与验证。 本文的研究成果为AADL在处理复杂嵌入式系统设计时提供了更强大的工具，特别是在处理层次结构方面，提升了模型的精确性和可验证性，对于提升系统设计的质量和安全性具有重要意义。此外，论文还展示了跨学科的合作，结合国家自然科学基金、国家重点研发计划、国防基础科研项目等多方面的资助，体现了国内在高级系统架构语言研究领域的持续投入和进展。