摘要：提出了一种基于时间抽象状态机(timed abstract state machine,简称TASM)的AADL(architecture analysis and design language)模型验证方法.分别给出了AADL子集和TASM的抽象语法,并基于语义函数和类ML的元语言形式定义转换规则.在此基础上,基于AADL开源建模环境OSATE(open source AADL tool environment)设计并实现了AADL模型验证与分析工具AADL2TASM,并基于航天器导航、制导与控制系统(guidance,navigation and control)进行了实例性验证.

摘要：能够提供更强计算能力的多核处理器将在安全关键系统中得到广泛应用,但是由于现代处理器所使用的流水线、乱序执行、动态分支预测、Cache等性能提高机制以及多核之间的资源共享,使得系统的最坏执行时间分析变得非常困难.为此,国际学术界提出时间可预测系统设计的思想,以降低系统的最坏执行时间分析难度.已有研究主要关注硬件层次及其编译方法的调整和优化,而较少关注软件层次,即,时间可预测多线程代码的构造方法以及到多核硬件平台的映射.提出一种基于同步语言模型驱动的时间可预测多线程代码生成方法,并对代码生成器的语义保持进行证明;提出一种基于AADL(architecture analysis and design language)的时间可预测多核体系结构模型,作为研究的目标平台;最后,给出多线程代码到多核体系结构模型的映射方法,并给出系统性质的分析框架.

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