检索结果-南通市图书馆

A Z Specification for Employment Clerical System

在线全文

学校读者我要写书评

暂无评论

Advances in Manufacturing 2000年第2期4卷 123-127页

作者： huai-kou miao Teklay Tesfay Bizuneh Bekele School of Computer Engineering and Science Shanghai University Shanghai 200072 China

Z has become recognized as a very effective formal specification language in improving the quality of software and ensuring the cost effectiveness of the development process. This paper presents part of a case study ... 详细信息

关键词： Z specification schema ClericalTemps

抽象精化和可满足性结合的EFSM模型测试用例优化生成

在线全文

学校读者我要写书评

暂无评论

计算机学报 2016年第11期39卷 2236-2252页

作者：陆公正缪淮扣苏州市职业大学计算机工程学院江苏苏州215104 上海大学计算机工程与科学学院上海200072 上海市计算机软件测评重点实验室上海201112

基于模型的测试是测试自动化的重要手段,通常采用模型检验技术从系统模型自动生成测试用例集,但生成的测试用例集往往存在冗余,这将影响测试用例执行的性能和成本.该文以扩展有限状态机(Extended Finite Machine,EFSM)为建模工具,根据... 详细信息

基于模型的测试是测试自动化的重要手段,通常采用模型检验技术从系统模型自动生成测试用例集,但生成的测试用例集往往存在冗余,这将影响测试用例执行的性能和成本.该文以扩展有限状态机(Extended Finite Machine,EFSM)为建模工具,根据公式簇建立状态等价关系,构建抽象模型,采用模型检验技术生成抽象反例(测试用例);给出了判定生成的抽象反例是否为伪反例的方法;采用反例引导的方法精化抽象模型,删除伪反例;最后,使用我们之前提出的基于可满足性的测试用例生成方法在抽象模型上生成约简的测试用例集.实验表明:该方法的测试用例数目约简比例最高达76%(警报侦测组件EFSM),总长度约简比例最高达68%(ATM EFSM),同时不会影响测试用例集的迁移覆盖率和查错能力.

关键词：测试用例约简扩展有穷状态机公式簇抽象反例引导的精化可满足性

Automatic generating test cases for testing Web applications

在线全文

学校读者我要写书评

暂无评论

通讯和计算机（中英文版） 2008年第6期5卷 21-26页

作者： CHEN Sheng-bo miao huai-kou QIAN Zhong-sheng School of Computer Engineering and Science Shanghai University Shanghai 200072 China School of Information Technology Jiangxi University of Finance ＆ Economics Nanchang 330013 China

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

基于规格说明的若干逻辑覆盖测试准则

软件学报 2010年第7期21卷 1536-1549页

作者：钱忠胜缪淮扣上海大学计算机工程与科学学院上海200072 江西财经大学信息管理学院江西南昌330013

基于规格说明的测试可以在不需要了解软件程序代码的情况下对软件进行功能测试.判定是形式规格说明中用于描述前、后置条件的主要形式.分析了基于规格说明的逻辑覆盖测试准则,针对已有的决定性逻辑覆盖测试准则的不足,提出了掩盖性逻辑... 详细信息

基于规格说明的测试可以在不需要了解软件程序代码的情况下对软件进行功能测试.判定是形式规格说明中用于描述前、后置条件的主要形式.分析了基于规格说明的逻辑覆盖测试准则,针对已有的决定性逻辑覆盖测试准则的不足,提出了掩盖性逻辑覆盖测试准则,并对其进行了详细分析.提出了掩盖性逻辑覆盖测试准则的一个可行的测试生成算法.根据该准则生成的测试用例能够发现条件的掩盖性带来的错误.然后,从判定的结构入手,分析了条件之间的约束关系、复杂判定的分解与合成、判定之间的关系.这些分别能够阐明逻辑覆盖中条件间的耦合性问题、同一个条件在判定中的多次出现问题以及判定在程序中的位置问题.继而提出了全真判定覆盖、全假判定覆盖、完全子判定覆盖、唯一条件真覆盖以及唯一条件假覆盖等测试准则.满足这些测试准则的测试用例集能检测出不同类型的错误.最后,给出了这些测试准则之间的包含关系图,并建议了不同测试准则适用的应用场景.

关键词：测试用例测试准则判定条件规格说明包含关系

在线全文

学校读者我要写书评

暂无评论

构件组合的抽象精化验证

软件学报 2008年第5期19卷 1149-1159页

作者：曾红卫缪淮扣上海大学计算机工程与科学学院上海200072

针对构件组合的状态爆炸问题,改进了反例引导的抽象精化框架,提出了组合式的抽象精化方法,使构件组合的模型检验转化为各成分构件的局部抽象精化,降低了分析的复杂度.提出了在构件组合情况下基于等价关系和存在商的构件抽象方法,用构件... 详细信息

针对构件组合的状态爆炸问题,改进了反例引导的抽象精化框架,提出了组合式的抽象精化方法,使构件组合的模型检验转化为各成分构件的局部抽象精化,降低了分析的复杂度.提出了在构件组合情况下基于等价关系和存在商的构件抽象方法,用构件抽象的组合建立构件组合的抽象;提出了组合确认定理并给出证明,使反例确认分解为在各构件上对反例投影的确认;通过对单个构件的等价关系的精化实现构件组合的抽象模型的精化.在模型检验构件组合的过程中,不需要为构件组合建立全局的具体状态空间.

关键词：构件组合模型检验状态爆炸等价关系反例引导的抽象精化

在线全文

学校读者我要写书评

暂无评论

模型驱动架构中模型构造与集成策略

软件学报 2006年第6期17卷 1411-1422页

作者：刘静何积丰缪淮扣华东师范大学软件学院上海200062 上海大学计算机科学与工程学院上海200072

模型驱动式开发是以模型构造、模型转换和精化为核心的.对象管理组织OMG选择将统一建模语言UML作为标准建模语言,并将其作为模型驱动架构MDA的支持平台.但UML模型缺乏严格的语义,不同视角和不同开发阶段的模型很难集成,所以目前MDA中各... 详细信息

模型驱动式开发是以模型构造、模型转换和精化为核心的.对象管理组织OMG选择将统一建模语言UML作为标准建模语言,并将其作为模型驱动架构MDA的支持平台.但UML模型缺乏严格的语义,不同视角和不同开发阶段的模型很难集成,所以目前MDA中各种模型之间是脱节的.基于统一程序设计理论UTP,将对象精化演算系统rCOS与UML结合起来,提高了UML模型的精确性与模型转换能力.建立模型驱动式开发中不同层次、不同视角的相关模型并将它们集成起来,建立了一个统一的模型系统.

关键词：模型驱动架构(MDA) UTP 模型构件形式方法

在线全文

学校读者我要写书评

暂无评论

用模型检验产生安全性质的测试

应用科学学报 2011年第5期29卷 529-536页

作者：曾红卫缪淮扣上海大学计算机工程与科学学院上海200072 上海市计算机软件评测重点实验室上海201112

安全关键系统必须满足规定的安全性质.测试生成通常独立于给定性质,"先验证再测试"的方法不能保证安全性质被测试.为此,该文提出了一种基于输入-输出标记迁移系统的安全性质测试方法.用输出变异建立被测实现的输出-完全模型,通过发现危... 详细信息

安全关键系统必须满足规定的安全性质.测试生成通常独立于给定性质,"先验证再测试"的方法不能保证安全性质被测试.为此,该文提出了一种基于输入-输出标记迁移系统的安全性质测试方法.用输出变异建立被测实现的输出-完全模型,通过发现危险迹产生测试用例.给出了基于图结构覆盖的安全性质测试准则,提出了形式化测试准则的方法.使用模型检验器NuSMV检验输出-完全模型可产生既满足结构覆盖又与安全性质相关的测试用例.

关键词：安全性质模型检验测试生成危险迹

Specifying Hotel Guestroom Reservation System Using ZNotation

在线全文

学校读者我要写书评

暂无评论

Advances in Manufacturing 1999年第4期 287-292页

作者： miao huai kou Bizuneh Bekele Teklay Tesfay (School of Computer Engineering and Science, Shanghai University)

The use of formal specification in software development is becoming increasingly prevalent. The Z notation is a formal method, a language, and a style for expressing formal specification of software systems. This pape... 详细信息

关键词： Z notation state model schema state schema

An approach to formalizing specification-based class testing

在线全文

学校读者我要写书评

暂无评论

Journal of Shanghai University(English Edition) 2006年第1期10卷 25-32页

作者：缪淮扣刘玲 School of Computer Engineering and Science Shanghai University Shanghai 200072 P. R. China

This paper presents a framework that can be used to formalize the specification-based single-class test generation process. Object-Z is used to describe both software requirements and the proposed framework. Using this framework, test engineers can automatically get the testing process model during the test generation process. With this model, properties of test cases （ such as relationship between test cases and methods can easily be captured. Furthermore, with the framework, the test process model can be updated automatically with the test generation process. The properties of test cases can then be updated correspondingly. It will greatly facilitate the regression testing. The main contribution of this paper is that it provides an approach to formalizing testing process by extending existing framework to class testing, and a way to represent test cases as multi-part, multi-step, multi-level artifacts.

关键词： test class framework class testing finite state machine (FSM) Object-Z.