UML2.0顺序图的时序描述逻辑语义 被引量：7

1

作者 张其文 童格明 李明 《计算机工程》 CAS CSCD 北大核心 2011年第3期52-54,共3页

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

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

在线阅读 下载PDF 职称材料

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

2

作者 李明 刘士仪 年福忠 《计算机应用》 CSCD 北大核心 2013年第1期266-269,共4页

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

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

在线阅读 下载PDF 职称材料

基于时序描述逻辑的UML状态图语义 被引量：1

3

作者 李明 杨海波 +1 位作者 张其文 王旭阳 《计算机工程》 CAS CSCD 北大核心 2010年第23期76-78,共3页

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

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

在线阅读 下载PDF 职称材料

基于时序描述逻辑的UML顺序图形式化方法 被引量：5

4

作者 陈振庆 《计算机工程》 CAS CSCD 2013年第3期36-40,共5页

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

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

在线阅读 下载PDF 职称材料

描述用户行为的数字权限时序描述逻辑系统 被引量：1

5

作者 凌志辉 翟玉庆 《计算机工程》 EI CAS CSCD 北大核心 2005年第19期61-63,共3页

数字权限管理技术(DRM)的核心是权限描述,而基于动作序列的权限描述模型主要是描述数字产品消费者(用户)允许产生的动作序列,通过动作序列分析,可跟踪权限的执行过程,方便地限制和预测用户在数字内容消费过程中的行为并审计其合理性。... 数字权限管理技术(DRM)的核心是权限描述,而基于动作序列的权限描述模型主要是描述数字产品消费者(用户)允许产生的动作序列,通过动作序列分析,可跟踪权限的执行过程,方便地限制和预测用户在数字内容消费过程中的行为并审计其合理性。文章提出一种基于时序描述逻辑的逻辑推理系统,该系统不仅可以表达用户行为的静态特征,而且可以刻画用户行为之间的时序关系。 展开更多

关键词 数字权限 时序描述逻辑 用户行为

在线阅读 下载PDF 职称材料

基于动态时序描述逻辑的动作理论

6

作者 孙永新 赵希顺 《计算机科学》 CSCD 北大核心 2014年第9期210-214,238,共6页

动态时序描述逻辑(DLTLDL)是一类描述逻辑的动态时序扩展。提出一种基于DLTLALCIO的动态域建模方法,利用该方法可构造出刻画动态域知识的DLTLALCIO理论,并解决动作推理中的框架问题和分支问题。动作推理问题,如动作可执行性和投影问题等... 动态时序描述逻辑(DLTLDL)是一类描述逻辑的动态时序扩展。提出一种基于DLTLALCIO的动态域建模方法,利用该方法可构造出刻画动态域知识的DLTLALCIO理论,并解决动作推理中的框架问题和分支问题。动作推理问题,如动作可执行性和投影问题等,可归结为关于DLTLALCIO理论的推理问题,并最终归结为DLTLALCIO的公式可满足性问题。DLTLALCIO公式可表达动作和时间约束,相对于其他基于描述逻辑的动作形式,基于DLTLALCIO的动作形式在需要执行复杂查询,尤其是含时间或动作的查询的应用场合具有更好的适用性。 展开更多

关键词 动态时序描述逻辑 动作推理 动态域 动作理论

在线阅读 下载PDF 职称材料

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

7

作者 陈振庆 《制造业自动化》 北大核心 2012年第2期77-79,84,共4页

本文针对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状态图 形式化规约 形式化验证

在线阅读 下载PDF 职称材料

基于时序描述逻辑的故障树分析方法研究 被引量：1

8

作者 司佳 朱羿全 马琳 《计算机技术与发展》 2017年第12期89-92,97,共5页

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

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

在线阅读 下载PDF 职称材料

基于时序描述逻辑的UML顺序图形式化研究 被引量：2

9

作者 冉婕 谢树云 漆丽娟 《计算机系统应用》 2018年第8期276-280,共5页

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

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

在线阅读 下载PDF 职称材料

基于描述逻辑的带属性依赖时序ER模型 被引量：12

10

作者 蒋运承 汤庸 +1 位作者 王驹 冀高峰 《计算机研究与发展》 EI CSCD 北大核心 2007年第10期1765-1773,共9页

分析了描述逻辑在数据库中的研究现状和存在的问题,特别是描述逻辑与时序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模型 属性依赖 时序数据库

在线阅读 下载PDF 职称材料

描述逻辑的动态时序扩展 被引量：5

11

作者 孙永新 赵希顺 符志强 《计算机应用研究》 CSCD 北大核心 2012年第2期536-541,共6页

在一些基于本体的动态应用中,需要描述组合动作和变化域的时间特性。为了对这类应用建模,通过整合动态时序逻辑和描述逻辑,提出一类描述逻辑扩展。分析了该类扩展的基本形式DLTLALC的语法和语义,并提出一种可终止的tableau算法判别DLTL... 在一些基于本体的动态应用中,需要描述组合动作和变化域的时间特性。为了对这类应用建模,通过整合动态时序逻辑和描述逻辑,提出一类描述逻辑扩展。分析了该类扩展的基本形式DLTLALC的语法和语义,并提出一种可终止的tableau算法判别DLTLALC公式可满足性。利用该类扩展,可以表达组合动作执行过程中域变化的时间特性,该类扩展为语义Web服务等动态应用建模和推理提供了一条有效途径。 展开更多

关键词 动态时序描述逻辑 动作推理 表判定算法 语义WEB服务

在线阅读 下载PDF 职称材料

面向对象的时序动态描述逻辑管理制度设计 被引量：1

12

作者 苏朋程 《商业时代》 北大核心 2013年第7期106-108,共3页

本文结合面向对象、时序动态描述逻辑等概念及理论,研究了管理制度设计的面向对象的时序动态描述逻辑公式描述形式,这些公式是管理制度中各条款语言文字化的逻辑及概念基础。文章采用面向对象、时序动态描述逻辑等理论和方法,实现将管... 本文结合面向对象、时序动态描述逻辑等概念及理论,研究了管理制度设计的面向对象的时序动态描述逻辑公式描述形式,这些公式是管理制度中各条款语言文字化的逻辑及概念基础。文章采用面向对象、时序动态描述逻辑等理论和方法,实现将管理目的、管理控制参数、管理过程等描述成逻辑公式,使管理制度更加直观、简洁,便于形式化地分析管理漏洞。最后,通过实例分析了面向对象的时序动态描述逻辑的管理制度设计过程及其步骤。 展开更多

关键词 管理对象 面向对象 时序动态描述逻辑 管理制度设计

在线阅读 下载PDF 职称材料