摘要：安全关键系统的失败会造成很严重的后果,确保其正确性非常重要.空间嵌入式操作系统是一个典型的安全关键系统,在其内存管理的设计上,必须保障其高效的分配与回收,同时对系统资源的占用降到最低.在传统的软件开发过程中,通常是在整个软件开发结束后再进行集中测试及验证,这样势必会造成开发进展的不确定性.因此,将形式化验证方法和软件工程领域内的“需求-设计-实现”的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个变异体进行了测试.实验结果表明:该方法是一种有效的边界测试点选取策略,可以克服测试的盲目性,降低测试成本,明显地提高故障覆盖程度.

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

摘要：自然景观真实感的模拟是计算机图形学领域中的研究热点和难点之一.尽管人们对静态云的真实感模拟进行了大量的研究,动态云模拟的工作还比较少.动态云的快速模拟技术在计算机游戏动画、飞行视景仿真、影视广告等许多领域具有重要的应用价值.提出了一种三维动态云快速模拟的新方法.首先,在较低分辨率的网格上求解云运动的物理方程,获得动态云的速度场.然后,采用纹理漂移的方法来增加云的表面细节.通过充分利用GPU的加速性能,该算法可以达到较高的绘制速度.最后,对上述算法进一步优化处理,使其可以适用于多种硬件平台.

摘要：本文提出了一种基于虚拟页地址映射的NAND Flash管理算法.该算法通过定义坏块表、对应表等结构,以及设计的坏块替换策略和虚拟页地址到实际物理页地址的转换算法,实现上层软件采用虚拟地址对NAND Flash的无坏块连续页地址访问.该算法是一种高效的地址映射算法,能高效地对数据进行索引,占用SRAM空间较少,使系统达到高性能,并使得闪存使用的更加稳定持久.

摘要：低成本卡通制作中的图像和视频通常缺乏对动物角色毛发效果的表现,为了能对已有图像及视频中的动物角色进行处理,为其增添具备真实感的毛发效果,提出一种毛发风格化算法——卡通化毛发纹理算法.针对卡通中的动物角色合成毛发纹理并进行替换,分为图像应用及视频应用2个部分.在图像替换时,对要进行风格化处理的目标区域进行图像结构分析,以获取覆盖目标区域的三角网格,再生成毛发纹元并映射于网格之上,通过绘制纹元来生成具备真实感的毛发效果;在进行视频替换时,提取视频关键帧并基于图像应用算法生成相应的卡通化毛发纹理进行图像替换,之后根据关键帧的替换结果指导整个视频的替换.为了获取随时间变化的图像关键帧目标区域,采用SIFT算法计算特征点在时间轴上的匹配;为了快速合成卡通化毛发纹理,采用基于GPU的光线行进算法加速毛发纹元的体绘制过程.实验结果表明,文中算法可成功地对已有图像及视频的动物角色添加具备真实感的毛发效果.

摘要：随机测试是实践中广泛采用的一种黑盒测试方法.近年来提出的适应性随机测试方法改进了随机测试的不足,仿真实验结果表明,改进效果取决于软件失效域的特征.提出以测试约束刻画软件失效域在输入域上的分布,探讨了基于现有的程序分析技术构造测试约束的过程,讨论了基于测试约束的软件失效域的特征分析方法.以一个实例软件验证所提出的测试约束构造过程及其软件失效域特征分析方法.测试约束揭示了软件故障的触发与传播的内在机制,基于测试约束的软件失效域的特征分析方法有助于改进测试用例的设计质量以及评价适应性随机测试方法的适用性.