期刊文献+
共找到6篇文章
< 1 >
每页显示 20 50 100
使用事件自动机规约的C语言有界模型检测 被引量:4
1
作者 阚双龙 黄志球 +1 位作者 陈哲 徐丙凤 《软件学报》 EI CSCD 北大核心 2014年第11期2452-2472,共21页
提出使用事件自动机对C程序的安全属性进行规约,并给出了基于有界模型检测的形式化验证方法.事件自动机可以规约程序中基于事件的安全属性,且可以描述无限状态的安全属性.事件自动机将属性规约与C程序本身隔离,不会改变程序的结构.在事... 提出使用事件自动机对C程序的安全属性进行规约,并给出了基于有界模型检测的形式化验证方法.事件自动机可以规约程序中基于事件的安全属性,且可以描述无限状态的安全属性.事件自动机将属性规约与C程序本身隔离,不会改变程序的结构.在事件自动机的基础上,提出了自动机可达树的概念.结合自动机可达树和有界模型检测技术,给出将事件自动机和C程序转化为可满足性模理论SMT(satisfiability modulo theory)模型的算法.最后,使用SMT求解器对生成的SMT模型求解,并根据求解结果给出反例路径分析算法.实例分析和实验结果表明,该方法可以有效验证软件系统中针对事件的属性规约. 展开更多
关键词 事件自动机 可满足性模理论 有界模型检测 自动机可达树 安全关键软件
下载PDF
基于多智能体的实时并发式智能机器人结构 被引量:4
2
作者 朱淼良 吴春明 +2 位作者 张友军 金毅 李捷 《高技术通讯》 CAS CSCD 1995年第10期20-24,共5页
利用分布式人工智能系统中的多智能体(MAS)原理设计了自主式移动机器人的智能体系结构RMAS,它是由多计算机连通域ROBIX、离散事件有限状态转换模型及流水线调度机构三部分组成,文中给出了仿真试验结果。
关键词 多智能体系统 机器人 智能机器人 结构
下载PDF
基于事件确定有限自动机的UML2.0序列图描述与验证 被引量:8
3
作者 张琛 段振华 田聪 《软件学报》 EI CSCD 北大核心 2011年第11期2625-2638,共14页
为了确保软件分析与设计阶段UML2.0序列图模型的可靠性,采用命题投影时序逻辑(propositional projection temporal logic,简称PPTL)模型检测方法对该模型进行分析和验证.提出了事件确定有限自动机(event deterministic finite automata... 为了确保软件分析与设计阶段UML2.0序列图模型的可靠性,采用命题投影时序逻辑(propositional projection temporal logic,简称PPTL)模型检测方法对该模型进行分析和验证.提出了事件确定有限自动机(event deterministic finite automata,简称ETDFA),并使用该自动机为序列图建立形式化模型,通过给出的基于ETDFA的PPTL模型检测算法得到验证结果.该方法可以在基于Spin的PPTL模型检测器的支持下实现.实例结果表明,该方法可以验证序列图的性质并保证其可靠性. 展开更多
关键词 UML2.0序列图 事件确定有限自动机 模型检测 命题投影时序逻辑 验证
下载PDF
RFID Complex Event Processing: Applications in Real-Time Locating System 被引量:2
4
作者 Yao-zong Liu Hong Zhang Yong-li Wang 《International Journal of Intelligence Science》 2012年第4期160-165,共6页
Complex event processing (CEP) can extract meaningful events for real-time locating system (RTLS) applications. To identify complex event accurately in RTLS, we propose a new RFID complex event processing method GEEP,... Complex event processing (CEP) can extract meaningful events for real-time locating system (RTLS) applications. To identify complex event accurately in RTLS, we propose a new RFID complex event processing method GEEP, which is based on the timed automata (TA) theory. By devising RFID locating application into complex events, we model the timing diagram of RFID data streams based on the TA. We optimize the constraint of the event streams and propose a novel method to derive the constraint between objects, as well as the constraint between object and location. Experiments prove the proposed method reduces the cost of RFID complex event processing, and improves the efficiency of the RTLS. 展开更多
关键词 Complex event Processing (CEP) REAL-TIME Locating System (RTLS) Radio Frequency Identification (RFID) TIMED automata (TA) event-Clock automata (ECA)
下载PDF
时间自动机两种模型的构造互模拟研究
5
作者 朱维军 王迤冉 +1 位作者 李琳娜 周清雷 《微电子学与计算机》 CSCD 北大核心 2007年第1期156-158,161,共4页
基于时间自动机不同模型的验证被工业界广泛应用,本文形式描述了两种这样的模型,给出了从事件时钟自动机到双向时间自动机的构造方法,证明了二者识别语言之间的包含关系。
关键词 双向时间自动机 事件时钟自动机 事件记录自动机 事件预测自动机
下载PDF
用布尔矩阵分析离散事件系统 被引量:1
6
作者 戴学丰 王春彦 《齐齐哈尔轻工业学院学报》 1996年第3期1-5,共5页
本文用布尔矩阵研究了一类可用自动机描述的离散事件系统的有关性质。通过简单的矩阵运算,便可确定出系统状态间的距离(事件数)等参数。此外还讨论了用状态转移矩阵确定系统的可能逻辑迹集等问题。
关键词 离散事件系统 自动机 布尔矩阵 逻辑迹集
下载PDF
上一页 1 下一页 到第
使用帮助 返回顶部