构件式体系结构模型映射的形式化语义 被引量：8

1

作者 侯金奎 万建成 +1 位作者 杨潇 王海洋 《计算机研究与发展》 EI CSCD 北大核心 2009年第2期310-320,共11页

语义一致性是模型驱动开发中模型转换正确性的一个重要标准,但目前模型转换中语义特性保持的定义、描述和验证仍是一个尚未解决的难题.基于软件体系结构,利用范畴理论和代数规范形式化描述体系结构模型及其间的映射关系,使之具有精确的... 语义一致性是模型驱动开发中模型转换正确性的一个重要标准,但目前模型转换中语义特性保持的定义、描述和验证仍是一个尚未解决的难题.基于软件体系结构,利用范畴理论和代数规范形式化描述体系结构模型及其间的映射关系,使之具有精确的语义.体系结构模型的形式化语义用类型范畴图表来表示,态射合成被用来追踪构件模型之间的关联和映射,不同层次模型间的映射关系用态射和函子来形式化描述.以此为基础,进一步分析了模型转换应保持的语义特性.范畴理论支持图形化建模,可以使模型中的构件关系以及结构特征可视化,有利于对模型转换的理解和追踪.应用研究表明,该描述框架很好地把握了模型驱动开发的实质、过程和要求,为模型转换和模型驱动开发提供了新的认知、设计和语义计算的指导架构. 展开更多

关键词 模型驱动开发 模型映射 形式化语义 软件体系结构 构件模型

在线阅读 下载PDF 职称材料

以体系结构为中心的构件模型的形式化语义 被引量：10

2

作者 楚旺 钱德沛 《软件学报》 EI CSCD 北大核心 2006年第6期1287-1297,共11页

目前的软件开发方法采用非结构化和非形式化方式建立构件模型,构件之间的关系是隐含的,并且缺乏严格的语义,不能有效地支持自顶向下的构件重用.利用范畴论定义构件之间的关系,使得构件之间的关系以及关系组合具有严格的语义.态射合成被... 目前的软件开发方法采用非结构化和非形式化方式建立构件模型,构件之间的关系是隐含的,并且缺乏严格的语义,不能有效地支持自顶向下的构件重用.利用范畴论定义构件之间的关系,使得构件之间的关系以及关系组合具有严格的语义.态射合成被用来跟踪不同抽象层次的构件之间的关系,利用体系结构设计模式精确地定义构件的组合关系和应满足的条件.范畴论支持图形化建模,可以使模型中的构件关系以及结构特征可视化,有利于模型的理解、跟踪和重用.形式化的构件建模方法适用于以重用为目标的软件开发. 展开更多

关键词 体系结构 构件模型 构件可跟踪性 形式化语义 软件重用

在线阅读 下载PDF 职称材料

UML 2.0的形式化语义研究 被引量：4

3

作者 张广泉 戎玫 黄正宝 《南京邮电大学学报（自然科学版）》 EI 2007年第3期39-43,共5页

由于UML2.0动态视图缺乏精确的语义,难以对它所表示的系统进行分析和验证。基于此,在描述UML2.0顺序图和状态图语法和语法约束的基础上,采用可执行的线性时序逻辑语言XYZ/E定义其形式化语义,这样不仅便于UML2.0顺序图和状态图之间的模... 由于UML2.0动态视图缺乏精确的语义,难以对它所表示的系统进行分析和验证。基于此,在描述UML2.0顺序图和状态图语法和语法约束的基础上,采用可执行的线性时序逻辑语言XYZ/E定义其形式化语义,这样不仅便于UML2.0顺序图和状态图之间的模型转换,也为使用UML和形式化方法相结合描述软件体系结构的交互行为奠定了基础。 展开更多

关键词 线性时序逻辑 形式化语义 UML2.0 顺序图 状态图 XYZ/E

在线阅读 下载PDF 职称材料

一种UML2的交互的形式化语义 被引量：2

4

作者 古思山 蔡树彬 李师贤 《计算机科学与探索》 CSCD 2012年第7期631-643,共13页

UML2(unified modeling language2.x)的规范为其交互定义了一种基于事件发生轨迹的语义,弥补了之前版本在语义上的欠缺。但是此语义是用自然语言(英语)描述的,不够精确、不一致,并且很多细节解释得不够清楚和完备。利用集合论以组合定... UML2(unified modeling language2.x)的规范为其交互定义了一种基于事件发生轨迹的语义,弥补了之前版本在语义上的欠缺。但是此语义是用自然语言(英语)描述的,不够精确、不一致,并且很多细节解释得不够清楚和完备。利用集合论以组合定义的方式形式化语义,并且证明了形式化后交互的语义为拟序集,此拟序集的线性化恰好就是规范所定义的轨迹集。此形式化语义可以作为UML2交互规范的很好的补充,不但有助于UML2交互的理解,还为UML2交互的应用和研究奠定了坚实的理论基础。 展开更多

关键词 交互 形式化语义 组合定义 线性化

在线阅读 下载PDF 职称材料

时间相关密码协议逻辑及其形式化语义 被引量：1

5

作者 雷新锋 刘军 肖军模 《软件学报》 EI CSCD 北大核心 2011年第3期534-557,共24页

在密码协议中,主体的认知与信仰状态是随时间推移而不断变化的.为了在协议分析中体现这种动态性,提出一种时间相关密码协议逻辑.该逻辑基于谓词模态逻辑,通过在谓词及模态词中引入时间参数以体现时间因素,使得逻辑可表达各个主体在协议... 在密码协议中,主体的认知与信仰状态是随时间推移而不断变化的.为了在协议分析中体现这种动态性,提出一种时间相关密码协议逻辑.该逻辑基于谓词模态逻辑,通过在谓词及模态词中引入时间参数以体现时间因素,使得逻辑可表达各个主体在协议不同时间点的行为、知识及信仰.给出该逻辑的形式化语义,在避免逻辑语言二义性的同时保证了逻辑的可靠性.该语义基于Kripke结构,将可能世界建立在主体局部世界与时间局部世界的基础上,使得任一可能世界能够反映协议的一个可能的全过程.该逻辑为密码协议,特别是时间相关密码协议提供了灵活的分析方法,增强了基于逻辑方法的协议分析能力. 展开更多

关键词 密码协议 时间相关 谓词模态逻辑 形式化语义

在线阅读 下载PDF 职称材料

支持MDD的体系结构模型的形式化语义 被引量：1

6

作者 侯金奎 马军 《中山大学学报（自然科学版）》 CAS CSCD 北大核心 2008年第6期109-113,119,共6页

为解决模型驱动开发中模型映射关系的定义和模型转换的正确性验证等方面存在的问题,利用范畴理论形式化描述软件体系结构模型及其间的关系,使之具有严格的语义。态射合成被用来追踪构件模型之间的关联和映射关系,不同抽象层次的体系结... 为解决模型驱动开发中模型映射关系的定义和模型转换的正确性验证等方面存在的问题,利用范畴理论形式化描述软件体系结构模型及其间的关系,使之具有严格的语义。态射合成被用来追踪构件模型之间的关联和映射关系,不同抽象层次的体系结构模型之间的一致性由函子来维持。范畴理论支持图形化建模,可以使模型中的构件关系以及结构特征可视化,有利于对模型转换的理解和追踪。应用研究表明,该方法不仅可为验证模型之间映射规则的正确性提供依据,还能为模型转换的具体实现提供理论指导。 展开更多

关键词 计算机软件 模型驱动开发 模型映射 软件体系结构 形式化语义

在线阅读 下载PDF 职称材料

协同系统体系结构模型的形式化语义 被引量：1

7

作者 侯金奎 《电子学报》 EI CAS CSCD 北大核心 2009年第B04期106-111,105,共7页

针对模型驱动的协同应用系统开发,将范畴理论、代数规范和进程代数相结合,为软件体系结构模型提出了一种新的语义描述方法.该方法在构件规约描述的基础上,用态射表示构件之间的关系,态射类型蕴含了构件关系的不同语义,从而用类型范畴图... 针对模型驱动的协同应用系统开发,将范畴理论、代数规范和进程代数相结合,为软件体系结构模型提出了一种新的语义描述方法.该方法在构件规约描述的基础上,用态射表示构件之间的关系,态射类型蕴含了构件关系的不同语义,从而用类型范畴图表来描述软件体系结构模型,用函子描述体系结构模型之间的映射关系.体系结构模型的形式化描述可用于判断一个转换是否满足某些特性或约束.以一个协同编著系统为例说明了该方法的应用. 展开更多

关键词 模型驱动开发 协同系统 软件体系结构 形式化语义

在线阅读 下载PDF 职称材料

支持冲突检测的P3P形式化语义研究

8

作者 孙艺 黄志球 +1 位作者 沈国华 柯昌博 《计算机科学与探索》 CSCD 2013年第10期905-915,共11页

隐私偏好平台(platform for privacy preferences,P3P)是现今世界上广泛使用的隐私策略语言之一,服务提供者通过P3P隐私策略来告知用户如何处理隐私信息。针对P3P隐私策略缺少形式化语义而难以被精确表达的问题,分析了P3P隐私策略对形... 隐私偏好平台(platform for privacy preferences,P3P)是现今世界上广泛使用的隐私策略语言之一,服务提供者通过P3P隐私策略来告知用户如何处理隐私信息。针对P3P隐私策略缺少形式化语义而难以被精确表达的问题,分析了P3P隐私策略对形式化语义的需求以及P3P隐私策略中存在的语义冲突,提出了一种支持冲突检测的data-recipient结构的P3P形式化语义,并用OWL(Web ontology language)本体对该语义进行了描述,阐述了语义冲突的检测方法,并通过实验验证了该方法的可行性。 展开更多

关键词 隐私偏好平台（P3P） 隐私策略 形式化语义 本体 冲突检测

在线阅读 下载PDF 职称材料

隐标识身份认证方法及其形式化语义分析

9

作者 贺前华 江瑾 黄翰陞 《计算机工程》 CAS CSCD 北大核心 2008年第12期147-148,151,共3页

针对用户身份标识在身份认证机制中的安全问题,提出一种隐藏身份标识的身分认证方案,用户毋需提交身份标识即可与服务器实现身份认证,并采用形式化的SVO逻辑语言分析该协议。SVO逻辑体系下的实验表明,该协议达到了预期的设计目标。

关键词 隐标识身份认证方法 SVO逻辑 形式化语义分析

在线阅读 下载PDF 职称材料

Verilog语言形式化语义研究

10

作者 李勇坚 孙永强 何积丰 《软件学报》 EI CSCD 北大核心 2001年第10期1573-1580,共8页

在连续离散混合时间模型中考虑 Verilog的语义行为 ,将混合模型中的一个区间作为 Verilog程序一次运行过程的指称 .提出了一种扩展的 ITL来描述这种混合区间 ,从而给出 Verilog的形式语义 .这种语义定义不仅考虑到了各种语言成分的最终... 在连续离散混合时间模型中考虑 Verilog的语义行为 ,将混合模型中的一个区间作为 Verilog程序一次运行过程的指称 .提出了一种扩展的 ITL来描述这种混合区间 ,从而给出 Verilog的形式语义 .这种语义定义不仅考虑到了各种语言成分的最终执行结果 。 展开更多

关键词 VERILOG语言 形式化语义 硬件描述语言

在线阅读 下载PDF 职称材料

基于Agent的分布式模型形式化语义描述

11

作者 侯金奎 王磊 《计算机应用》 CSCD 北大核心 2013年第12期3423-3427,3440,共6页

为解决分布式系统构建过程中系统组合和语义验证等方面的问题,基于范畴理论和进程代数,为基于Agent的分布式系统模型提出了一种形式化的语义描述框架。范畴图表用于描述整个系统的结构模型,态射用来表示系统各组成部分之间的交互和协作... 为解决分布式系统构建过程中系统组合和语义验证等方面的问题,基于范畴理论和进程代数,为基于Agent的分布式系统模型提出了一种形式化的语义描述框架。范畴图表用于描述整个系统的结构模型,态射用来表示系统各组成部分之间的交互和协作机制。在此基础上,对Agent规范的描述、组合、精化以及迁移过程中的语义保持问题进行了探讨。应用研究表明,该框架适用于分布式系统模型的描述和构建,有助于分析系统分解和组合的正确性。 展开更多

关键词 分布式系统 系统组合 形式化语义 范畴理论 AGENT

在线阅读 下载PDF 职称材料

基于Object-Z的XPath形式化语义 被引量：1

12

作者 杨红丽 郝克刚 韩俊刚 《计算机科学》 CSCD 北大核心 2004年第2期175-180,共6页

本文描述了XPath语言的形式化语义。一个统一的面向对象的语义视角用于建模所有XPath语言构造。语义的表示采用形式化规范语言Object-Z的符号系统。这种高度结构化的语义模型具有简洁、可组合性和可复用性的特点。

关键词 XPath语言 形式化语义 OBJECT-Z 面向对象 数据类型 程序设计语言

在线阅读 下载PDF 职称材料

XQuery语言的形式化语义

13

作者 杨红丽 韩俊刚 郝克刚 《计算机科学》 CSCD 北大核心 2004年第3期15-18,27,共5页

XQuery语言用于查询XML文档。目前,该语言规范还是W3C的工作草稿。语言的形式化语义有助于语言的标准化,本文通过重用XML家族语言通用语义构件的方法,形式化建模XQuery语言的语义,语义的描述采用Object-Z规范语言。这种面向对象的语义... XQuery语言用于查询XML文档。目前,该语言规范还是W3C的工作草稿。语言的形式化语义有助于语言的标准化,本文通过重用XML家族语言通用语义构件的方法,形式化建模XQuery语言的语义,语义的描述采用Object-Z规范语言。这种面向对象的语义描述不仅具有简洁性、可扩展性和可组合性.而且有助于规范之间的一致性和协调性。 展开更多

关键词 XQUERY语言 形式化语义 面向对象 XML语言 应用程序 标准化

在线阅读 下载PDF 职称材料

信任本体的形式化语义研究 被引量：2

14

作者 王海艳 谢武锋 《武汉大学学报（理学版）》 CAS CSCD 北大核心 2011年第5期369-374,共6页

针对现有的信任模型缺少信任相关概念属性在数理上的定义以及严格可靠的信任语义推理和统一的形式化抽象模型的问题,本文提出形式化动态信任本体的概念,结合本体在语义层次的形式化描述方法,对实体信任、行为信任和区域信任进行本体化,... 针对现有的信任模型缺少信任相关概念属性在数理上的定义以及严格可靠的信任语义推理和统一的形式化抽象模型的问题,本文提出形式化动态信任本体的概念,结合本体在语义层次的形式化描述方法,对实体信任、行为信任和区域信任进行本体化,并对三种信任本体进行形式化语义演绎和推理.给出了信任相关属性的形式化理论分析,并通过典型的激发场景实例,有效地验证了信任本体化理论. 展开更多

关键词 信任本体 形式化语义 情景演算

原文传递

UML的形式化描述语义 被引量：6

15

作者 单黎君 朱鸿 《计算机工程与科学》 CSCD 北大核心 2010年第3期96-103,共8页

本文提出了一种新的定义UML形式化语义的方法。我们将建模语言的语义区分为描述语义和功能语义两个方面。描述语义定义哪些系统满足模型,功能语义定义模型中的基本概念。本文用一阶逻辑定义了UML的类图、交互图和状态图的描述语义,并介... 本文提出了一种新的定义UML形式化语义的方法。我们将建模语言的语义区分为描述语义和功能语义两个方面。描述语义定义哪些系统满足模型,功能语义定义模型中的基本概念。本文用一阶逻辑定义了UML的类图、交互图和状态图的描述语义,并介绍我们实现的将UML模型转换成逻辑系统的软件工具LAMBDES,该工具集成了定理证明器SPASS,可以对模型进行自动推理。我们成功地将此方法和工具应用于模型的一致性检查。 展开更多

关键词 建模语言 形式化语义 UML 一阶逻辑 一致性检查

在线阅读 下载PDF 职称材料

基于构件的服务模型形式化语义描述

16

作者 侯金奎 王磊 张奎廷 《华中科技大学学报（自然科学版）》 EI CAS CSCD 北大核心 2013年第S2期1-5,共5页

为解决服务系统描述和构建过程中服务的组合和验证等方面的问题,以范畴理论为基础,引入进程代数,为服务系统的架构模型提出了一种形式化的语义描述方法.整个服务结构模型通过由服务标志和标志态射构成的范畴图表来描述,态射用来表示服... 为解决服务系统描述和构建过程中服务的组合和验证等方面的问题,以范畴理论为基础,引入进程代数,为服务系统的架构模型提出了一种形式化的语义描述方法.整个服务结构模型通过由服务标志和标志态射构成的范畴图表来描述,态射用来表示服务规范之间的关系,余极限用来描述服务的层次组合.以此为基础,进一步从服务端口、结构和行为等方面对服务的组合、分解以及精化过程所中应保持的语义特性进行了分析.实例研究表明:该框架不仅能在抽象层次上支持服务系统的建模和分析,而且还可通过映射抽象模型到实现技术来支持服务组合,可以很好地分析需求分解和服务组合的正确性,可用于指导服务系统的描述和构建. 展开更多

关键词 服务系统 服务组合 形式化语义 体系架构模型 范畴理论

原文传递

句法和语义的对应——语义形式化的基石 被引量：3

17

作者 林胜强 邹崇理 《湖北大学学报（哲学社会科学版）》 CSSCI 北大核心 2016年第1期55-61,161,共7页

在我国的语言学界和计算语言学界,缺乏语义分析的形式化已成为中文信息处理的瓶颈问题。要使语义分析形式化,需要建立句法和语义对应的原则,这样能够把句法的可计算性延伸到语义那里。此外,从哲学角度思考,句法和语义的对应显示出一些... 在我国的语言学界和计算语言学界,缺乏语义分析的形式化已成为中文信息处理的瓶颈问题。要使语义分析形式化,需要建立句法和语义对应的原则,这样能够把句法的可计算性延伸到语义那里。此外,从哲学角度思考,句法和语义的对应显示出一些差异现象。这种"差异"的根源之一在于自然语言中存在的非连续现象。在自然语言某些非连续现象那里,"特异"的语义成分对形成整体的语义来说是非组合的,这就是句法和语义对应的"盲区",也是语义形式化需要关注的地方。 展开更多

关键词 句法 语义 语义形式化 自然语言

在线阅读 下载PDF 职称材料

基于K Framework的向量化机器学习指令语义形式化

18

作者 黄厚华 刘嘉祥 施晓牧 《软件学报》 EI CSCD 北大核心 2023年第8期3853-3869,共17页

ARM针对ARMv8.1-M微处理器架构推出基于M-Profile向量化扩展方案的技术,并命名为ARM Helium,声明能为ARM Cortex-M处理器提升达15倍的机器学习性能.随着物联网的高速发展,微处理器指令执行正确性尤为重要.指令集的官方手册作为芯片模拟... ARM针对ARMv8.1-M微处理器架构推出基于M-Profile向量化扩展方案的技术,并命名为ARM Helium,声明能为ARM Cortex-M处理器提升达15倍的机器学习性能.随着物联网的高速发展,微处理器指令执行正确性尤为重要.指令集的官方手册作为芯片模拟程序,片上应用程序开发的依据,是程序正确性基本保障.主要介绍利用可执行语义框架K Framework对ARMv8.1-M官方参考手册中向量化机器学习指令的语义正确性研究.基于ARMv8.1-M的官方参考手册自动提取指令集中描述向量化机器学习指令执行过程的伪代码,并将其转换为形式化语义转换规则.通过K Framework提供的可执行框架利用测试用例,验证机器学习指令算数运算执行的正确性. 展开更多

关键词 ARMv8.1-M架构 向量化指令 机器学习 K Framework 形式化语义

在线阅读 下载PDF 职称材料

基于语义形式化的XBRL链接库优化

19

作者 张颖敏 《财会月刊（中）》 北大核心 2015年第2Z期53-57,共5页

XBRL链接库用于表示XBRL财务元素之间的关系,具有可选性。本文探讨添加不同链接库形式化表示后的系统推理的效率问题,并通过对个别利润表实例证明该优化方法是有效的,能降低形式化表达的规则数,提高逻辑推理的效率。

关键词 XBRL XBRL链接库 元数据 语义形式化

在线阅读 下载PDF 职称材料

形式语义描述方法研究进展与评价 被引量：4

20

作者 张迎周 张卫丰 钱俊彦 《南京邮电大学学报（自然科学版）》 EI 2006年第6期86-94,共9页

程序设计语言形式语义描述技术在1990年代进入新一轮发展高潮,它对程序设计语言的设计和标准化,编译程序的设计和优化,程序推理,以及安全协议形式化描述、分析验证与设计等都有着重要的意义。但不同于成熟统一的形式化语法描述技术,语... 程序设计语言形式语义描述技术在1990年代进入新一轮发展高潮,它对程序设计语言的设计和标准化,编译程序的设计和优化,程序推理,以及安全协议形式化描述、分析验证与设计等都有着重要的意义。但不同于成熟统一的形式化语法描述技术,语义的形式描述技术尚处于蓬勃发展和多种技术并存时期。首先回顾形式语义描述方法的研究发展史;然后通过实例介绍当前主要的语义形式描述方法;最后给出这些方法的评价标准和比较结果,并指出最有发展潜力的语义描述方法,以及将来的发展方向。 展开更多

关键词 形式化语义描述 安全协议分析 博弈语义 单子语义

在线阅读 下载PDF 职称材料