期刊文献+
共找到6篇文章
< 1 >
每页显示 20 50 100
Capability requirements modeling and verification based on fuzzy ontology 被引量:4
1
作者 Qingchao Dong Zhixue Wang Weixing Zhu Hongyue He 《Journal of Systems Engineering and Electronics》 SCIE EI CSCD 2012年第1期78-87,共10页
The capability requirements of the command, control, communication, computing, intelligence, surveillance, reconnaissance (C41SR) systems are full of uncertain and vague information, which makes it difficult to mode... The capability requirements of the command, control, communication, computing, intelligence, surveillance, reconnaissance (C41SR) systems are full of uncertain and vague information, which makes it difficult to model the C41SR architecture. The paper presents an approach to modeling the capability requirements with the fuzzy unified modeling language (UML) and building domain ontologies with fuzzy description logic (DL). The UML modeling constructs are extended according to the meta model of Depart- ment of Defense Architecture Framework to improve their domain applicability, the fuzzy modeling mechanism is introduced to model the fuzzy efficiency features of capabilities, and the capability requirement models are converted into ontologies formalized in fuzzy DL so that the model consistency and reasonability can be checked with a DL reasoning system. Finally, a case study of C41SR capability requirements model checking is provided to demonstrate the availability and applicability of the method. 展开更多
关键词 fuzzy ontology fuzzy unified modeling language (UML) fuzzy description logic (DL) model checking.
在线阅读 下载PDF
定义及验证UML Statechart图中的数据流语义 被引量:1
2
作者 陆公正 吴澜波 张广泉 《计算机工程与应用》 CSCD 北大核心 2009年第24期56-59,共4页
在传统的UML Statechart图中加入了数据流对象后,因为UML Statechart图缺乏精确的数据流语义,所以不适合应用UML Statechart图对工作流中的数据流进行建模并验证其正确性。为了解决这一问题,选择标记转换系统(LTS)作为语义域,并用结构... 在传统的UML Statechart图中加入了数据流对象后,因为UML Statechart图缺乏精确的数据流语义,所以不适合应用UML Statechart图对工作流中的数据流进行建模并验证其正确性。为了解决这一问题,选择标记转换系统(LTS)作为语义域,并用结构化操作语义(SOS)分两步定义了UML Statechart图的数据流语义,为工作流中的数据流正确性验证奠定了基础。在此基础上,使用时序逻辑公式表示数据流所需满足的性质,在验证数据流的正确性之前,给出了将它的UML Statechart图模型转化为可达状态迁移图的算法,最后通过模型检测算法验证数据流的正确性。 展开更多
关键词 统一建模语言(UML) UML Statechart图 数据流语义 时序逻辑 验证 模型检测
在线阅读 下载PDF
RGPS过程层元模型正确性验证 被引量:1
3
作者 袁开银 郭瑞 +1 位作者 陆翔升 吴尽昭 《计算机工程》 CAS CSCD 2012年第15期39-42,共4页
利用Web服务本体描述语言对RGPS过程层元模型进行描述,建立Promela模型。基于线性时序逻辑,以及Spin检测工具的偏序规约和on-the-fly等优化技术对Promela模型进行正确性验证,设计并实现RGPS过程层元模型正确性验证平台。通过城市交通系... 利用Web服务本体描述语言对RGPS过程层元模型进行描述,建立Promela模型。基于线性时序逻辑,以及Spin检测工具的偏序规约和on-the-fly等优化技术对Promela模型进行正确性验证,设计并实现RGPS过程层元模型正确性验证平台。通过城市交通系统实例证明该验证方法的正确性和有效性。 展开更多
关键词 RGPS框架 Promela建模 Spin模型检测工具 过程层元模型 线性时序逻辑
在线阅读 下载PDF
基于时间区间时序逻辑的实时系统统一模型检测
4
作者 朱维军 乔芃喆 +1 位作者 周清雷 张海宾 《电子科技大学学报》 EI CAS CSCD 北大核心 2014年第5期712-716,共5页
在同一个逻辑框架内无法自动验证实时区间模型的实时区间性质。为此,该文使用一个离散时间区间时序逻辑公式建立实时系统模型,使用另一个离散时间区间时序逻辑公式描述实时系统需要满足的性质,在此基础上,离散时间区间时序逻辑统一模型... 在同一个逻辑框架内无法自动验证实时区间模型的实时区间性质。为此,该文使用一个离散时间区间时序逻辑公式建立实时系统模型,使用另一个离散时间区间时序逻辑公式描述实时系统需要满足的性质,在此基础上,离散时间区间时序逻辑统一模型检测问题即可归约为目前已解决的离散时间区间时序逻辑可满足性判定问题。该文证明了新方法的有效性以及正确性,为区间实时逻辑这一类的模型检测问题提供了方法。 展开更多
关键词 统一模型检测 实时系统 可满足性判定 时间区间时序逻辑
在线阅读 下载PDF
扩展Tempura语言统一模型检测算法
5
作者 朱维军 周清雷 张海宾 《华南理工大学学报(自然科学版)》 EI CAS CSCD 北大核心 2011年第7期163-168,共6页
针对扩展区间时序逻辑目前没有可用的统一模型检测算法的问题,找到了该逻辑可执行子集即扩展Tempura语言的可判定子集——首先限定该逻辑一阶部分的常量与变量均为有穷可枚举类型,然后加上该逻辑的命题部分.在此基础上,提出了扩展区间... 针对扩展区间时序逻辑目前没有可用的统一模型检测算法的问题,找到了该逻辑可执行子集即扩展Tempura语言的可判定子集——首先限定该逻辑一阶部分的常量与变量均为有穷可枚举类型,然后加上该逻辑的命题部分.在此基础上,提出了扩展区间时序逻辑统一模型检测算法,以判定由上述定义的语言子集所书写的规范程序是否满足命题版扩展区间时序逻辑公式所描述的性质.具体方法是首先翻译规范程序到命题扩展区间时序逻辑公式,然后使用该逻辑的公式满足性判定算法进行自动验证.验证实例证实了新方法的有效性. 展开更多
关键词 模型检测 扩展Tempura语言 区间时序逻辑 区间模型 程序规范 统一框架
在线阅读 下载PDF
命题投影时序逻辑并发建模与自动验证 被引量:2
6
作者 朱维军 张海宾 周清雷 《华中科技大学学报(自然科学版)》 EI CAS CSCD 北大核心 2010年第8期77-80,共4页
针对目前尚无模型检测方法对区间并发模型进行区间性质的自动验证的情况,采用命题投影时序逻辑中具有特定结构的一类公式来建立系统的区间并发模型,该逻辑的任意公式可以描述模型需要满足的区间性质,通过归约为已有的逻辑公式可满足性... 针对目前尚无模型检测方法对区间并发模型进行区间性质的自动验证的情况,采用命题投影时序逻辑中具有特定结构的一类公式来建立系统的区间并发模型,该逻辑的任意公式可以描述模型需要满足的区间性质,通过归约为已有的逻辑公式可满足性判定算法,证明了命题投影时序逻辑统一框架模型检测是可判定的,从而得到了其自动验证方法,并给出了一个验证实例. 展开更多
关键词 模型检测 时序逻辑 可计算性与判定性 命题投影时序逻辑 并发模型 统一逻辑框架
原文传递
上一页 1 下一页 到第
使用帮助 返回顶部