检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

C程序控制流程模型的提取技术与实现

计算机科学 2014年第5期41卷 208-214页

作者：杨昌坤许庆国上海大学计算机工程与科学学院上海200072 上海市计算机软件评测重点实验室上海201112

控制流图描述了函数执行时可能采取的执行路径。绝大多数静态分析工具都在抽象语法树之上生成控制流图并据此对程序的运行行为进行分析。在模型检测过程中,提取正确的控制流图是构建系统模型的关键。在分析C程序的抽象语法树和控制结构... 详细信息

控制流图描述了函数执行时可能采取的执行路径。绝大多数静态分析工具都在抽象语法树之上生成控制流图并据此对程序的运行行为进行分析。在模型检测过程中,提取正确的控制流图是构建系统模型的关键。在分析C程序的抽象语法树和控制结构的基础上,设计并实现了程序控制流图提取的算法,并分析了算法的正确性。基于提取的控制流程,可对C程序的某些性质进行模型检验。

关键词：控制流图抽象语法树模型检测

Nondeterministic Probabilistic Petri Net -- A New Method to Study Qualitative and Quantitative Behaviors of System

在线全文

学校读者我要写书评

暂无评论

Journal of Computer Science & Technology 2013年第1期28卷 203-216页

作者： Yang Liu Huai-Kou Miao Hong-Wei Zeng Yan Ma Pan Liu School of Computer Engineering and Science Shanghai University Shanghai 200072 China School of Information Science and Technology Taishan University Taian 271021 China State Key Laboratory of Novel Software Technology Nanjing University Nanjing 210093 China

There are many variants of Petri net at present, and some of them can be used to model system with both function and performance specification, such as stochastic Petri net, generalized stochastic Petri net and probabilistic Petri net. In this paper, we utilize extended Petri net to address the issue of modeling and verifying system with probability and nondeterminism besides function aspects. Using probabilistic Petri net as reference, we propose a new mixed model NPPN （Nondeterministic Probabilistic Petri Net） system, which can model and verify systems with qualitative and quantitative behaviours. Then we develop a kind of process algebra for NPPN system to interpret its algebraic semantics, and an action- based PCTL （Probabilistic Computation Tree Logic） to interpret its logical semantics. Afterwards we present the rules for compositional operation of NPPN system based on NPPN system process algebra, and the model checking algorithm based on the action-based PCTL. In order to put the NPPN system into practice, we develop a friendly and visual tool for modeling, analyzing, simulating, and verifying NPPN system using action-based PCTL. The usefulness and effectiveness of the NPPN system are illustrated by modeling and model checking an elaborate model of travel arrangements workflow.

关键词： nondeterminism probabilistic Petri net model checking action-based probabilistic computation tree logic

在线全文

学校读者我要写书评

暂无评论

表格语言的分析比较

计算机科学 2014年第3期41卷 23-26页

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

表格语言具有可读性和可理解性的优点,它能非常精确地表示软件系统需求。在过去的30多年间,表格语言已经成功地应用于多个安全关键嵌入式软件的开发中。准确了解这些表格语言的特性,对表格语言的研究及推广有重要的指导意义。对3种不同... 详细信息

表格语言具有可读性和可理解性的优点,它能非常精确地表示软件系统需求。在过去的30多年间,表格语言已经成功地应用于多个安全关键嵌入式软件的开发中。准确了解这些表格语言的特性,对表格语言的研究及推广有重要的指导意义。对3种不同的表格语言进行了详细的综述和讨论,从不同角度分析比较了其异同点,并提出了进一步的研究方向。

关键词：表格方法形式方法规格说明验证与确认工具支持

在线全文

学校读者我要写书评

暂无评论

一种基于特征迁移系统的软件产品线测试方法

计算机应用研究 2014年第9期31卷 2724-2728页

作者：杨华北曾红卫上海大学计算机工程与科学学院上海200072

为了在软件产品线的应用工程阶段最大程度地复用领域工程的测试用例,领域测试用例需要覆盖领域模型中的变化性。针对此问题,提出了一种以特征模型为出发点的软件产品线测试方法,通过扩展特征迁移系统建立软件产品线的领域行为模型,对模... 详细信息

为了在软件产品线的应用工程阶段最大程度地复用领域工程的测试用例,领域测试用例需要覆盖领域模型中的变化性。针对此问题,提出了一种以特征模型为出发点的软件产品线测试方法,通过扩展特征迁移系统建立软件产品线的领域行为模型,对模型中的变化性迁移进行抽象,得到精简的测试模型;应用迁移覆盖准则,导出包含变化性的领域测试用例;在应用工程阶段,根据具体应用所包含的特征,绑定领域测试用例中的变化性,复用领域测试用例导出针对具体应用的测试用例。最后通过一个咖啡机产品线验证了该测试方法,导出了可复用的领域测试用例。

关键词：软件产品线软件测试领域工程变化性标签迁移系统

在线全文

学校读者我要写书评

暂无评论

GUI回归测试的测试脚本修复技术研究

计算机应用研究 2016年第1期33卷 136-140页

作者：朱静曾红卫上海大学计算机工程与科学学院上海200072

回归测试对修改后的软件重新进行测试,确认修改没有引入新的错误或导致其他代码产生错误。研究图形用户界面(GUI)回归测试脚本的自动化修复技术,采用有限状态机描述GUI的交互行为,并基于有限状态机(FSM)产生测试用例集;使用自动化测试... 详细信息

回归测试对修改后的软件重新进行测试,确认修改没有引入新的错误或导致其他代码产生错误。研究图形用户界面(GUI)回归测试脚本的自动化修复技术,采用有限状态机描述GUI的交互行为,并基于有限状态机(FSM)产生测试用例集;使用自动化测试工具生成测试脚本,建立状态迁移和测试脚本的映射关系表;通过比较GUI新旧版本的FSM得到GUI的变化信息,根据变化信息和映射表对原测试脚本自动修复。实例验证了脚本修复方法的可行性和有效性,修复了失效的测试脚本,保证了修复后的测试脚本的完备性和一致性。

关键词：图形用户界面回归测试有限状态机模型比较测试脚本修复

在线全文

学校读者我要写书评

暂无评论

优化基于模型检验的测试生成

计算机辅助设计与图形学学报 2011年第3期23卷 496-502页

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

利用模型检验器输出的反例构造测试用例是测试自动化的一种重要手段.由于一个测试用例可能覆盖多个测试目标,测试生成过程中可能存在不必要的对模型检验器的调用,测试包也往往存在大量冗余,严重影响测试性能.为此,提出一种测试生成的动... 详细信息

利用模型检验器输出的反例构造测试用例是测试自动化的一种重要手段.由于一个测试用例可能覆盖多个测试目标,测试生成过程中可能存在不必要的对模型检验器的调用,测试包也往往存在大量冗余,严重影响测试性能.为此,提出一种测试生成的动态监控优化方法.在模型检验一个测试目标产生测试用例后,采用时态逻辑公式重写技术缩减测试目标集,删除那些被新测试用例覆盖的测试目标;同时,在新测试用例加入测试包时对其进行筛选,以消除冗余.实例结果表明,文中方法可有效地减少模型检验器的调用次数,缩减测试包.

关键词：模型检验测试用例生成时态逻辑公式重写测试包缩减

在线全文

学校读者我要写书评

暂无评论

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

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

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

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

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

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

基于Ajax技术的Web应用的建模与测试用例生成

在线全文

学校读者我要写书评

暂无评论

计算机科学 2014年第8期41卷 219-223,244页

作者：贺涛缪淮扣钱忠胜上海大学计算机工程与科学学院上海200072 上海市计算机软件评测重点实验室上海201114 江西财经大学信息管理学院南昌330013

Ajax技术使Web应用能够通过异步请求从服务端获取数据,并在网页上局部刷新显示。这使得一张网页可以包含多个不同状态,状态数的激增使其关系变得更加复杂,给Web应用的建模与测试带来了更大的难度。研究基于Ajax技术的Web应用的建模与测... 详细信息

Ajax技术使Web应用能够通过异步请求从服务端获取数据,并在网页上局部刷新显示。这使得一张网页可以包含多个不同状态,状态数的激增使其关系变得更加复杂,给Web应用的建模与测试带来了更大的难度。研究基于Ajax技术的Web应用的建模与测试用例生成方法,给出一种可行的产生测试用例的技术。结合课题组自身开发的项目进行建模与测试用例的生成分析,结果表明,该技术能有效地得到所需的测试用例。

关键词： Web应用模型检查测试用例 Ajax技术 Kripke结构

在线全文

学校读者我要写书评

暂无评论

基于FSM的测试理论、方法及评估

计算机学报 2011年第6期34卷 965-984页

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

为搭建基于FSM的测试方法由理论研究通往工业应用的桥梁,文中讨论了若干基于FSM模型的测试方法及其相关理论,提出构造区分序列的理论及测试序列集合冗余约简的理论,补充并实现了若干基于FSM的测试生成算法.随后文中提出了基于FSM的测试... 详细信息

为搭建基于FSM的测试方法由理论研究通往工业应用的桥梁,文中讨论了若干基于FSM模型的测试方法及其相关理论,提出构造区分序列的理论及测试序列集合冗余约简的理论,补充并实现了若干基于FSM的测试生成算法.随后文中提出了基于FSM的测试方法评估的5项量化指标,实验评估了若干基于FSM模型的测试方法,给出了一些基于FSM测试的经验建议.文中的评估有助于基于FSM的测试方法在工业中的推广.

关键词：基于FSM的测试测试评估测试生成算法基于FSM的测试理论冗余约简