摘要：同步语言具有确定性并行和精确时间语义等特性,因此被广泛用于设计和验证安全关键软件.随着安全关键领域应用多核处理器逐渐成为趋势,同步语言的多线程代码生成及其语义保持证明研究成为研究热点.目前,已有同步语言代码生成方法还较少考虑多线程代码生成的语义保持证明.因此,本文提出一种同步语言SIGNAL多线程代码生成的语义保持证明方法:首先形式化定义编译过程中源、目标、中间语言的结构化操作语义;其次形式化定义多线程代码生成过程;最后基于互模拟等价思想证明编译前后的语义一致性.

摘要：随着系统复杂性的急剧增加,未来安全关键软件越来越多地采用异构构件组合架构,各种构件可能使用不同的计算模型或实现语言,使得整个软件系统呈现异构性.因此,设计此类系统需要使用复杂的建模方法.AADL(architecture analysis and design language)是一种安全关键系统体系结构多范式建模语言,丰富的可表达方式和可扩展性使其成为安全关键异构软件设计的重要选择.提出一种AADL和SDL(specification and description language)混合建模方法,支持以自底向上的方式对安全关键软件系统进行混合建模,并给出面向多核处理器平台的代码自动生成方法.首先,通过扩展AADL属性集,以支持使用SDL建模语言表达软件构件的功能行为.其次,以Ada作为目标语言,给出AADL-SDL混合模型的多任务代码生成方法.最后,实现了原型工具支持AADL和SDL混合建模及多任务Ada代码生成,并基于导航、制导与控制系统案例对所提方法的有效性进行分析.