检索结果-南通市图书馆

基于时序描述逻辑的Web服务本体语言过程模型语义

在线全文

学校读者我要写书评

暂无评论

计算机应用 2013年第1期33卷 266-269页

作者：李明刘士仪年福忠兰州理工大学计算机与通信学院兰州730050

针对Web服务本体语言(OWL-S)过程模型存在动态交互和时序特征表达能力不足的问题,提出一种基于时序描述逻辑的过程模型形式化方法。通过对OWL-S过程模型的原子过程和组合过程语义进行形式化的描述,得到了OWL-S的过程模型的动态语义,最... 详细信息

针对Web服务本体语言(OWL-S)过程模型存在动态交互和时序特征表达能力不足的问题,提出一种基于时序描述逻辑的过程模型形式化方法。通过对OWL-S过程模型的原子过程和组合过程语义进行形式化的描述,得到了OWL-S的过程模型的动态语义,最终实现了对OWL-S过程模型的形式化建模。实例结果验证了所提方法的可行性,为进一步的分析和验证提供了基础。

关键词： Web服务本体语言时序描述逻辑服务组合形式化过程模型建模

在线全文

学校读者我要写书评

暂无评论

基于时序描述逻辑的UML状态图语义

计算机工程 2010年第23期36卷 76-78页

作者：李明杨海波张其文王旭阳兰州理工大学计算机与通信学院兰州730050

将UML图形转换成形式化规范是一种精确UML语义、扩大形式化软件方法适用范围的有效途径。鉴于描述逻辑强的可判定推理能力,提出一种采用时序描述逻辑形式化UML状态图,对描述逻辑进行时序扩展,得到可以表示动态和时序语义的形式化规范—... 详细信息

将UML图形转换成形式化规范是一种精确UML语义、扩大形式化软件方法适用范围的有效途径。鉴于描述逻辑强的可判定推理能力,提出一种采用时序描述逻辑形式化UML状态图,对描述逻辑进行时序扩展,得到可以表示动态和时序语义的形式化规范——时序描述逻辑,给出一套UML状态图向时序描述逻辑表达式转换的规则,通过实例验证了该方法的可行性。

关键词：描述逻辑时序扩展时序描述逻辑状态图形式化

在线全文

学校读者我要写书评

暂无评论

UML2.0顺序图的时序描述逻辑语义

计算机工程 2011年第3期37卷 52-54页

作者：张其文童格明李明兰州理工大学计算机与通信学院兰州730050

针对UML2.0顺序图用于对象间交互行为建模时存在动态语义缺乏精确形式化描述的问题,提出一种基于时序描述逻辑的UML2.0顺序图形式化方法。对描述逻辑进行时序扩展,得到可表示动态和时序语义的形式化规范——时序描述逻辑,根据UML2.0新... 详细信息

针对UML2.0顺序图用于对象间交互行为建模时存在动态语义缺乏精确形式化描述的问题,提出一种基于时序描述逻辑的UML2.0顺序图形式化方法。对描述逻辑进行时序扩展,得到可表示动态和时序语义的形式化规范——时序描述逻辑,根据UML2.0新增的交互操作符将UML2.0顺序图分成一个或多个最大顺序片段,通过形式化最大顺序片段和交互操作符得到UML2.0顺序图的时序描述逻辑语义。实例检验结果表明,该方法具有可行性。

关键词： UML2.0顺序图时序描述逻辑形式化描述逻辑

在线全文

学校读者我要写书评

暂无评论

基于时序描述逻辑的UML状态图形式化验证

制造业自动化 2012年第2期34卷 77-79,84页

作者：陈振庆广西贺州学院计算机科学与工程系贺州542800

本文针对UML状态图具有动态行为和时序特征的特点,提出了一种新的描述逻辑,即时序描述逻辑TDDL(SHOIN(D))。首先给出了TDDL(SHOIN(D))的语法和语义,研究了TDDL(SHOIN(D))的断言公式集一致性推理和动作推理问题,给出了TDDL(SHOIN(D))的... 详细信息

本文针对UML状态图具有动态行为和时序特征的特点,提出了一种新的描述逻辑,即时序描述逻辑TDDL(SHOIN(D))。首先给出了TDDL(SHOIN(D))的语法和语义,研究了TDDL(SHOIN(D))的断言公式集一致性推理和动作推理问题,给出了TDDL(SHOIN(D))的断言公式集一致性推理算法,并证明了该推理算法的可判定性;然后给出了动作包含、等价关系的判断方法,并证明了这些方法的可判定性。最后利用TDDL(SHOIN(D))对UML状态图进行了形式化验证。

关键词：时序描述逻辑 UML状态图形式化规约形式化验证

在线全文

学校读者我要写书评

暂无评论

基于时序描述逻辑的UML状态图语义研究

基于时序描述逻辑的UML状态图语义研究

作者：杨海波兰州理工大学

学位级别：硕士

统一建模语言(Unified Modeling Language) UML简洁、直观,便于建模人员之间的交流与沟通,适用于软件开发的各个阶段。然而,UML缺乏精确的形式化语义,难以对它所描述的系统进行形式化分析和一致性检验。描述逻辑具有很强的表达和可判定... 详细信息

统一建模语言(Unified Modeling Language) UML简洁、直观,便于建模人员之间的交流与沟通,适用于软件开发的各个阶段。然而,UML缺乏精确的形式化语义,难以对它所描述的系统进行形式化分析和一致性检验。描述逻辑具有很强的表达和可判定推理能力,但基本的描述逻辑只能表示静态领域的知识,无法对具有动态和时序特征的知识进行描述。时序逻辑包含大量的时序算子,可以对静态和动态领域的知识进行描述,但它的推理能力不是很强。针对上述问题,本文对基本的描述逻辑进行时序扩展,然后用扩展后的描述逻辑,即用时序描述逻辑TDLs (Temporal Description Logics)对UML状态图进行形式化研究,提高UML状态图语义描述的精确性。本文的主要研究工作包括：***和描述逻辑的异同点。比较了UML和描述逻辑的异同点,包括：静态、动态、共享、可扩展性、继承、封装、类之间的关系、类和属性的层次,以及推理特性。2.描述逻辑的时序扩展。针对基本的描述逻辑无法对具有动态与时序特征的知识进行描述的问题,考虑采用时序算子对基本的描述逻辑进行扩展,得到既可以表示静态知识,又可以对动态和时序知识进行描述的时序描述逻辑,给出了扩展后的语法、语义、定义及公理。***状态图的形式化。状态图是UML重要的行为图之一,通过对状态图进行分析,将UML状态图映射为时序描述逻辑表达式,给出了映射规则,并通过一个实例说明了映射过程,检验了方法的可行性,对形式化后的表达式也进行了正确性检验。

关键词：描述逻辑时序扩展时序描述逻辑 UML状态图形式化

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

基于时序描述逻辑的UML顺序图形式化方法

计算机工程 2013年第3期39卷 36-40页

作者：陈振庆贺州学院计算机科学与工程系广西贺州542800

根据统一建模语言(UML)顺序图的时序特征,提出一种基于时序描述逻辑ALCQIUS的UML顺序图形式化方法。研究ALCQIUS时序扩展部分的语法和语义、ALCQIUS断言公式集一致性定理,给出ALCQIUS断言公式集一致性推理算法,并证明该推理算法的可判... 详细信息

根据统一建模语言(UML)顺序图的时序特征,提出一种基于时序描述逻辑ALCQIUS的UML顺序图形式化方法。研究ALCQIUS时序扩展部分的语法和语义、ALCQIUS断言公式集一致性定理,给出ALCQIUS断言公式集一致性推理算法,并证明该推理算法的可判定性。以公安报警系统为例,说明基于ALCQIUS的UML顺序图形式化规约和形式化验证具备可行性,并且ALCQIUS为UML顺序图形式化提供了合理的逻辑基础。

关键词：时序描述逻辑统一建模语言顺序图静态语义动态语义形式化规约形式化验证

在线全文

学校读者我要写书评

暂无评论

基于时序描述逻辑的UML顺序图形式化研究

计算机系统应用 2018年第8期27卷 276-280页

作者：冉婕谢树云漆丽娟云南昭通学院物理与信息工程学院昭通657000

在统一建模语言(UML)规范中顺序图的语义是以自然语言的形式描述的,是一种半形式化的语言,不能对系统的交互行为进行形式化分析及论证.针对UML顺序图缺乏精确的形式化描述问题,根据顺序图的时序特征,提出了增加交互操作符的UML顺序图的... 详细信息

在统一建模语言(UML)规范中顺序图的语义是以自然语言的形式描述的,是一种半形式化的语言,不能对系统的交互行为进行形式化分析及论证.针对UML顺序图缺乏精确的形式化描述问题,根据顺序图的时序特征,提出了增加交互操作符的UML顺序图的六元组形式化方法.对描述逻辑进行时序扩展,得到可表示动态和时序语义的形式化规范——时序描述逻辑.应用时序描述逻辑的时态算子得到时序描述逻辑语义形式的UML顺序图.用UML顺序图描述完整的C语言执行过程,将其形式化描述,实验结果表明,这种方法是可行的.

关键词： UML顺序图形式化时序描述逻辑算子

在线全文

学校读者我要写书评

暂无评论

基于时序描述逻辑的故障树分析方法研究

计算机技术与发展 2017年第12期27卷 89-92,97页

作者：司佳朱羿全马琳南京航空航天大学计算机科学与技术学院江苏南京210016

故障树分析法是工业界常用的安全分析方法之一。然而由于其非形式化方法的局限性,难以对软件故障进行形式化验证,更难以描述嵌入式实时系统中事件之间的时序逻辑关系。因此,提出了一种基于时序描述逻辑的故障树分析方法,以解决故障树难... 详细信息

故障树分析法是工业界常用的安全分析方法之一。然而由于其非形式化方法的局限性,难以对软件故障进行形式化验证,更难以描述嵌入式实时系统中事件之间的时序逻辑关系。因此,提出了一种基于时序描述逻辑的故障树分析方法,以解决故障树难以对时序关系进行描述以及难以形式化验证的问题。首先,通过时序描述逻辑对故障树进行时序特征的扩充与规约;其次抽取出用描述逻辑表示的软件安全属性;最后对软件系统进行安全属性建模并通过模型检测工具SPIN形式化验证软件系统是否满足这些属性。以某一机载控制系统环境输入模块为案例,对该案例进行故障树分析和建模并给出该案例的待验证安全属性以及实验分析结果。结果表明,提出的方法是有效的和可行的。

关键词：故障树分析时序描述逻辑安全属性形式化验证

在线全文

学校读者我要写书评

暂无评论

基于描述逻辑的带属性依赖时序ER模型

计算机研究与发展 2007年第10期44卷 1765-1773页

作者：蒋运承汤庸王驹冀高峰中山大学计算机科学系广州510275 广西师范大学计算机科学与信息工程学院桂林541004

分析了描述逻辑在数据库中的研究现状和存在的问题,特别是描述逻辑与时序ER模型的关系,在Artale的基础上提出了一种形式化带属性依赖时序ER模型εRVTAD.针对带属性依赖时序ER模型εRVTAD的需求和特点,提出了一种新的描述逻辑,即时序描... 详细信息

分析了描述逻辑在数据库中的研究现状和存在的问题,特别是描述逻辑与时序ER模型的关系,在Artale的基础上提出了一种形式化带属性依赖时序ER模型εRVTAD.针对带属性依赖时序ER模型εRVTAD的需求和特点,提出了一种新的描述逻辑,即时序描述逻辑ALCQI(D)US.给出了ALCQI(D)US的语法和语义,提出了基于ALCQI(D)US的带属性依赖时序ER模型,即给出了如何将带属性依赖时序ER模型εRVTAD转化为ALCQI(D)US知识库,以及利用ALCQI(D)US的推理机制给出了带属性依赖时序ER模型εRVTAD的可满足性、冗余性、包含关系和蕴含关系等自动推理问题,证明了这些推理问题的正确性.

关键词：描述逻辑时序描述逻辑 ER模型时序ER模型属性依赖时序数据库