相信逻辑的某些性质和定理

本文研究了相信逻辑在相信蕴涵下的某些性质．在相信蕴涵的定义下，相信逻辑是非单调的．本文给出了几个相信逻辑的单调性的充分且必要条件．还证明了一个默认理论的延伸恰好就是对应的相信理论的相信公式的所有相信蕴涵式的全体．从而给默认理论的延伸以一个较为直观、简洁的表述．     

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

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

Model Checking-Based Testing of Web Applications

A formal model representing the navigation behavior of a Web application as the Kripke structure is proposed and an approach that applies model checking to test case generation is presented. The Object Relation Diagram as the object model is employed to describe the object structure of a Web application design and can be translated into the behavior model. A key problem of model checking-based test generation for a Web application is how to construct a set of trap properties that intend to cause the violations of model checking against the behavior model and output of counterexamples used to construct the test sequences. We give an algorithm that derives trap properties from the object model with respect to node and edge coverage criteria.     

Data Exchange in Grid Workflow

In existing web services-based workflow, data exchanging across the web services is centralized, the workflow engine intermediates at each step of the application sequence. However, many grid applications, especially data intensive scientific applications, require exchanging large amount of data across the grid services. Having a central workflow engine relay the data between the services would resu＇lts in a bottleneck in these cases. This paper proposes a data exchange model for individual grid workflow and multiworkflows composition respectively. The model enables direct communication for large amounts of data between two grid services. To enable data to exchange among multiple workflows, the bridge data service is used.     

基于结构覆盖和状态识别的FSM一致性测试实验评估

针对在测试资源紧张的情况下所面临的不同测试技术中测试方法选择问题,阐明了对基于结构覆盖和基于状态识别的测试生成技术进行实验评估的必要性,以10个有限状态机（finite state machine, FSM）应用实例为实验对象,从测试开销和错误覆盖能力两方面对这两种技术进行了实证研究,为FSM一致性测试中这两种技术的选择应用提供了经验性的参考建议。     

OCL 2.0表达式语义学比较研究

从语法、语义域和语义映射三个方面,给出了基于UML元模型和形式化的OCL表达式语义描述.并探讨了OCL表达式上下文、OCL表达式赋值环境的概念.在OCL表达式语义的形式化描述中,定义了对象模型和OCL表达式语法,给出OCL表达式语义解释和OCL后置条件表达式的语义解释.通过对OCL表达式语义二种描述方法比较,可以看到OCL表达式语义学描述的关键是反映OCL表达式本质的语法描述.