检索结果-内蒙古大学图书馆

计算机科学 2005年第12期32卷 110-111,145页

作者：文艳军王戟齐治昌国防科技大学计算机学院长沙410073

标记迁移系统是一种在计算机辅助设计和验证中得到广泛使用的形式模型。当系统中的模块比较多时,系统的整体模型有可能出现状态空间的指数级爆炸,组合可达性分析是缓解这一问题的一种有效方法。已有的工作缺乏对该方法基本原理的清晰描... 详细信息

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

关键词：标记迁移系统计算机辅助设计和验证组合可达性分析状态空间爆炸问题观察等价

来源：评论

学校读者我要写书评

暂无评论

互模拟准局部验证算法的扩展与实现

引用

软件学报 2018年第6期29卷 1517-1526页

作者：郑晓琳邓玉欣付辰雷国庆上海市高可信计算重点实验室(华东师范大学) 上海200062 计算机科学国家重点实验室(中国科学院软件研究所) 北京100190

互模拟是并发系统分析和验证的一个重要概念.主要扩展了一种由Du和Deng提出的准局部算法,使其更加适用于一般的标记迁移系统.用Java实现扩展后的准局部算法与Fernandez和Mounier提出的局部算法.以VLTS为实验数据基准进行大量的实验,发... 详细信息

互模拟是并发系统分析和验证的一个重要概念.主要扩展了一种由Du和Deng提出的准局部算法,使其更加适用于一般的标记迁移系统.用Java实现扩展后的准局部算法与Fernandez和Mounier提出的局部算法.以VLTS为实验数据基准进行大量的实验,发现在大多数情况下,前者的性能比后者更好.同时,修改了算法使其能够验证模拟关系.最后,用Java实现对标记迁移系统进行转换,使算法同时可以验证弱互模拟关系.

关键词：互模拟标记迁移系统扩展

来源：评论

学校读者我要写书评

暂无评论

组合E-服务的活动链行为模式设计及验证

引用

同济大学学报（自然科学版） 2011年第3期39卷 427-433页

作者：陈波曾国荪李莉鲍宇同济大学计算机科学与技术系上海201804 广西工学院计算机工程系广西柳州545006

提出一种新颖的活动链的行为规范概念,该概念的粒度介于活动和场景概念之间,并根据基于活动链的行为刻画需求,设计"链存在、链缺失、链前提和链因果"四个行为模式,并给出这些模式到标记迁移系统LTS的映射规则,精确刻画了行为... 详细信息

提出一种新颖的活动链的行为规范概念,该概念的粒度介于活动和场景概念之间,并根据基于活动链的行为刻画需求,设计"链存在、链缺失、链前提和链因果"四个行为模式,并给出这些模式到标记迁移系统LTS的映射规则,精确刻画了行为模式的操作语义,通过定义组合E-服务满足活动链模式的内涵,给出可满足性验证的充要条件和判定算法,最后给出实例分析.

关键词：活动链行为模式组合E-服务可满足性验证标记迁移系统

来源：评论

学校读者我要写书评

暂无评论

DBMS安全审计功能测试用例生成方法

引用

清华大学学报（自然科学版） 2011年第10期51卷 1258-1263,1268页

作者：叶晓俊刘泊伶谢丰张翀斌李斌清华大学软件学院信息系统与工程研究所北京100084 中国信息安全测评中心北京100085

数据库管理系统(DBMS)安全审计功能的符合性测试要求测评人员设计有效覆盖安全功能规范的测试用例。本文提出一种基于安全审计规范使用标记迁移系统(LTS)建立形式化模型的DBMS安全审计测试用例自动化生成方法。该方法根据数据库分级评... 详细信息

数据库管理系统(DBMS)安全审计功能的符合性测试要求测评人员设计有效覆盖安全功能规范的测试用例。本文提出一种基于安全审计规范使用标记迁移系统(LTS)建立形式化模型的DBMS安全审计测试用例自动化生成方法。该方法根据数据库分级评估的安全目标建立审计功能组件的LTS模型,再依据LTS模型启发式路径搜索算法从模型的路径中生成测试场景,然后根据评估对象的安全约束填入被测数据库场景数据生成测试用例集。使用本方法产生了200多个测试用例,用例通过配置变量或设置语句等脚本化工作后在被测DBMS上运行,从中发现了未知安全隐患。实验结果表明:基于行为模型的测试用例生成方法能生成覆盖安全目标安全审计组件功能测试需求的测试用例集。

关键词：数据库安全审计安全目标标记迁移系统测试用例生成

来源：评论

学校读者我要写书评

暂无评论

基于事件结构的并发程序可视化调试方法

引用

软件学报 2014年第3期25卷 457-471页

作者：伍晓泉魏峻中国科学院软件研究所计算机科学国家重点实验室北京100190 中国科学院软件研究所软件工程技术研究开发中心北京100190 中国科学院大学北京100049

在多核和并发技术得到广泛应用的今天,如何有效地调试并发程序,成为一个重要且亟待解决的研究课题.并发程序的不确定性及其行为的复杂性,使得传统的调试技术难以得到有效的应用;而软件维护场景中错误发现与错误调试过程的分离使得错误... 详细信息

在多核和并发技术得到广泛应用的今天,如何有效地调试并发程序,成为一个重要且亟待解决的研究课题.并发程序的不确定性及其行为的复杂性,使得传统的调试技术难以得到有效的应用;而软件维护场景中错误发现与错误调试过程的分离使得错误重现难以实现,面向缺陷报告的调试需求使得自动的错误定位技术难以应用,加剧了调试的困难.针对软件维护阶段由缺陷报告导向的程序调试场景,提出了可视化的并发程序调试方法.该方法能够根据缺陷报告中的信息对程序进行切片,缩小需要分析的代码范围;通过静态分析构造出程序行为的全局视图,帮助程序员发现隐含的程序执行路径;根据事件结构的语义简化程序行为视图,使得行为模型规模可控;根据图形中的分支,引导用户关注路径中的关键操作,从而更快地发现程序中的缺陷.与动态调试方法相比,该方法能够避免错误重现的代价.借助缺陷报告中的信息以及事件结构模型的特点,该方法能够尽量减少状态爆炸的发生.已开发出的交互式并发程序调试工具原型JESVis Debugger,初步实现了所提出的方法.

关键词：可视化调试并发程序事件结构配置结构标记迁移系统

来源：评论

学校读者我要写书评

暂无评论

基于状态空间等价类的有色Petri网特性验证

引用

计算机工程与应用 2003年第11期39卷 16-18页

作者：李沛武华中科技大学计算机学院南昌水利水电高等专科学校南昌330029

在有色Petri网的状态空间中,有时一些状态具有相似的行为,这些状态可以用定义在状态空间上的一致的等价关系来表达,对每个等价状态类只研究它的一个代表状态的行为,这极大地减小了有色Petri网的状态空间。但是,通常对一个给定的等价关... 详细信息

在有色Petri网的状态空间中,有时一些状态具有相似的行为,这些状态可以用定义在状态空间上的一致的等价关系来表达,对每个等价状态类只研究它的一个代表状态的行为,这极大地减小了有色Petri网的状态空间。但是,通常对一个给定的等价关系是否为一致的验证都是通过用户的经验人工进行的,这不但容易产生错误,而且效率低下。该文依据普通状态图和等价类状态图的标记迁移系统关系,对状态空间一致性等价定义的计算机辅助验证做了深入的讨论,给出了相应的结果。

关键词：有色Petri网状态空间标记迁移系统等价类

来源：评论

学校读者我要写书评

暂无评论

一种新的安全通信协议安全性验证框架

引用

计算机应用研究 2009年第10期26卷 3888-3890,3917页

作者：谭渊徐中伟梅萌吴剑同济大学电子与信息工程学院上海201804

将CRA应用于安全通信协议的层次结构分析领域,采用LTS对协议的层次结构进行行为建模,并利用映像LTS描述协议行为的安全属性。采用接口技术对行为模型和属性模型进行组合约简,通过观察组合模型中错误状态是否可达来判定协议是否安全,为... 详细信息

将CRA应用于安全通信协议的层次结构分析领域,采用LTS对协议的层次结构进行行为建模,并利用映像LTS描述协议行为的安全属性。采用接口技术对行为模型和属性模型进行组合约简,通过观察组合模型中错误状态是否可达来判定协议是否安全,为安全通信协议的安全性验证提供了一种新的框架。最后基于该框架给出FSFB/2(fail safe field bus/2)协议的安全性验证,表明该框架的可用性。

关键词：安全通信协议安全性验证标记迁移系统组合可达分析

来源：评论

学校读者我要写书评

暂无评论

具有不确定需求的软件测试用例生成方法研究

引用

计算机工程与应用 2018年第20期54卷 35-41页

作者：王莹浙江理工大学理学院杭州310018

软件测试是软件开发重要的一部分,是保证软件质量,提高软件可靠性的重要途径。测试在需求分析阶段就开始介入,而在现实中很多需求是不确定的,在软件测试的过程中会面临许多不确定性的挑战。主要研究具有不确定需求的软件测试用例生成方... 详细信息

软件测试是软件开发重要的一部分,是保证软件质量,提高软件可靠性的重要途径。测试在需求分析阶段就开始介入,而在现实中很多需求是不确定的,在软件测试的过程中会面临许多不确定性的挑战。主要研究具有不确定需求的软件测试用例生成方法,利用基于标记迁移系统的Partial Models(部分模型)对不确定的需求进行建模,进而基于建立的模型生成有效的测试用例。针对模型中具有的不确定性引入概率,对不确定的部分进行概率表示,进一步基于标记迁移系统和Partial Models的特点提出测试用例生成方法。由于模型中具有不确定信息,由此生成的测试用例具有一定的概率,基于此对测试用例进行优先级排序。

关键词：软件测试不确定需求测试用例标记迁移系统部分模型(PartialModels) 概率表示

来源：评论

学校读者我要写书评

暂无评论

基于不确定需求的测试用例生成方法研究

基于不确定需求的测试用例生成方法研究

引用

作者：王莹浙江理工大学

学位级别：硕士

软件工程的第一步是需求分析,准确的分析需求对软件开发具有重要的意义。现实中,由于在需求的采集和细化阶段对系统的理解不全面,或者是相关领域环境的不确定,再者是语言表达的模糊性等都会使需求存在不确定性。因此针对不确定的需求构... 详细信息

软件工程的第一步是需求分析,准确的分析需求对软件开发具有重要的意义。现实中,由于在需求的采集和细化阶段对系统的理解不全面,或者是相关领域环境的不确定,再者是语言表达的模糊性等都会使需求存在不确定性。因此针对不确定的需求构建的模型会出现不确定的因素,且根据该模型生成的测试用例同样会存在不确定的可能。目前,不确定需求的研究受到大家广泛的关注。然而,对不确定需求的研究多集中在检测、管理不确定性和基于需求变更建立需求模型上,却很少有人研究如何基于不确定需求直接生成测试用例。本文主要研究如何基于软件的不确定需求为软件测试生成测试用例。研究一种典型的不确定需求,其蕴含“多种可能性”。本文的测试用例生成方法利用基于标记迁移系统的部分模型来描述不确定需求。然后,基于标记迁移系统和部分模型的特点,本文提出了一个测试用例自动生成算法。最后,根据与对应测试用例的不确定性相关的权值对测试用例进行优先级排序,以便为执行这些测试用例提供一个推荐建议。本文的贡献点如下:(1)提出一种针对不确定需求建模的方法。该方法是基于标记迁移系统的一种形式化建模方法,能够描述软件系统的状态变化和迁移路径,以便基于路径的测试用例生成。(2)给出一个测试用例自动生成算法。该算法的本质是一种基于路径的遍历算法,其目的在于从不确定需求的形式化模型中生成一组测试用例。由于通过形式化模型描述不确定性,导致测试用例也包含与不确定需求相关的信息,基于此对测试用例排序有助于生成的执行测试用例。(3)提出一个解决循环的机制。考虑到模型中存在循环的复杂性,提出一个解决机制以避免状态爆炸的问题。

关键词：不确定需求测试用例概率表示标记迁移系统部分模型优先级排序

来源：评论

学校读者我要写书评

暂无评论

CPS系统的时空UML模型建模方法研究

CPS系统的时空UML模型建模方法研究

引用

作者：刘子微华东师范大学

学位级别：硕士

信息物理系统(Cyber-Physical System, CPS)是继20世纪IT革命后,对国内外信息技术领域产生深远影响的一类重要系统。如何对CPS系统进行建模以及如何捕捉并描述系统的CPS特性是目前国内外研究的热点和难点。在对CPS系统进行设计时,首要... 详细信息

信息物理系统(Cyber-Physical System, CPS)是继20世纪IT革命后,对国内外信息技术领域产生深远影响的一类重要系统。如何对CPS系统进行建模以及如何捕捉并描述系统的CPS特性是目前国内外研究的热点和难点。在对CPS系统进行设计时,首要要求是要保证系统内各物理实体之间通讯的实时性,并且要求对物理实体的空间信息做记录处理以分析其空间特性。实时性的要求也反映了当前计算机科学和控制论结合研究中出现的一大难题：计算机科学的需求模型是用离散数学描述的,而控制论的模型是用微分方程和系统行为来描述的；控制对时间和空间的要求都十分敏感,而计算机则只关心具体功能的实现。这反映了控制论和计算机理论本质上的差异,如何将二者统一起来,亦即将连续系统和离散系统结合在一起也是CPS系统设计所面临的巨大挑战。这些要求决定了大多数现有研究都不能完全满足CPS系统的要求,因此需要提出一个全新的理论模型以解决这些重点难点问题。统一建模语言(Unified Modeling Language, UML)是一种面向对象的工业化建模语言。为增强UML语言的建模能力,UML在许多其他特定的专业领域又有不同的扩展概要文件(Profile),如针对实时嵌入式系统进行建模的MARTE概要文件(The UML Profile for Modeling and Analysis of Real-time and Embedded systems, MARTE)。MARTE作为UML的扩展概要文件,增强了UML针对实时嵌入式系统进行建模的能力。因此,对象管理组织(Object Management Group, OMG)采用了MARTE概要文件来取代原有的关于调度、性能和时间性质方面的UML概要文件。MARTE提出了一个详尽的、统一的时间结构模型,在该模型之中可以对连续时间和离散时间进行统一的建模。然而,MARTE缺少严格的形式化语法和语义说明,并且也没有提出将连续时间和离散时间统一的具体做法。这显然不能满足对实时性属性要求严格的CPS系统的设计需要。因此,本文在MARTE概要文件的基础上,结合混成自动机理论,提出一种新的UML状态图模型—时空UML状态图模型(Spatio-Temporal UML statechart, STUML statechart)。STUML状态图使用类型变量和类型表达式,其基本变量类型包括连续变量、离散变量和时钟变量,基本表达式类型有布尔表达式、微分表达式、时钟约束表达式和动作表达式。本文扩展了UML状态图中关于事件的定义。在STUML状态图中,我们将传统的事件定义扩展为CPS事件,扩展后的CPS事件增加了对事件发生点的地理位置信息的记录,以此来记录系统的空间信息。在此基础之上,本文给出了STUML状态图模型的形式化的语法和语义。该模型的形式化语法定义为一个十一元组,其中对警备条件、CPS事件、动作、活动、不变式等都给出了详细的形式化定义。STUML状态图模型的形式化语义包括安全语义和活性语义。STUML状态图的安全语义的定义基于标记迁移系统,而其活性语义则基于活性迁移系统给出。最后,在上述工作的基础上,以一个列车自动防护系统为例,对其进行建模和语义描述,具体说明了STUML状态图的用法和作用。

关键词： CPS系统 UML MARTE 混成自动机标记迁移系统列车自动防护系统

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：