基于过程与场景分析的航天应用软件测试方法

航天应用软件系统具有软件种类多、规模大、信息交换关系复杂等特点，如何开展软件测试是工程实践中的一个难题。结合某测控信息应用软件系统实例，提出了一种基于形式化模型的软件系统测试方法。基于软件系统形式化定义和线索分析技术，绘制软件系统运行流程图、阶段分析图，建立可表述软件系统级行为的场景树模型和场景树图；根据测试充分性要求，提出基于场景树图的路径覆盖准则，给出满足路径覆盖准则的测试用例集自动化生成算法；结合工程实例，给出了方法应用数据，开展测试结果分析。验证结果表明该测试方法是可行的和有效的，能够保障软件测试的充分性。     

核电安全级仪控系统形式化功能验证

提出了一种基于形式化技术的功能验证方法,对可编程逻辑模块级/子系统级进行功能验证。通过实例逻辑验证表明,依据功能验证平台,按照验证步骤对设计程序进行缺陷检查,测试用例能保证RTL代码结构和功能覆盖达到100%,并提供验证报告方便快速定位并进行缺陷修复,大大地降低了仪控系统在核电厂实际使用过程中出现问题的概率,保证核电安全级仪控系统稳定性、可靠性和安全性的要求,为仪控系统提供更充分更有力的依据。     

SCVerify:抗功耗侧信道攻击软件实现的验证

功耗侧信道攻击,通过使用统计分析技术推断出加密算法中的密钥,已成为物理网络设备的一个巨大威胁.随机掩码是一种被广泛使用的用来消除密钥数据和侧信道泄露数据之间关联性的对策.尽管现有技术可以验证加密软件代码是否被随机掩码保护,但是它们在准确性和可扩展性方面受到限制.为消除此类限制,提出了一种基于原有技术改进过的验证随机掩码策略的方法,该方法比已有的基于句法类型的推断技术更准确,比使用SAT(SMT)模型计数的方法更具有可扩展性.实际上,该方法使用一系列语义类型推导规则去推导分布类型,这些规则最初保持抽象以允许快速推导,然后具体化那些抽象规则推导解决不了的验证问题.此类细化方法集成在验证工具SCVerify中,并使用包含AES和MAC-Keccak等加密算法的测试用例进行了验证,实验结果表明此方法在准确性和可扩展性方面明显优于当前的技术.     

基于可拓理论的装备知识形式化描述模型研究

通过分析现有装备知识描述方法的特点,提出了构建装备知识形式化描述模型的需求;概括和归纳了可拓理论的内容及国内外研究现状,结合基元原理和拓展分析原理构建了5种装备知识形式化描述模型;为了说明装备知识形式化描述模型的可行性和有效性,以部分装备知识为例进行实例验证;装备知识形式化描述是进行装备参数聚合及装备体系评估的前提和基础。     

用于通信网络协议开发的形式化方法

随着形式化方法和技术日趋完善，网络协议开发也逐渐向形式化描述方法过渡和发展，并逐渐渗透到网络协议分析、综合及测试的各个环节中，形成应用于各个环节的软件工程方法。本文通过对通信网络协议的要素进行分析，并对网络协议形式化方法、形式化模型及描述进行阐述，在此基础上对通信网络协议的形式化方法进行了探究，并给出了一些自己的看法和建议。     

汉英菜名概念框架元素语言形式化的凸显元素组合及结果对比研究

汉英菜名概念框架元素的语言形式化的差异主要体现于凸显元素组合和结果两个方面;凸显元素组合方面,二者存在汉语菜名概念框架中凸显元素组合的类型较英语更丰富等4条差异;结果方面,英语菜名的形式结构与概念结构的象似性较强,汉语菜名的则较弱。     

基于Event-B的自动化模块组合方法研究

Event-B共享变量和共享事件方法可将大型系统分解成多个子系统,并独立建模开发,但其需要手工干预以实现模型间事件的组合。为提高组合效率,提出一种针对模型的自动化组合理论,并开发自动化组合工具原型。为在精化模型中逐步引入模块调用,改进PROG方法,开发自动精化工具原型。通过2个应用案例,验证了自动化组合工具能自动组合事件,自动精化工具能减少调用变量的数量,从而增强系统模型的可读性和可维护性。     

基于符号模型检测的Web服务组合形式化验证

随着经济的发展和市场竞争的加剧,企业必须能够快速且准确地满足市场和用户的各种需求。Web服务组合正是由于单个Web服务不能满足企业及用户的需求而产生的一种技术,而如何确保组合的正确性来实现服务增值是一个尚未完全解决的问题。针对此问题,提出了一种基于符号模型检测器NuSMV对Web服务组合进行验证的方法,并提出了基于消息会话的Web服务有限状态自动机的形式化定义。最后实例验证了Web服务组合交互的正确性和有无死锁状态现象,进一步证明了方法的可行性。