| 摘要: |
| 运行时验证中的一个重要研究内容就是从高层规约生成高效的监控器,并有效控制监控器的生成复杂度与监控器运行时开销.基于线性时序逻辑(LTL)的预测语义,通过删除与合并Büchi自动机中的大部分状态,提出一种高效的预测监控器构造技术.通过该方法,可以大大降低最终预测监控器的规模,提高监控器产生的效率;同时保证把监控器的运行时开销控制在合理的范围内.基于上述预测监控器构造技术,实现了相应工具monitor_tool,该工具比LTL3_tool工具更小,且能够为更多的LTL性质产生监控器. 同时,产生的监控器能够尽可能早的识别一个持续被监控的执行轨迹是否满足指定的正确性性质. |
| 关键词: 线性时序逻辑 预测监控器 自动机 运行时验证 |
| DOI： |
| 分类号:TP311 |
| 基金项目:国家自然科学基金项目(50875087) |
|
| The construction of an LTL-based efficient anticipatory monitor |
|
MA Pei-xun1,ZHAO Chang-zhi21,2
|
|
1. Computer Department, Changsha Social Work College, Changsha 410004, China;2.Computer School, National University of Defense Technology ,Changsha 410073, China
|
| 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 LTL3_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. |
| Key words: linear temporal logic anticipatory monitor automaton runtime verification |
