【摘 要】
：
地下建筑工程中的设备系统经常处于静止状态,为保证其在需要时能安全可靠的运行,需对设备定期进行自动巡检在自动巡检过程中,设备自动巡检控制逻辑起到了举足轻重的作用为了
【机 构】
：
解放军理工大学国防工程学院南京210007解放军理工大学国防工程学院南京210007;计算机软件新技术国家重点实验室(南京大学)南京210093
论文部分内容阅读
地下建筑工程中的设备系统经常处于静止状态,为保证其在需要时能安全可靠的运行,需对设备定期进行自动巡检在自动巡检过程中,设备自动巡检控制逻辑起到了举足轻重的作用为了解决复杂的设备自动巡检控制逻辑造成的一系列问题,之前提出了一种层级有限自动机(HFA)的形式化模型,并利用HFA对设备自动巡检控制逻辑实现了行为建模,但并未添加时间属性及验证其正确性与可靠性现提出一种层级时间自动机形式化模型,并利用它对设备自动巡检控制逻辑进行建模,再用UPPAAL对其进行分析与形式化验证,分别验证其安全性、可达性、活性及时间约束,以此来确保其时效正确性与可靠性这种建模与形式化验证方法,弥补了之前无时间约束的漏洞,有效的确保了设备自动巡检控制逻辑的正确性与可靠性最终,该模型通过了模拟和验证,充分证明了设备自动巡检控制逻辑是正确可靠的.
其他文献
针对现有的合成孔径雷达（SAR）成像方法，介绍了隐抽样平均算法的基本原理及时延确定的方法；进一步，将隐抽样平均算法用于SAR成像中，提出了基于隐抽样平均的SAR成像算法；该成像算法利
日前，工业和信息化部发布《船舶工业技术进步和技术改造投资方向（2009—2011）》（以下简称《投资方向》），明确了船舶工业科研开发的重点领域和主要内容，以及技术改造的重点领域和主要
高性能处理器普遍采用片上集成大容量复杂结构的一级Cache提高处理器性能，但随着Cache容量和复杂度的增加，访问Cache所产生的访存延迟和功耗明显增加；基于存储队列，提出了一种通
远程心电监护中采集到的心电信号往往包含较严重的噪声干扰，给医生的诊断带来了困难，针对这一问题，介绍了一种基于人工神经网络和自适应噪声抵消的ECG信号自动提取方法；用一个三
主要讨论了LVDS的信号特点,并重点讨论了图像信号时序的分析和转换以及模拟摄像机与PXI 1422的时序,提出了在考虑导引头图像数据凝视发送方式和线扫交替发送方式两个模式下的
以基于PXI总线RS422数据格式通信卡的设计为例,介绍PXI总线在目前高速数据通信中的一种应用及Windows2000/XP下WDM设备驱动程序的运行机理和编程要点;针对开发调试工具DriverStudio给出了基于一定实时性要求的驱动程序实例,重点讨论了驱动程序设计中的中断处理实现及与Win32应用程序异步通信等关键问题;实验结果表明,多线程技术和中断传输方式相结合,实时响应速度有了显著提高,
异构信息空间中的实体和关联关系普遍具有时间信息、多种时间版本的实体数据共存,而传统的实体集成忽略了时间信息,不支持时间维度上的集成。提出一种异构信息空间中时间感知
超密集网络中,严重的小区间干扰制约了终端用户的数据速率,针对该问题,提出一种基于簇优先级的资源分配方案。该方案分为3个步骤：首先,采用基于图论的染色算法为毫微微接入点（F
针对巡航导弹动力学仿真的任务要求,对巡航导弹作战流程和飞行弹道工作展开了深入研究,并设计开发了新一代具有跨平台、通用性、可灵活配置及高可扩展特性等特点的巡航导弹动
中国航天科工信息技术研究院今天正式揭牌。该研究院由原中国航天科工信息技术研究院、中国航天科工八五一一研究所、北京航天测控技术开发公司、中国航天系统工程公司等单位