基于时序逻辑的编译优化形式化描述及测试用例生成方法

来源 :中国科学院软件研究所 | 被引量 : 0次 | 上传用户:q19070
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
编译器是软件开发的基础支撑性工具,它的正确性直接影响到应用软件的可靠性,保证其质量的有效手段之一是软件测试。优化是编译过程中的重要阶段,它主要通过对程序进行等价性变换来提高目标程序的执行性能,或缩减目标程序的代码规模、降低程序的运行功耗等。编译优化测试是针对编译器优化功能和效果的测试,检查经过优化变换后的代码是否保持了原程序的功能语义、是否达到了性能改进的目标。   编译测试的主要流程和通常的软件测试一样,包括了测试用例生成、测试用例执行以及测试结果判定等活动。编译器测试中的测试用例是高级语言源程序,手工生成工作量大,难以保证充分的覆盖度,为提高效率,需要有自动化的测试用例生成方法。自动化的测试用例生成方法需要对优化进行形式化描述作为支撑。   典型的优化变换包括四个部分:源程序、目标程序、变换动作以及变换实施的使能条件,其中使能条件是源程序具有的某种程序性质。变换描述语言TRANS采用条件重写规则描述优化变换,其中使能条件用时序逻辑公式表示。   循环优化是一种重要的优化,其变换的实施通常涉及到循环结构、归纳变量、循环依赖的识别。本文针对循环优化的特点,对TRANS语言做了宏扩展,详细讲述了循环、循环嵌套、归纳变量、循环依赖等循环结构和基础特征的时序逻辑特性,给出相应的TRAINs语言宏定义;并以循环逆转、循环交换、循环合并三个典型的优化为例阐述了扩展宏定义的使用方法。扩展的宏定义能简化复杂的循环优化变换描述结果,为针对优化的测试用例自动化生成以及形式化验证研究奠定了基础。   本文提出了一种基于时序逻辑的编译优化测试用例生成方法。该方法通过变换中涉及的关键语句和它们之间的关系构造测试用例的模板,在模板之上通过随机策略插入程序语句从而完成测试用例的生成。它的核心是关键结点控制图生成算法,关键结点控制图是测试用例模板的表现形式,算法包括三个阶段:初始化、时序逻辑公式规整化和图的生成。该方法为多种编译优化的测试提供了统一的用例生成方法,生成的测试用例具较强针对性。
其他文献
随着电子商务的迅速崛起,Web应用已发展到全球化,Web服务作为一种新兴的web应用模式,是B2B(business to business)和.B2C(Business to customer]应用中有效的解决方案,它是一个崭
近年来,随着计算机和网络的广泛应用,人们的生活、学习和工作方式开始发生变化。在带来方便和快捷的同时,网络安全、计算机安全及信息安全开始引起人们的重视。 在保护计算机
随着科学技术的不断发展,人们对智能家居的需求越来越强烈,消费者希望借助智能家居从繁重的家庭生活中解放出来,实现对家庭设备的远程控制、统一管理;厂商也可以通过智能家居产
随着计算技术应用领域的不断扩大和网络技术的快速发展,普适计算、泛在计算等计算模式成为研究热点。适应这一发展趋势,未来的嵌入式操作系统将向小型化、一体化、个性化方向发
图像融合是图像处理中的一个新兴研究领域,它在图像空间配准的基础上,采用图像处理方法分析每幅待融合图像的特征,借鉴多源信息融合的理论,采用合适的融合策略来融合这些特征
随着信息技术的不断发展和计算机网络的日益普及,网络安全问题日趋严重。现有的安全技术与产品主要应用和部署在网络层,在一定范围内能保障网络系统的安全,实际应用中,更需要采取
随着计算机仿真技术和高精度传感仪器的发展,科学研究各领域的数据量呈现爆炸式增长。与此同时,数据类型多样化和处理速度难以匹配生产速度等问题也对科学数据管理提出了挑战。
隐蔽通道包括所有可以绕过系统强制访问控制机制的通信机制,隐蔽通道分析是高安全级信息系统设计开发过程中必不可少的组成部分。本文研究了隐蔽通道的标识、带宽计算模型和隐
海洋环流模式被广泛应用于海洋环境和气候预测研究。随着研究不断深入,海洋环流模式向着高分辨率的方向发展。分辨率的提高会导致模式的计算量和模式对计算资源的需求呈几何级
门户提供了对信息资源的单一访问入口。随着信息化建设的深入,门户已经成为企业新型办公环境的重要组成部分,并在消除信息孤岛等方面发挥了关键的作用。   集成企业内部和外