软件形式化方法与应用专题前言

形式化方法起步于程序理论和语义的研究,历经50余年的发展,成为了计算机科学的重要领域.它使用严格的数学方法,研究并发展软件和硬件系统的建模、设计、开发、验证与演化等技术,为保障系统的正确性、可靠性和安全性提供了重要途径.本专刊收录的13篇论文反映了近年来我国学者在软件形式化方法与应用领域的部分研究成果.     

基于工作流的软件过程开发平台的研究*

首先介绍了传统软件过程中人为因素的影响,并给出了减少这种影响的解决方法：在工作流与软件过程相结合的基础上集成软件过程开发平台SPDET（Software Process Develop Environment Tool）。然后详细的讨论了SPDET的几个重要的组成部分,并给出了SPDET的设计和实现。     

UML statecharts的测试用例生成方法

测试用例生成是软件测试的关键。根据UML statecharts的层次和并发结构,研究相应的测试用例产生方法。它视复合状态为抽象状态,分别构造主UML statecharts和复合状态所对应的子UML statecharts的测试基,并依据一定的合成规则和Wp－方法生成整个UML statecharts的测试用例。这种方法能够支持递增式测试用例的生成。理论和实验结果说明,如果满足测试条件,它们保证全故障覆盖,且产生较好的测试用例。这种改进对大型复杂系统尤其有效,也便于构造自动测试工具。     

基于IDA-Pro的软件逆向分析方法

二进制程序转换作为软件逆向分析的主要手段发挥着积极作用。该文给出一种程序转换方法,应用软件二进制程序经IDA Pro反汇编得汇编语言程序,依据下推自动机原理设计汇编文法识别该汇编文件、制定相应的转换规则和优化措施将汇编语言转换成中间语言。转换所得中间语言可读性较强,具有通用性且易于理解。该方法达到了较高的自动化程度,缩小了目标程序的代码量,其应用可有效地减少软件分析和调试人员在追踪代码时所需的时间和工作量。给出应用上述方法进行程序转换的实例。     

UML Statecharts的切片模型检验方法

统一建模语言UML已被广泛应用于软件设计和开发中,而验证UML模型是否满足关键的性质需求成为一个重要问题.由于空间爆炸和语义的复杂性,对Statecharts进行模型检验受到软件规模和设计精化程度的制约.本文在用扩展层次自动机(EHA)结构化的表示UML Statecharts后,通过分析EHA中存在的层次、并发和事件同步等特征定义了一组依赖关系.对于由状态和迁移组成的切片准则,给出对EHA进行切片的算法.该算法能保证切片后的EHA与原来的Statecharts对性质具有相同的可满足性,且删除了与被验证性质无关的层次和并发状态,缓解了空间爆炸问题.     

面向路径的测试数据自动生成工具及其图形界面的Tcl/Tk设计

面向路径的测试数据生成问题是软件测试中一个基本问题。文章介绍了自主开发的面向路径的测试数据自动生成工具。Tcl/Tk是一种图形界面设计工具,其功能强大,可运行于Windows,UNIX等操作系统上,具有良好的可移植性。文章简要介绍Tcl/Tk,并给出用Tcl/Tk设计面向路径的测试数据自动生成工具的图形界面的方法。     

基于使用模型的统计测试方法的研究

介绍了基于使用模型的统计测试方法，论述了使用模型的概念和特点，以及从使用模型中可以计算出的静态参数和它们在统计测试和软件开发中所起的作用，还具体阐述了怎样通过使用模型生成测试用例，同时根据测试充分性理论讨论了统计测试中测试充分性的度量方法，最后简要介绍了自行开发的统计测试辅助工具STToolkit。     

面向路径的测试数据自动生成工具的设计与实现

面向路径的测试数据生成问题是软件测试中的一个基本问题。Gupta等提出一种线性化谓词函数的迭代松驰方法求解该问题。文献[2]改进了该方法，证明改进后的方法与原方法生成的约束系统相同，文章以改进后的方法为核心算法，根据软件工程的思想，采用面向对象的方法，使用UML进行设计，并且在Linux Red Hat7.0操作系统下用C＋＋语言言实现一个为程序路径自动生成测试数据的原型工具，然后将它移植到Windows操作系统。     

标记迁移系统的组合可达性分析

标记迁移系统是一种在计算机辅助设计和验证中得到广泛使用的形式模型。当系统中的模块比较多时,系统的整体模型有可能出现状态空间的指数级爆炸,组合可达性分析是缓解这一问题的一种有效方法。已有的工作缺乏对该方法基本原理的清晰描述和精确表达。本文对其基本原理进行了分析和概括,并作了形式化陈述,证明了相关结论。本文的工作有助于深入理解和澄清组合可达性分析的内部工作机制。     

一种面向性质的实时系统测试方法

尽管Statecharts在反应式实时系统建模领域获得了广泛应用,基于Statecharts开发的实时软件的测试仍然十分困难.由于引入了时间维,待测系统的行为空间变得非常庞大,使得难以对其进行全面深入测试.本文提出了一种面向性质的实时系统测试方法.首先对UML Statecharts作适当实时扩展,使得扩展后能描述non-trivial时间约束;然后用一种受限实时逻辑描述待测系统的功能特性;在此基础上根据待测性质从系统模型生成有针对性的测试序列.实验表明,在相同测试深度下,面向性质测试比非面向性质测试需要少得多的测试序列.