摘要：架构分析与设计语言(AADL)是一种用于描述复杂嵌入式系统体系架构的建模语言,被广泛用于安全关键系统建模与验证。AADL通过行为附件以状态机的形式对组件的内部行为建模。工业界中的复杂系统常使用层次自动机描述组件的功能行为,而行为附件中没有表达层次自动机的机制。针对这一问题,提出了AADL行为附件的层次化扩展——HBA。首先给出了HBA的形式语法,然后定义了HBA的操作语义。提出了HBA的元模型,并在OSATE环境中实现其文本和图形化编辑器。为了便于形式化验证,给出了HBA到时间自动机(TA)的转换规则,并基于模型检测工具UPPAAL进行形式化验证。最后,给出一个案例研究来验证所提方法的有效性。

摘要：随着嵌入式软件系统在汽车、核工业、航空、航天等安全关键领域的广泛应用,其失效将会导致财产的损失、环境的破坏甚至人员的伤亡,使得保障软件安全性成为系统开发过程中的重要部分.传统的安全性分析方法主要应用在软件的需求分析阶段和设计阶段,然而需求与设计之间的鸿沟却一直是软件工程领域的一大难题.正是由于这一鸿沟的存在,使得需求分析阶段的安全性分析结果难以完整而详尽地反映在软件设计中.其根本原因是:当前的软件需求主要通过自然语言描述,存在二义性与模糊性,且难以进行自动化处理.为了解决这一问题,面向构件化嵌入式软件,首先提出了一种半结构化的限定自然语言需求模板用于需求规约,能够有效地降低自然语言需求的二义性与模糊性;然后,为了降低自动化处理的复杂性,采用需求抽象语法图作为中间模型,实现基于限定自然语言需求模板规约的软件需求与AADL模型之间的转换,并在此过程中自动记录两者之间的可追踪关系;最后,基于AADL开源工具OSATE对所提出方法进行了插件实现,并通过航天器导航、制导与控制系统(guidance,navigation and control,简称GNC)进行了实例性验证.

摘要：在航空、航天、交通、能源等安全关键领域中,软件的失效可能导致系统处于危险状态,从而导致财产损失、环境破坏甚至人员伤亡,如何保障这类软件的可靠性和安全性一直是学术界和工业界共同面临的难题.近年来,形式化模型驱动的安全关键软件设计与验证方法逐渐受到重视,并被认为是切实可行的重要手段.然而,形式化模型驱动开发方法的生命周期一般较少涉及需求阶段,主要原因是当前工业界的软件需求主要通过自然语言文本描述.而安全关键软件引起严重事故的问题链的最上端原因往往又是软件需求尤其是安全性需求的问题. AADL(Architecture Analysis&Design Language)是一种广泛应用于安全关键软件领域的建模语言标准.本文针对自然语言需求和AADL模型驱动开发方法之间还存在鸿沟的问题,研究基于限定自然语言的安全关键软件需求建模及AADL模型自动生成方法.首先,提出一种基于限定自然语言的需求规约方法,通过结构化的需求组织方式及受限的自然语言以减少需求表达中存在的二义性.其次,给出限定自然语言需求到AADL模型的自动转换方法.此外,本文给出一种结构化的验证性质描述模板,并自动转换到AADL组合验证附件AGREE(Assume Guarantee REasoning Environment) Annex,从而支持对AADL模型进行形式化验证.最后,在AADL开源工具环境OSATE中实现了原型工具,并基于航天导航制导控制子系统进行案例分析.