检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

基于重写逻辑的UML模型一致性检查方法

计算机工程 2006年第8期32卷 23-25,31页

作者：尹剑飞郭荷清欧毓毅华南理工大学计算机科学与工程学院广州510641

在模型驱动开发的场景下,保证UML模型的一致性具有重要意义,但目前大多数UML/MDA工具仅提供了有限支持。该文提出了一种基于代数重写逻辑的UML模型一致性检查的方法。首先定义了基于两级代数规范的实施构架以分别检查UML模型的设计时和... 详细信息

在模型驱动开发的场景下,保证UML模型的一致性具有重要意义,但目前大多数UML/MDA工具仅提供了有限支持。该文提出了一种基于代数重写逻辑的UML模型一致性检查的方法。首先定义了基于两级代数规范的实施构架以分别检查UML模型的设计时和运行时语义一致性,其次定义了检查包括类图、状态机图和顺序图在内的多图一致性的重写规则。该方法为保持面向可执行的UML模型的一致性提供了有效支持。

关键词：模型检查重写逻辑代数规范 UML

在线全文

学校读者我要写书评

暂无评论

OWL-S模型转化为重写逻辑模型的方法

计算机应用 2011年第6期31卷 1491-1494页

作者：沈雅芬黄宁彭永义北京航空航天大学可靠性与系统工程学院北京100191 北京航空航天大学计算机学院北京100191

OWL-S模型在基于服务的软件设计中具有重要作用,但由于其非完全形式化的模型,不能直接对其进行形式化分析与验证。基于OWL-S模型的重写逻辑语义框架,通过对数据类型、表达式、控制结构与Process的转换,设计并实现了OWL-S模型到重写逻辑... 详细信息

OWL-S模型在基于服务的软件设计中具有重要作用,但由于其非完全形式化的模型,不能直接对其进行形式化分析与验证。基于OWL-S模型的重写逻辑语义框架,通过对数据类型、表达式、控制结构与Process的转换,设计并实现了OWL-S模型到重写逻辑模型的自动转化工具,为能够在软件实现前为设计模型的形式化分析与验证,以及可靠性分析提供基础。

关键词：软件可靠性 Web服务本体重写逻辑模型转化形式化验证

在线全文

学校读者我要写书评

暂无评论

模型转换的重写逻辑构架研究

计算机工程与应用 2006年第2期42卷 14-16,19页

作者：尹剑飞王学斌深圳大学信息工程学院深圳518060 国防科学技术大学计算机学院网络与信息安全研究所长沙410073

规则式的模型转换技术在模型驱动构架的模型转换实施中占有重要地位,但目前诸实施对于转换规则的定义存在多种解释、转换的协调方面、终止性和一致性等数学属性缺乏支持。该文提出一种Maude重写逻辑基础的构架(RLBA)以实施模型转换,通... 详细信息

规则式的模型转换技术在模型驱动构架的模型转换实施中占有重要地位,但目前诸实施对于转换规则的定义存在多种解释、转换的协调方面、终止性和一致性等数学属性缺乏支持。该文提出一种Maude重写逻辑基础的构架(RLBA)以实施模型转换,通过产生式规范、多方法风格的重写规则集设计、OC(对象配置)和OM(对象消息)重写规则分类等技术并结合模型检查工具,为自动产生元模型和模型的面向对象可执行代数规范、转换规则的严格形式化定义、转换协调方面的刻画、终止性和一致性等的验证提供支持。

关键词：模型转换重写逻辑可执行代数规范模型驱动构架

在线全文

学校读者我要写书评

暂无评论

基于重写逻辑的SN P系统模型检测

基于重写逻辑的SN P系统模型检测

作者：张民上海交通大学

学位级别：硕士

随着计算机科学与其他学科之间的相互渗透和影响,科学家们根据不同原理提出了不同的计算模型。细胞膜计算是一种基于生物细胞膜结构和功能的新型计算模型,近年来得到广泛的研究。SN P系统(Spiking Neural P Systems)是对类神经细胞膜计... 详细信息

随着计算机科学与其他学科之间的相互渗透和影响,科学家们根据不同原理提出了不同的计算模型。细胞膜计算是一种基于生物细胞膜结构和功能的新型计算模型,近年来得到广泛的研究。SN P系统(Spiking Neural P Systems)是对类神经细胞膜计算(Neural-like P Systems)的扩展。与其他细胞膜计算的不同的是,它在计算中引入了时间的概念,计算由一个全局时钟驱动。SN P系统已被证明具有与图灵机相同的计算能力。然而随着研究的深入,模型的设计越来越复杂,如何有效地验证模型的正确性和研究SN P系统的性质成为该领域当前一个迫切需要解决的问题。模型检测作为一种研究和验证系统性质的方法,可以有效地帮助我们解决这一问题。目前用于模型检测的工具主要有SPIN、Maude等。Maude是一种基于重写逻辑的形式化描述语言,由Maude解释器解释执行,主要用于模型检测和逻辑推理。[0] 本文的主要工作是:通过扩展Maude中的重写规则语义,利用代数方法定义了SN P系统中计算规则的操作语义,并借助于Maude中面向对象的形式化描述,给出了SN P系统通用的描述方法,把SN P系统转化成为可执行的形式化描述。这种形式化的描述可以被Maude解释器解释运行,从而自动推导系统的计算结果、验证系统的某些性质等。最后,本文将这一形式化描述方法应用于具体的SN P系统模型并给出了验证的结果,证明了模型检测的可行性与正确性。本文的主要贡献是:将模型检测应用于SN P系统;利用Maude语言定义了SN P系统中计算规则的操作语义;给出了SN P系统在Maude下通用的形式化描述方法;达到了通过计算机辅助验证SN P系统正确性与完整性[0]的目的。

关键词：细胞膜计算 SN P系统重写逻辑模型检测 Maude

基于重写逻辑的PKMv3协议形式化建模与验证

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

计算机应用与软件 2017年第11期34卷 270-277页

作者：佘葭张民华东师范大学计算机科学与软件工程学院上海200062

IEEE802.16m标准在MAC安全子层定义了密钥管理PKMv3协议,用于认证和授权信息的传输以及密钥的交换。由于宽带无线网络具有易遭受攻击的特性,引入入侵者模型分析密钥管理协议的安全机制。利用一种基于重写逻辑的形式化建模语言Maude,实现... 详细信息

IEEE802.16m标准在MAC安全子层定义了密钥管理PKMv3协议,用于认证和授权信息的传输以及密钥的交换。由于宽带无线网络具有易遭受攻击的特性,引入入侵者模型分析密钥管理协议的安全机制。利用一种基于重写逻辑的形式化建模语言Maude,实现对PKMv3网络环境中的通信主体以及系统状态的建模,并利用其自带的模型检测工具验证协议的安全特性。验证结果表明,PKMv3协议能保证密钥的机密性以及认证的可靠性,但仍有可能遭遇到中间人攻击破坏消息传输的完整性。

关键词： IEEE802. 16m 标准 PKMv3 协议密钥管理重写逻辑 Maude 语言形式化验证

在线全文

学校读者我要写书评

暂无评论

Petri网的重写逻辑模型及其属性验证

桂林电子科技大学学报 2011年第3期31卷 208-212页

作者：聂锡宁蔡国永桂林电子科技大学计算机科学与工程学院广西桂林541004

为了对大规模或复杂结构的系统进行规格,人们在经典的库所/迁移Petri网基础上加入层次、时间等来扩展它。为此,提出使用重写逻辑表达Petri网的新方法来探索对Petri网的替代。通过把异步并发系统的Petri网图形表达转化为重写逻辑理论,可... 详细信息

为了对大规模或复杂结构的系统进行规格,人们在经典的库所/迁移Petri网基础上加入层次、时间等来扩展它。为此,提出使用重写逻辑表达Petri网的新方法来探索对Petri网的替代。通过把异步并发系统的Petri网图形表达转化为重写逻辑理论,可以更容易和更直接地验证原系统的安全性、活性和可达性等行为属性,而不需要建立标识图或搜索网络不变量。以银行家问题为例,展示模型转化过程,并检测了该模型的无死锁性。结果表明,库所/变迁Petri网可以等效转化为重写规则代数组合的重写逻辑,并能在重写逻辑软件Maude中验证保留的基本属性。

关键词： Petri网重写逻辑验证形式化方法 Maude

在线全文

学校读者我要写书评

暂无评论

活性细胞膜计算的可执行性描述与实现

上海交通大学学报 2008年第10期42卷 1635-1639页

作者：张民戚正伟董笑菊上海交通大学电子信息与电气工程学院上海200240 上海交通大学软件学院上海200240

基于重写逻辑理论,利用Maude语言对活性细胞膜计算模型进行可执行性描述,实现了借助于计算机自动验证计算模型的正确性、完整性,以及辅助研究模型的性质等功能.通过采用Maude语言对活性细胞膜计算中6条基本规则的定义,给出了模型通用的... 详细信息

基于重写逻辑理论,利用Maude语言对活性细胞膜计算模型进行可执行性描述,实现了借助于计算机自动验证计算模型的正确性、完整性,以及辅助研究模型的性质等功能.通过采用Maude语言对活性细胞膜计算中6条基本规则的定义,给出了模型通用的描述方法.利用该方法描述与验证了可满足性问题在活性细胞膜计算中的模型.通过对计算结果的分析,说明了方法的可行性与正确性.

关键词：活性细胞膜计算重写逻辑可满足性问题

在线全文

学校读者我要写书评

暂无评论

面向服务架构软件实现前的可靠性评价方法

计算机应用 2011年第9期31卷 2436-2439,2484页

作者：吕堂祺黄宁贾晓光王东北京航空航天大学可靠性与系统工程学院北京100191 北京航空航天大学计算机学院北京100191

为了在软件实现前评估其可靠性,针对基于面向服务架构(SOA)设计的软件提出了一种可靠性评价方法:用OWL-S描述软件的需求和设计信息,利用Maude为OWL-S过程模型的控制结构定义形式化语义,使用分布函数构建软件的操作剖面,在Maude中增加软... 详细信息

为了在软件实现前评估其可靠性,针对基于面向服务架构(SOA)设计的软件提出了一种可靠性评价方法:用OWL-S描述软件的需求和设计信息,利用Maude为OWL-S过程模型的控制结构定义形式化语义,使用分布函数构建软件的操作剖面,在Maude中增加软件的操作剖面信息和体系结构信息如何参与可靠度计算的描述,在Maude系统的支持下,通过重写得到软件的可靠度,并基于此方法设计开发了一个软件可靠性预计工具——SRPT。所提出的软件可靠性评价方法综合考虑了数据流、控制流、构件和软件操作剖面信息以及体系结构信息对软件可靠性的影响,能够在软件实现前根据软件设计预测其可靠度,为软件的开发设计提供了工程指导。

关键词：面向服务架构 OWL—S模型重写逻辑操作剖面可靠性评价

在线全文

学校读者我要写书评

暂无评论

一种基于活性顺序图的运行时验证研究

计算机科学 2016年第8期43卷 137-141,164页

作者：叶俊民张坤叶竹君陈盼陈曙华中师范大学计算机学院武汉430079 华中师范大学国家物理学人才培养基地武汉430079

运行时验证是一种轻量级的形式化验证方法,使用可视化的需求规约描述语言建模需求规约场景是运行时验证领域的研究热点。针对目前基于活性顺序图的运行时验证方法中容易产生冗余性质、二值语义的验证结果不准确、基于Maude工具引擎的重... 详细信息

运行时验证是一种轻量级的形式化验证方法,使用可视化的需求规约描述语言建模需求规约场景是运行时验证领域的研究热点。针对目前基于活性顺序图的运行时验证方法中容易产生冗余性质、二值语义的验证结果不准确、基于Maude工具引擎的重写逻辑验证算法效率较低等问题,提出一种基于活性顺序图的运行时验证的改进方法,以支持现有的运行时验证技术。实验表明,改进方法验证结果准确,且验证过程开销较小。

关键词：活性顺序图线性时序逻辑重写逻辑运行时验证