随着功能需求的不断增加,安全关键系统的设计变得越来越复杂。如何通过建模与验证的方法保证安全关键系统的质量,一直以来都是形式化方法领域备受关注的问题。AADL作为一种应用广泛的建模语言,在安全关键系统的设计与实现中发挥着重要的作用。它提供了丰富的组件用来描述系统的体系结构,并且能够支持性能关键属性的早期预测和重复性分析。然而,AADL描述系统行为的方式主要是基于自动机理论,在建模和验证大型复杂系统时难免会遇到状态空间爆炸问题。此外,由于缺乏描述行为细节的手段,AADL难以支持功能需求的分析与验证,从而无法保证整个系统的正确性和安全性。针对AADL语言在行为描述以及模型验证上的不足,本文提出了一种基于约束求解的精化行为建模方法。该方法扩展了AADL语言以增强其描述行为细节的能力,并且能够支持Z3求解器对构建的精化行为模型进行分析与验证,从而在一定程度上缓解状态空间爆炸的情形。本文的主要贡献如下:(1)基于AADL语言的扩展机制,提出了一个能够支持精化行为建模的附属语言RBML,并给出它的语法和语义。该语言创新性地引入了自定义机制,用来提升行为建模时的灵活性。它允许用户根据需要在RBML规范中定义变量、方法和约束,以描述AADL核心语言所不能表达的数据、行为和需求。(2)定义了RBML语言到Z3求解器的转换规则并设计了主要的转换算法。本文选择了Z3求解器作为验证工具,可以在提升验证效率的同时有效地缓解状态空间爆炸的问题。本文还使用了OpenModelica工具对RBML规范中的连续行为进行仿真,来增强验证结果的可靠性。(3)设计并实现了一个工具链,用于支持RBML语言的建模、验证和仿真。本文实现了RBML语言在OSATE平台上的集成,允许用户在AADL模型中插入RBML附属规范以支持精化行为建模。此外,本文还开发了一个模型转换工具AADL2ZAO,用于将AADL模型自动转换为对应的形式化规范。该工具还与Z3和OpenModelica建立了连接,以便对转换生成的规范进行验证和仿真。本文以百度Apollo自动驾驶系统为例,说明了RBML语言在安全关键系统的行为建模与分析中的具体应用。实验结果表明,本文提出的方法能够有效地建模和分析行为的实现细节,从而保证功能设计的正确性以及整个系统的安全性。