重写逻辑

作品数:11被引量:10H指数:2
导出分析报告
相关领域:自动化与计算机技术更多>>
相关作者:戚正伟尹剑飞栾天骄蔡国永黄宁更多>>
相关机构:华东师范大学北京航空航天大学上海交通大学华南理工大学更多>>
相关期刊:《上海交通大学学报》《计算机学报》《计算机工程与应用》《计算机系统应用》更多>>
相关基金:国家重点基础研究发展计划国家自然科学基金国防科技技术预先研究基金国家高技术研究发展计划更多>>
-

检索结果分析

结果分析中...
条 记 录,以下是1-10
视图:
排序:
基于重写逻辑的PKMv3协议形式化建模与验证
《计算机应用与软件》2017年第11期270-277,共8页佘葭 张民 
国家自然科学基金青年基金项目(61502171)
IEEE802.16m标准在MAC安全子层定义了密钥管理PKMv3协议,用于认证和授权信息的传输以及密钥的交换。由于宽带无线网络具有易遭受攻击的特性,引入入侵者模型分析密钥管理协议的安全机制。利用一种基于重写逻辑的形式化建模语言Maude,实现...
关键词:IEEE802. 16m 标准 PKMv3 协议 密钥管理 重写逻辑 MAUDE 语言 形式化验证 
一种基于活性顺序图的运行时验证研究被引量:1
《计算机科学》2016年第8期137-141,164,共6页叶俊民 张坤 叶竹君 陈盼 陈曙 
国家科技支撑计划项目(2015BAK33B00);中央高校基本科研业务费专项资金科研项目(CCNU15GF003);教育部人文社会科学研究规划基金(15YJA880095)资助
运行时验证是一种轻量级的形式化验证方法,使用可视化的需求规约描述语言建模需求规约场景是运行时验证领域的研究热点。针对目前基于活性顺序图的运行时验证方法中容易产生冗余性质、二值语义的验证结果不准确、基于Maude工具引擎的重...
关键词:活性顺序图 线性时序逻辑 重写逻辑 运行时验证 
实时系统规范语言STeC的Maude重写系统被引量:2
《计算机工程》2013年第10期57-62,67,共7页栾天骄 陈仪香 王江涛 
国家"973"计划基金资助项目(2011CB302802);国家"863"计划基金资助项目(2011AA010101);国家自然科学基金资助项目(61021004)
信息物理融合系统的网络化、系统化和信息化等特性使得软件系统的复杂程度不断增加。为此,引入实时系统的规范语言STeC,用于刻画具有时空一致性要求的实时系统。对于STeC语言的自动逻辑推理问题,通过拓展Maude中的关系等式和重写规则,将...
关键词:实时系统 实时系统的规范语言 重写逻辑 形式化分析 时空一致性 操作语义 
面向服务架构软件实现前的可靠性评价方法
《计算机应用》2011年第9期2436-2439,2484,共5页吕堂祺 黄宁 贾晓光 王东 
国防"十一五"预研项目
为了在软件实现前评估其可靠性,针对基于面向服务架构(SOA)设计的软件提出了一种可靠性评价方法:用OWL-S描述软件的需求和设计信息,利用Maude为OWL-S过程模型的控制结构定义形式化语义,使用分布函数构建软件的操作剖面,在Maude中增加软...
关键词:面向服务架构 OWL—S模型 重写逻辑 操作剖面 可靠性评价 
OWL-S模型转化为重写逻辑模型的方法被引量:1
《计算机应用》2011年第6期1491-1494,共4页沈雅芬 黄宁 彭永义 
国防"十一五"预研项目
OWL-S模型在基于服务的软件设计中具有重要作用,但由于其非完全形式化的模型,不能直接对其进行形式化分析与验证。基于OWL-S模型的重写逻辑语义框架,通过对数据类型、表达式、控制结构与Process的转换,设计并实现了OWL-S模型到重写逻辑...
关键词:软件可靠性 Web服务本体 重写逻辑 模型转化 形式化验证 
Petri网的重写逻辑模型及其属性验证被引量:1
《桂林电子科技大学学报》2011年第3期208-212,共5页聂锡宁 蔡国永 
国家自然科学基金(61063039)
为了对大规模或复杂结构的系统进行规格,人们在经典的库所/迁移Petri网基础上加入层次、时间等来扩展它。为此,提出使用重写逻辑表达Petri网的新方法来探索对Petri网的替代。通过把异步并发系统的Petri网图形表达转化为重写逻辑理论,可...
关键词:PETRI网 重写逻辑 验证 形式化方法 MAUDE 
电子机构基于角色的访问控制模型
《计算机系统应用》2009年第9期50-53,共4页李红霞 蔡国永 
根据电子机构的基本概念、结构,提出了电子机构基于角色的访问控制模型,并与传统的基于角色的访问控制模型进行比较。采用重写逻辑Maude工具中面向对象的建模方法对该模型进行建模,并将模型应用到医院管理信息系统中。测试结果表明该模...
关键词:电子机构 重写逻辑 访问控制 
活性细胞膜计算的可执行性描述与实现被引量:1
《上海交通大学学报》2008年第10期1635-1639,共5页张民 戚正伟 董笑菊 
国家重点基础研究发展规划(973)项目(2003CB317005);国家自然科学基金资助项目(60573002;60703033);高等学校博士学科点基金资助项目(20010248033)
基于重写逻辑理论,利用Maude语言对活性细胞膜计算模型进行可执行性描述,实现了借助于计算机自动验证计算模型的正确性、完整性,以及辅助研究模型的性质等功能.通过采用Maude语言对活性细胞膜计算中6条基本规则的定义,给出了模型通用的...
关键词:活性细胞膜计算 重写逻辑 可满足性问题 
基于重写逻辑的UML模型一致性检查方法被引量:1
《计算机工程》2006年第8期23-25,31,共4页尹剑飞 郭荷清 欧毓毅 
国家"973"计划基金资助项目(G20000263)
在模型驱动开发的场景下,保证UML模型的一致性具有重要意义,但目前大多数UML/MDA工具仅提供了有限支持。该文提出了一种基于代数重写逻辑的UML模型一致性检查的方法。首先定义了基于两级代数规范的实施构架以分别检查UML模型的设计时和...
关键词:模型检查 重写逻辑 代数规范 UML 
模型转换的重写逻辑构架研究被引量:2
《计算机工程与应用》2006年第2期14-16,19,共4页尹剑飞 王学斌 
国家973重点基础研究发展规划资助项目(编号:G20000263)
规则式的模型转换技术在模型驱动构架的模型转换实施中占有重要地位,但目前诸实施对于转换规则的定义存在多种解释、转换的协调方面、终止性和一致性等数学属性缺乏支持。该文提出一种Maude重写逻辑基础的构架(RLBA)以实施模型转换,通...
关键词:模型转换 重写逻辑 可执行代数规范 模型驱动构架 
检索报告 对象比较 聚类工具 使用帮助 返回顶部