摘要：安全关键系统的失败会造成很严重的后果,确保其正确性非常重要.空间嵌入式操作系统是一个典型的安全关键系统,在其内存管理的设计上,必须保障其高效的分配与回收,同时对系统资源的占用降到最低.在传统的软件开发过程中,通常是在整个软件开发结束后再进行集中测试及验证,这样势必会造成开发进展的不确定性.因此,将形式化验证方法和软件工程领域内的“需求-设计-实现”的3层开发框架相结合,通过性质分层传递验证的方法,保证了各个层次间的一致性.首先,从需求层面的需求分析开始,引入形式化证明的思路,证明对需求层逻辑的正确性,从而可以更好地指导程序的设计.其次,在设计层面的验证可以极大地减少开发代码的错误率,证明设计算法和需要实现的函数之间调用逻辑的正确性.最后,在实现层,证明所实现代码与函数设计的一致性,并且证明代码实现的正确性.使用交互式定理证明辅助工具Coq,以某一国产空间嵌入式操作系统的内存管理模块为例,证明了其内存管理算法的正确性以及需求、设计、实现的一致性.

摘要：软件测试是一种广泛使用的软件质量保证手段.变异测试是一种基于故障的软件测试方法,广泛用于评估测试用例集的充分性与软件测试技术的有效性.数量庞大的变异体导致变异测试的成本非常高.提出一种数据流分析指导的变异体精简方法(DFSampling),设计了启发式规则,基于这些规则对随机选择技术与基于路径感知的变异体精简技术(PAMR)进行了改进.采用经验研究的方式评估了DFSampling的有效性,比较了DFSampling与随机选择技术、PAMR技术的有效性,实验结果表明DFSampling是一种有效的变异体精简策略,提高了变异测试的效率.

摘要：将确定性元胞自动机、随机元胞自动机、及作者创建的多元随机元胞自动机，用于模拟自然界广泛存在的自组织现象。建立了若干自组织行为的元胞自动机模型，并用自己编制的ＰＣＷｉｎｄｏｗｓ环境下的通用元胞自动机程序，模拟了ＢＺ振荡反应、定向压力下结晶条带形成、三分子化学反应等自组织过程。最后对该程序的工作平台及主要的模块与功能作了简单的说明。

摘要：为确保星上操作系统中任务管理设计的可靠性,利用定理证明工具Coq对操作系统任务管理模块进行需求层建模及形式化验证.从用户角度,基于星上操作系统任务管理的基本机制,提出一种基于任务状态列表集合的验证框架.在需求层将基本机制进行形式化建模,并在Coq中实现.针对建立的需求层模型,提出6条与实际星上操作系统任务管理一致的性质并进行验证.给出其中一条性质在Coq中的验证过程,结果表明,模型满足该条性质.

摘要：模型库管理系统是决策支持系统的核心，其基本功能包括模型的定义、组合、存储和调用．该文介绍一个支持客户／服务器模式的模型库管理系统的设计和实现，在这个系统中，模型被视为程序模块，通过运用面向对象的方法进行组织以及对模型的远程和动态的透明调用提供支持，使实现的系统具有良好的动态可扩充性．同时，通过提供模型定义语言和模型库管理，便于决策支持系统客户软件的开发．

摘要：布料上的污渍效果是计算机游戏和影视制作中有待模拟的细节之一.提出一种基于物理的布料上污渍效果的真实感模拟的方法——采用多层模型对布料进行建模.对于污渍在布料上的渗透和扩散运动,提出了NSEAM(Navier-Stokes equations for anisotropic edia)模型,它可以模拟污渍和布料之间的相互作用,如扩散作用、蒸发作用、渗透作用等.最后,采用硬件加速的方法对上述过程进行了真实感绘制.实验结果表明,文中方法可以生成不同结构的布料上较为逼真的污渍效果,其绘制效果令人满意.

摘要：借鉴组合逻辑电路固定型故障的诊断原理,提出一种软件边界测试点选取策略.根据RSDIMU容错软件需求规范开发出52个测试用例,同时采用边界值分析、健壮性测试等边界值测试方法设计了2组测试用例,对34个版本的RSDIMU程序和429个变异体进行了测试.实验结果表明:该方法是一种有效的边界测试点选取策略,可以克服测试的盲目性,降低测试成本,明显地提高故障覆盖程度.

摘要：针对字符串测试数据自动生成,讨论了字符串间的距离,将不满足路径条件的字符串谓词表示成一个实值目标函数;利用快速下降搜索算法实施目标函数极小化,实现了基于搜索的面向路径字符串测试数据自动生成方法;探讨了其测试数据生成效率与初始输入、路径处理顺序之间的关系,并与遗传算法等几种算法进行了比较.实验结果表明:该方法是一种更经济有效的测试数据生成方法.

摘要：XML模式和DTD(documenttypedefinition)规范化设计是给出一个很好地表示数据间依赖关系并消除了冗余的XML模式或DTD的集合.目前在这一方面开展的研究还不多,而且才刚起步.Provost提出将关系数据库理论应用于XML模式规范化设计的思想,这一思想还没有付诸实施.在Provost思想的基础上给出用于XML模式和DTD规范化设计的层次模式设计的算法.首先分析了基于Provost思想的层次分解;然后给出用于消除冗余模式的分解树设计算法;最后给出用于XML模式和DTD规范化设计的层次模式设计算法,这一算法克服了Provost思想的缺陷.相应于其他XML模式和DTD规范化设计的研究,在算法产生的层次模式中,完全MVD(multivalueddependency)和嵌入MVD的集合由给出的MVD集合导出;并且产生的层次模式具有消除冗余模式和满足无损联接的特性.

摘要：为了在构建大规模森林场景时快速而有效地在森林区域内分布大量的植物,提出一种基于Poisson disk tiles模型,通过样本块拼铺的方式快速合成大面积植物分布的方法.在样本集生成阶段,采用一种角匹配的方式,并配合Relaxation dart throwing算法来生成植物分布的样本块集合,从而克服了传统方法中的圆盘越界问题和顶角问题;在合成阶段,按照角匹配的方式,并采用直接随机拼铺的模式来快速合成视域范围内的植物分布,可满足大规模植被场景的实时合成与漫游要求.此外,提出一种合成植物多密度变化、多物种混合分布的方法,其采用一种分离策略,通过从高密度样本块中分离提取一部分样本点来生成多密度等级及多物种等级的子样本块集;根据所合成地区的密度信息和物种信息来选取合适的样本块集进行拼铺,从而合成带有密度变化及多物种混合的植物分布.在此基础上,实现了一个大规模森林场景的构建与漫游系统.实验结果表明,文中方法在构建大规模植物场景上是非常有效的,即使植物规模达到千万级,其合成效率也可以满足交互式应用的需求.