摘要
安全关键软件是指应用于航空、航天、核能、武器装备等领域且对软件安全性和正确性有着极高要求的一类软件。随着安全关键软件的规模和复杂性不断增加，安全关键软件越来越多地采用异构构件组合架构，使得整个软件系统呈现异构性。异构软件系统的执行与交互语义也从完全同步发展到全局异步-局部同步(GloballyAsynchronousLocallySynchronous,GALS)方式，即不同构件具有各自的时钟控制(称为多时钟)，构件之间采用异步通信方式。具有多时钟、异步通信等特征的异构软件设计与验证是航空航天工业界面临的巨大挑战。模型驱动开发方法已成为保证安全关键软件正确性和安全性的重要手段，而复杂嵌入式系统的体系结构与分析语言AADL(ArchitectureAnalysisandDesignLanguage)作为一种面向安全关键异构系统的多范式建模语言，广泛应用于安全关键软件的软/硬件结构、运行时环境、功能和非功能属性的建模。 本文提出了一种面向安全关键异构软件的AADL组合设计与验证方法，支持AADL及行为附件BehaviorAnnex、同步语言SIGNAL、异步建模语言SDL和Ada的多范式建模及异构模型的组合验证和代码自动生成，并设计和实现了AADL组合设计、验证与代码生成原型工具。主要研究成果如下： 首先，提出了基于AADL多范式建模的组合设计方法，重点解决了异构模型之间的数据和语义的互联互通，给出了AADL-ASN.1属性集扩展，以支持AADL异构模型的通信数据建模；提出了AADL异构模型容器(AADLHeterogeneousModelContainer,AADL-HMC)以支持AADL模型语义与异构建模语言语义互通；并基于AADL-HMC语义给出了AADL-HMC属性集扩展，支持AADL异构建模。 其次，针对AADL组合验证工具AGREE目前主要支持AADL同步子集的问题，提出了支持多时钟、异步通信等特征的AADL异构模型组合验证方法X-AGREE，主要包括基于模态自动机的方式给出队列通信、线程调度等AADL异步子集的语义，AADL异步子集到Lustre模型的转换，以及基于模型检测工具JKind的Lustre模型验证。 然后，提出了AADL异构模型的代码自动生成方法，以Ada为例，给出了AADL架构模型到Ada代码框架的生成、ASN.1数据模型到Ada数据结构的生成和异构行为模型到Ada功能行为代码的生成，并通过AADL-HMC生成Ada运行时代码，以支持基于AADL-HMC语义对Ada异构功能行为代码进行调度与集成。 最后，基于AADL开源建模环境OSATE和组合验证环境AGREE设计并实现了AADL多范式建模工具AADL-MPM、AADL异构模型组合验证工具X-AGREE及Ada代码生成工具AADL-MPM2Ada，并通过工业界实际案例卫星姿轨控系统分析了本文所提方法的有效性。
NETL