基于监控器的LTL公式可监控性判定算法
投稿时间:2018-05-14  修订日期:2018-06-06  点此下载全文
引用本文:
摘要点击次数: 291
全文下载次数: 0
作者单位邮编
吴逸凡 南京航空航天大学 计算机科学与技术学院 211106
陈哲* 南京航空航天大学计算机科学与技术学院 211106
中文摘要:在运行时验证等领域,线性时序逻辑被用来描述约束。但并非所有的线性时序逻辑公式都可以用于验证,如果一个公式不可监控,那么将它用于运行时验证领域就是没有意义的。可监控性要求在运行时验证中的任意时刻,均存在有限步的延伸使得事件序列满足或违反公式。可监控性的要求较为严格,在运行时验证中,实际只关心当前状态是否存在有限步的延伸使得公式被满足,因此本文提出了弱可监控性。当前,针对可监控性问题的研究主要集中在理论层面,为此,本文设计了一种基于监控器的弱可监控性及可监控性判定算法,并实现了一款弱可监控性及可监控性的判定工具monic。
中文关键词:线性时序逻辑  可监控性  弱可监控性  监控器  
 
The monitorability decision algorithm of LTL formula based on monitor
Abstract:In runtime verification and some other fields, linear temporal logic is used to describe constraint. But not all formulas can be used in verification. It’s meaningless if a formula without monitorability is used in verification. Monitorability request there are some finite extension make event sequence satisfy formula at any time in runtime verification. Monitorability is strict, actually, the concern of runtime verification is if there are some finite extensions of current state make the event sequence satisfy formula, so in this article we put forward weakly-monitorability. Now, the research on monitorability focus on theory, so in this article, we design an algorithm which is based on monitor to decide monitorability and weakly-monitorability, and we implement this algorithm in monic.
keywords:Linear temporal logic  Monitorability  Weakly-monitorability  Monitor  
查看全文   查看/发表评论   下载pdf阅读器