基于场景的形式化测试模型生成方法

在复杂的Web应用软件中,如何有效地实现自动化测试是当前软件测试研究中的热点与难点.使用统一建模语言（unified modeling language,UML）状态图对Web应用软件的行为建模,利用已有的方法将已建好的模型形式化成有限状态机(finite state machine,FSM);然后使用UML顺序图表示场景,通过使用场景规约系统行为,最终得到约简后的形式化测试模型用以实现自动测试.     

一种将遗传算法应用于谓词求精的方法

提出了将Manna的程序综合方法和Caroll Morgan的求精演算方法相结合的求精方法.为了提高求精的自动化程度,在求精的规则选择过程中引入遗传算法.利用遗传算法能够在庞大的规则库空间中搜索合适规则的特性,提高求精的自动化程度.     

自动定理证明中的一个通用证明法

在自动定理证明中，我们发现一个卓有成效的证明方法——多余文字参数法．利用这一方法可以简单便捷地证明许多难以证明的各种推理策略中的完备性问题．本文列举了如何应用这一方法来证明自动定理证明中归结原理的完备性、语义归结的完备性、线性归结的完备性以及输入归结和单位归结的等价性问题．事实表明这些原本都是十分棘手的证明问题，由于使用了这一方法而变为十分简单而自然的工作，而且这些不同的完备性问题其证明步骤和过程也几乎是一样的     

一个基于AI产生式系统的软件开发新模型

在设计一个程序以前，应该完整地并且精确地说明要求解的问题．作为一个产品。软件相对于其形式规格说明来说应该是可靠和正确的．规格说明是程序变换方法的起点，程序变换方法保证了程序的正确性．本文给出了ＡＤＴＳＬ的简要描述，并提出了一个基于人工智能中的产生式系统的软件开发新模型．     

一种改进的实时系统可达性分析算法

首先简介了时间自动机、时钟区域、区域等价、时钟带的概念.利用时钟带,可以将时间自动机的无穷状态空间转化为有穷.实时系统的绝大多数安全性和部分活性可以通过可达性分析算法来验证.然而,当系统时钟个数较多时,用DBM存储时钟带,会造成内存空间的很大耗费.该文提出了用邻接表存储时钟带,给出了改进的算法,并对算法的空间复杂度作了分析.实验表明,当时钟个数大于5时能节约很大的内存空间,从而在一定程度上缓解了状态爆炸.     

基于LSC模型检验的性质抽取

采用LSC(live sequence chart)描述基于场景的需求规格说明,根据设计模型必须满足需求规格说明的一致性原理,针对安全性、可达性、活性等性质,设计3种用于自动生成和抽取性质的覆盖准则,并根据准则从LSC需求规格说明中抽取与设计模型相关的性质.抽取的结果可用于自动化验证,为验证需求模型与设计模型的一致性提供保障.     

用XML实现基于大型数据库的结构化排版

近年来信息咨询企业的业务发展迅猛,纸质信息咨询产品的种类越趋繁多,客户数量也成千上万地增长.客户信息自然需要用Oracle等大型数据库进行管理;而信息的排版现在也有相当多的软件,例如Adobe公司的FrameMaker SGML等.为了使这些排版软件能够灵活、有效地从大型数据库中抽取需要的客户信息,必须在这两者之间架起一座方便的桥梁.该文介绍用FrameMaker SGML进行2次开发的原理,给出了用XML实现从大型数据库抽取客户信息数据,再由FrameMaker SGML进行编辑排版的技术,最后讨论了主要模块的设计和实现.     

结构化面向对象形式规格说明语言OOZS——类型检查器

ＯＯＺＳ类型检查器是ＯＯＺＳ规格说明的一种检查程序,它可以找出用户编写的ＯＯＺＳ规格说明中出现的语法错误以及类型操作的不一致错误,并能够自动定位错误．本文介绍了ＯＯＺＳ类型检查器的设计与实现．     

一种用于模型验证的Web应用模型抽取方法

以模型验证为目标,提出一种Web应用FSM(finite state machines)模型的抽取方法. 该方法将模型抽取划分为链接提取、模型构造和结果显示. 通过建立标签库和对标签的定位,并结合正则表达式的方法,对Web应用进行逆向分析,从源代码开始进行链接及相关信息的提取、规整和存储. 对Web应用中的页面、链接等建模元素进行分析,应用映射与聚合等抽象技术对获得的信息进行重构,得到适用于验证的Web 应用的FSM模型.     

一种基于Object-Z规格说明的集成测试用例生成方法

形式化方法具有精确的描述性和很强的抽象性.用形式化方法描述规格说明,避免了在需求分析阶段对数据结构和算法细节的详细描述,同时又避免了一般建模方法中的模糊性和歧义性.针对组件系统的集成测试产生测试用例,提出一种使用Object-Z模式描述组件模型的方法,并且针对模型提出测试准则,产生测试场景,然后根据得到的测试场景产生测试用例.