线性时序逻辑公式的可监控性量化算法  

Quantitative Algorithm for Deciding Monitorability of Linear Temporal Logic

作　　者：陈云云 陈哲[1,2,3] CHEN Yun-yun;CHEN Zhe(Department of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China;Collaborative Innovation Center of Novel Software Technology and Industrialization,Nanjing 211106,China;Key Laboratory of Safety-Critical Software,Ministry of Industry and Information Technology,Nanjing 211106,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京211106 [2]软件新技术与产业化协同创新中心,南京211106 [3]高安全系统的软件开发与验证技术工业和信息化部重点实验室,南京211106

出　　处：《小型微型计算机系统》2020年第11期2413-2419,共7页Journal of Chinese Computer Systems

基　　金：国家自然科学基金委员会-中国民航局民航联合研究基金项目(U1533130)资助;高安全系统的软件开发与验证技术工业和信息化部重点实验室开放基金项目(XCA18164-02)资助.

摘　　要：在运行时验证中,对于给定的线性时序逻辑公式,常用其可监控性和弱可监控性来衡量其是否适合用于运行时验证.而实际上,可监控性的要求过于严格,弱可监控性解决的又仅仅是一个“存在”问题.为了量化公式的可监控性和弱可监控性,本文提出了概率可监控性,并给出了根据其定义进行求解的方法.此外,本文还提出了基于马尔可夫链的概率可监控性求解算法,并将该算法分别基于概率模型检测器PRISM和SMT求解器进行了代码实现.实验结果表明,基于马尔可夫链的概率可监控性求解算法是正确的,且基于SMT求解器实现的算法效率明显高于基于PRISM实现的算法效率.Monitorability and weak monitorability are often used to measure whether a given linear temporal logic formula is suitable for runtime verification.However,monitorability is too restrictive for practical runtime verification,and weak monitorability solves only an″existence″problem.In this paper,we propose a new notion of probabilistic monitorability to quantify the monitorability and weak monitorability of a formula.We then introduce a new Markov-chain-based algorithm for computing probabilistic monitorability,and implement it using PRISM and SMT solvers.Experimental results show that our algorithm is correct,and the SMT-solver-based implementation is significantly more efficient than the PRISM-based implementation.

关 键 词：线性时序逻辑 运行时验证 可监控性 概率可监控性 马尔可夫链 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]