时间自动机
时间自动机的相关文献在1998年到2022年内共计274篇,主要集中在自动化技术、计算机技术、铁路运输、无线电电子学、电信技术
等领域,其中期刊论文232篇、会议论文14篇、专利文献1659728篇;相关期刊99种,包括郑州大学学报(理学版)、电子学报、电脑知识与技术等;
相关会议12种,包括2014年河南省计算机学会学术年会暨河南省计算机大会、第十一届全国软件与应用学术会议(NASAC2012)、2011全国软件与应用学术会议(NASAC2011)等;时间自动机的相关文献由567位作者贡献,包括周清雷、庄雷、张广泉等。
时间自动机—发文量
专利文献>
论文:1659728篇
占比:99.99%
总计:1659974篇
时间自动机
-研究学者
- 周清雷
- 庄雷
- 张广泉
- 吕继东
- 姬莉霞
- 李宣东
- 黄志球
- 唐涛
- 戎玫
- 赵建华
- 郑国梁
- 朱维军
- 王瑞
- 董荣胜
- 何亚丽
- 关永
- 张怡欢
- 王亮
- 王从银
- 王国卿
- 王婷
- 王峻
- 郭亚锋
- 陈铁明
- 陈铭松
- 凌翔
- 刘智
- 吴志鹏
- 周宇
- 周颜
- 岳香芬
- 张东波
- 张习勇
- 张亚东
- 张振宇
- 张昱
- 张超
- 朱雪阳
- 李广元
- 李晓娟
- 李真
- 杨启亮
- 杨瑞
- 林利彬
- 王晓旭
- 秦昊
- 缪淮扣
- 胡军
- 苏锦祥
- 郭华
-
-
宋莉;
李飞;
赵瑜;
赵健
-
-
摘要:
针对等级转换场景下的变异测试集不完备问题,提出基于时间自动机(Time Automata,TA)的等级转换场景变异测试研究方法。该方法结合时间自动机理论和等级转换操作流程建立TA模型,同时设计15种变异算子对模型进行变异测试,通过计算加权变异分数评估测试案例集的完备性,并对加权变异分数较低的算子进一步修改补充,最终得到了较为完备的变异测试案例集。
-
-
刘嘉诚;
王梓丞;
易立富;
王光前
-
-
摘要:
全自动运行是未来城市轨道交通发展的主要方向,与传统驾驶模式相比,对于特殊运行场景下的应急处理能力与处理效率有着更高的要求。本文基于列车发生火灾的特殊运行场景,区别于以往由调度人员作为综合监控系统与列车自动监督系统的联动桥梁,设计了全自动驾驶场景下的火灾联动方案,确定了火灾报警系统的火灾识别流程、列车控制管理系统的数据转发和应急控制流程、运行控制中心的火灾响应流程,以及各系统之间的通信校验流程;同时,使用基于时间自动机理论的UPPAAL工具,对从火灾识别到火灾应急响应的全过程进行了形式化建模分析,并且对该联动方案的安全性和功能进行了形式化验证。验证结果表明,该联动方案能够有效地满足各个系统之间的联动要求,为全自动驾驶模式下的非正常运行场景的应急联动处理打下基础。
-
-
李耀;
张晓霞;
郭进;
张亚东
-
-
摘要:
测试模型是高铁信号系统安全关键功能测试用例编制的重要基础,针对高铁信号系统安全关键功能测试建模过程中描述信号系统领域特征不够全面的问题,提出时间状态机测试建模理论和测试用例生成方法.分析高铁信号系统测试建模的特点,提出信号系统安全关键功能测试模型的建模需求;以有限状态机理论为研究基础,结合功能逻辑和时钟约束提出时间状态机建模方法,采用Z规格说明语言给出时间状态机的形式化定义;将时间状态机转换为时间自动机,证明转换之间的一致性,并基于时间自动机的测试理论自动生成测试用例,再以计算机联锁系统中的道岔转换功能为例,建立时间状态机测试模型并生成测试用例.最后,将两种方法生成的测试案例进行对比,结果表明:在功能逻辑方面,基于时间状态机建模方法生成的测试案例100%地覆盖了基于时间自动机建模方法生成的测试案例,并新增了16条具有时钟约束的测试案例,能够满足高铁信号系统安全关键功能测试建模的需求.
-
-
石安;
张卓若;
代立云
-
-
摘要:
实时系统的建模与验证是实时系统开发过程中不可或缺的环节。由于目前业界中广泛使用的建模验证工具UPPAAL存在下载安装慢、拖拽控件不灵活且不支持多用户进行项目团队管理等弊端与局限性,在考虑UPPAAL缺点的同时结合实际应用需要,设计并实现基于B/S架构的实时系统的建模和验证工具。该工具通过浏览器即可访问,提供良好建模操作体验的同时支持多用户进行项目团队管理。使用该工具编辑运行具体实例,验证了实例系统的可达性、安全性等性质,获得了预期的正确结果,完成了该工具的功能测试。
-
-
孔琳琳;
杨启亮;
邢建春;
孙晓波;
邹荣伟;
汤润之
-
-
摘要:
基于BIM的建筑运维平台已经在国防工程中逐步得到应用,其在工程日常运行、应急管理及作战保障中发挥着重要作用.但是,由于现有的建筑信息模型(BIM)中缺少火灾应急管理描述,使得BIM运维平台在火灾情况下的工程应急管理和处理能力受到限制.为此,提出一种面向国防工程火灾应急管理的BIM扩展方法,通过对国防工程火灾应急管理流程与IFC标准框架分析,融合火灾应急管理涉及要素实体、关系、流程和知识等信息,在IFC标准框架中定义面向国防工程火灾应急管理的新实体、新过程,并利用时间自动机等形式化工具验证了BIM火灾应急管理模型的正确性,为BIM在国防工程火灾应急管理中的应用奠定了技术基础.
-
-
陈光;
蒋同海;
王蒙;
唐新余;
季文飞
-
-
摘要:
探讨基于时间自动机理论进行物联网系统建模和模型检测的理论、方法、工具和实践.对时间自动机的基础理论进行比较全面和精确的论述,完善部分概念及其精确的形式化定义.提出基于时间自动机理论进行建模的方法,并指出时间自动机理论研究对物联网系统建模的指导意义.介绍时间自动机的建模工具UPPAAL,说明基于UPPAAL建立时间自动机模型的建模、仿真和检测方法.结合物联网系统中一个经典的温度感知服务的系统需求、理论与实践相结合,进行温度感知管理系统时间自动机建模,并进行模型仿真与模型检测.实验结果表明,该系统能够正确感知温度,具有容错性且不会陷入死锁.
-
-
陆芝浩;
王瑞;
孔辉;
关永;
施智平
-
-
摘要:
Ptolemy是一个广泛应用于信息物理融合系统的建模和仿真工具包,主要通过仿真的方式保证所建模型的正确性.形式化方法是保证系统正确性的重要方法之一.提出了一种基于形式模型转换的方法来验证离散事件模型的正确性.离散事件模型根据不同事件的时间戳触发组件,时间自动机模型能够表达这个特征,因此选用Uppaal作为验证工具.首先定义了离散事件模型的形式语义;其次设计了一组从离散事件模型到时间自动机的映射规则;然后在Ptolemy环境中实现了一个插件,可以自动将离散事件模型转换为时间自动机模型,并通过调用Uppaal验证内核完成验证;最后,以一个交通信号灯控制系统为例进行了成功的转换和验证,实验结果证实了该方法能够验证Ptolemy离散事件模型的正确性.
-
-
孙青怡;
黄志韬
-
-
摘要:
PLCopen标准库描述了常见的运动控制功能块,广泛运用于运动控制系统.不过,很少有方法来验证基于这个标准的系统.以验证运动控制程序的安全性、可达性为目标,提出针对PLCopen运动控制功能块的模型转换方法.根据可编程控制器的周期扫描特性,提出可编程控制器执行模型.提出将功能块图程序(function block diagram,FBD)转换为基于Uppaal系统的时间自动机模型,从而验证运动控制程序的可靠性.
-
-
马海迎;
李奕彤;
袁晓舒;
桑梓;
何立栋
-
-
摘要:
近年来,汽轮机控制保护系统面临的安全威胁引起了学术界及工业界的广泛重视.不同于以往针对通信协议的攻击,攻击者逐渐将目标转移到控制器本身上来.为了应对这种新的威胁,学者们开始研究如何对控制器建立有效的模型去刻画、分析这种攻击对系统运行的影响,进而设计及时、有效的防御策略.本文在总结相应研究的基础上,提出一种基于时间自动机的形式化方法对汽轮机控制保护系统进行建模,同时借助UPPAAL软件,对建立的模型进行仿真及验证.研究表明,本文提出的模型可以较好地描述汽轮机控制保护系统的工作过程,为后续安全问题研究奠定基础.
-
-
程宝;
张福景
-
-
摘要:
TCMS(Train Control and Management System)是列车运行控制、数据监测的中枢,文章分析磁浮列车TCMS的系统拓扑和功能需求,建立时间自动机模型,运用UPPAAL验证工具对TCMS的安全性和时效性进行验证。结果表明,时间自动机对于磁浮列车的TCMS建模和验证效果良好。
-
-
-
高新;
臧洌;
黄越
- 《第十五届全国青年通信学术会议》
| 2010年
-
摘要:
针对移动Ad hoc网络AODV路由协议所面临的安全问题,本文设计了一种基于信誉值和资源值的安全簇首选举机制,并在该分簇结构网络中引入一种基于有限时间自动机的入侵检测算法。簇首担任该簇的检测节点,通过时间自动机判断入侵者。该方法不需要事先训练数据,能够实时检测入侵行为。通过仿真实验,证实了该算法具有较高的检测率。
-
-
-
-
- 《2008年全国理论计算机科学学术年会》
| 2008年
-
摘要:
本文介绍一种具有优先级扩展的时间自动机模型,并对一种计算DBM减法算法进行改进.这种减法是DBM上操作中的一种,它会产生需要用DBM集来表示的非凸集合.DBM的数量影响符号模型检测的性能,我们的减法算法是有效的,因为它产生的DBM的数量相对于最初算法具有较大程度的约减.DBM减法操作扩展了具有优先级的时间自动机理论,它对于具有紧急行为的变换描述、死锁检测、时间博弈等问题具有非常重要的作用。
-
-
-
-
张广泉;
戎玫;
朱雪阳;
何亚丽
- 《2010年全国软件与应用学术会议(NASAC2010)》
| 2010年
-
摘要:
Web服务组合是当前Web服务领域的一个研究热点,目前已有一些相关的描述与验证方法,但从体系结构角度研究Web服务组合描述与验证方法,则是一个新的研究内容.基于软件体系结构描述语言XYZ/ADL和精化检验/模型检测方法,提出了一种Web服务组合的描述与验证框架.XYZ/ADL是时序逻辑语言XYZ/E的扩展,考虑到多数Web服务具有实时特征,可采用XYZ/E的实时扩展语言即XYZ/RE表示系统应满足的时间约束.针对Web服务组合系统,根据XYZ/RE到时间自动机的映射规则将系统描述转换为对应的时间自动机,分别采用精化检验和模型检测两种技术验证Web服务组合的正确性;最后通过两个实例分析分别阐述了上述方法的可行性和有效性.
-
-