| 基于LTL预测语义的高效监控器构造 |
| |
| 引用本文： | 马佩勋,赵常智.基于LTL预测语义的高效监控器构造[J].湖南科技大学学报(自然科学版),2013,28(1):87-92. |
| |
| 作者姓名： | 马佩勋 赵常智 |
| |
| 作者单位： | 1.长沙民政学院 软件学院,湖南 长沙 410004;2.国防科学技术大学 计算机学院,湖南 长沙 410073 |
| |
| 基金项目： | 国家自然科学基金项目(50875087) |
| |
| 摘 要： | 运行时验证中的一个重要研究内容就是从高层规约生成高效的监控器,并有效控制监控器的生成复杂度与监控器运行时开销.基于线性时序逻辑(LTL)的预测语义,通过删除与合并Büchi自动机中的大部分状态,提出一种高效的预测监控器构造技术.通过该方法,可以大大降低最终预测监控器的规模,提高监控器产生的效率;同时保证把监控器的运行时开销控制在合理的范围内.基于上述预测监控器构造技术,实现了相应工具monitor_tool,该工具比LTL3_tool工具更小,且能够为更多的LTL性质产生监控器. 同时,产生的监控器能够尽可能早的识别一个持续被监控的执行轨迹是否满足指定的正确性性质.
|
| 关 键 词： | 线性时序逻辑 预测监控器 自动机 运行时验证 |
The construction of an LTL-based efficient anticipatory monitor |
| |
| MA Pei-xun,ZHAO Chang-zhi.The construction of an LTL-based efficient anticipatory monitor[J].Journal of Hunan University of Science & Technology(Natural Science Editon),2013,28(1):87-92. |
| |
| Authors: | MA Pei-xun ZHAO Chang-zhi |
| |
| Institution: | 1. Computer Department, Changsha Social Work College, Changsha 410004, China;2.Computer School, National University of Defense Technology ,Changsha 410073, China |
| |
| Abstract: | |
| |
| Keywords: | linear temporal logic anticipatory monitor automaton runtime verification |
|
| 点击此处可从《湖南科技大学学报(自然科学版)》浏览原始摘要信息 |
| 点击此处可从《湖南科技大学学报(自然科学版)》下载免费的PDF全文 |
|
