结合关注事件的时间自动机语言包含模型检测

论文摘要

时间自动机是实时系统形式化建模和验证的主要手段,能够对系统各个组件能否正确交互及通信进行验证.系统模型和待验证属性都用时间自动机表示,时间自动机语言包含模型检测方法能够验证系统模型是否满足带有时间要求的属性.目前相关工作中没有完善的能够应用于实际的语言包含检测方法,因为该方法要求系统模型和验证属性具有相同的事件集合,但在实际问题中,系统模型往往包含大量事件,而属性模型一般只关注少数的事件.因此,本文改进了已有的时间自动机语言包含算法,使其在运行时只需考虑关注事件,并总结了时间自动机描述的常用属性模式,以帮助用户更好地建模.此外,本文将该方法用于一个水位控制系统的建模和验证,得出了有效结论.

论文目录

文章来源

类型: 期刊论文

作者: 王婷,苏琪,陈铁明

关键词: 时间自动机,语言包含,模型检测,属性模式

来源: 小型微型计算机系统 2019年12期

年度: 2019

分类: 信息科技

专业: 计算机软件及计算机应用

单位: 浙江工业大学计算机科学与技术学院

基金: 国家自然科学基金项目(61602412,U1509214,61772026)资助

分类号: TP301.1

页码: 2578-2584

总页数: 7

文件大小: 1599K

下载量: 43

相关论文文献

• [1].有关时间自动机重置的若干问题的计算复杂性[J]. 软件学报 2019(07)
• [2].基于价格时间自动机的飞机着陆最优成本研究[J]. 济南大学学报(自然科学版) 2013(02)
• [3].基于层次时间自动机的动态行为取证建模方法[J]. 微电子学与计算机 2012(11)
• [4].一种基于时间自动机网络的实时系统形式化验证方法[J]. 苏州大学学报(自然科学版) 2008(01)
• [5].基于层次时间自动机的移动授权的建模与验证[J]. 科学技术与工程 2020(11)
• [6].基于概率时间自动机的智能医疗环境处理流程分析[J]. 工业工程与管理 2018(06)
• [7].设备自动巡检控制逻辑的层级时间自动机建模与验证[J]. 计算机科学 2017(04)
• [8].可调整时间自动机可达性算法的研究[J]. 信息技术 2014(09)
• [9].基于时间自动机的脑网络时空演化建模方法[J]. 计算机工程与应用 2018(14)
• [10].一种层次式时间自动机模型检测方法[J]. 计算机应用与软件 2012(11)
• [11].模型检测基于概率时间自动机的反例产生研究[J]. 计算机研究与发展 2008(10)
• [12].时序图到时间自动机自动转换与布局算法[J]. 计算机工程与设计 2017(08)
• [13].基于时间自动机的自主化ATP等级转换功能建模与验证[J]. 城市轨道交通研究 2019(07)
• [14].基于时间自动机的智慧实训室通信模式研究[J]. 实验技术与管理 2018(03)
• [15].基于时间自动机的实时系统建模及验证[J]. 计算机时代 2011(06)
• [16].基于时间自动机的嵌入式系统AADL模型可调度性验证[J]. 东南大学学报(自然科学版) 2015(06)
• [17].基于时间自动机的物联网服务建模和验证[J]. 网络安全技术与应用 2015(06)
• [18].基于概率时间自动机的模型检测反例表示研究[J]. 苏州大学学报(自然科学版) 2011(02)
• [19].基于时间自动机网的C~3I系统建模和实时性验证[J]. 哈尔滨工程大学学报 2008(03)
• [20].基于扩展RED图的概率时间自动机可达性分析[J]. 计算机系统应用 2016(10)
• [21].一种基于离散时间自动机的LTL性质检测工具[J]. 计算机仿真 2008(04)
• [22].基于时间自动机的物联网组合服务建模[J]. 计算机工程与设计 2019(01)
• [23].基于概率时间自动机Web服务质量的形式化建模分析[J]. 吉林大学学报(理学版) 2015(03)
• [24].复杂环境下基于价格时间自动机飞机着陆调度[J]. 传感器与微系统 2013(06)
• [25].SpaceWire网络层分析的时间自动机模型[J]. 微电子学与计算机 2019(01)
• [26].基于时间自动机的风洞试验自动控制研究[J]. 微计算机信息 2009(04)
• [27].多核模型检测工具CTAV的实现与优化[J]. 计算机系统应用 2018(09)
• [28].在原型验证系统中构建度量区间时序逻辑公式的时间自动机(英文)[J]. Journal of Shanghai University(English Edition) 2008(04)
• [29].识别时间自动机中可加速环的方法[J]. 计算机工程与设计 2010(23)
• [30].时间自动机模型验证的研究进展[J]. 计算机应用与软件 2008(06)

标签：时间自动机论文;  语言包含论文;  模型检测论文;  属性模式论文;