基于LTL预测语义的高效监控器构造
DOI:
作者:
作者单位:

作者简介:

通讯作者:

基金项目:

国家自然科学基金项目(50875087)


The construction of an LTL-based efficient anticipatory monitor
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
    摘要:

    运行时验证中的一个重要研究内容就是从高层规约生成高效的监控器,并有效控制监控器的生成复杂度与监控器运行时开销.基于线性时序逻辑(LTL)的预测语义,通过删除与合并Büchi自动机中的大部分状态,提出一种高效的预测监控器构造技术.通过该方法,可以大大降低最终预测监控器的规模,提高监控器产生的效率;同时保证把监控器的运行时开销控制在合理的范围内.基于上述预测监控器构造技术,实现了相应工具monitor_tool,该工具比LTL3_tool工具更小,且能够为更多的LTL性质产生监控器. 同时,产生的监控器能够尽可能早的识别一个持续被监控的执行轨迹是否满足指定的正确性性质.

    Abstract:

    To create an efficient monitor with limited complexity and less cost at runtime from top-level specification is very important in research on runtime verification. By deleting and merging most status of Büchi automaton, a new way was proposed to construct an efficient anticipatory monitor which was based on the anticipatory semantics of Linear Temporal Logic (LTL). Through this method, on one hand, much smaller final anticipatory monitor was generated and the efficiency was improved that of the generation of the monitor; On the other hand, the runtime cost of the monitor was control into a reasonable region. A tool named ” monitor_tool” was implemented to check the approach above, it’s more effective than LTL3_tool and able to generate monitors for more LTL properties.Meanwhile,The generated monitor can identify a continuously monitored trace as either satisfying or falsifying a property as early as possible.

    参考文献
    相似文献
    引证文献
引用本文

马佩勋,赵常智.基于LTL预测语义的高效监控器构造[J].湖南科技大学学报(自然科学版),2013,28(1):87-92

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
历史
  • 收稿日期:
  • 最后修改日期:
  • 录用日期:
  • 在线发布日期: 2013-06-09