科研之友
微信
新浪微博
Facebook
分享链接
摘要
在运行时验证中,对于给定的线性时序逻辑公式,常用其可监控性和弱可监控性来衡量其是否适合用于运行时验证.而实际上,可监控性的要求过于严格,弱可监控性解决的又仅仅是一个"存在"问题.为了量化公式的可监控性和弱可监控性,本文提出了概率可监控性,并给出了根据其定义进行求解的方法.此外,本文还提出了基于马尔可夫链的概率可监控性求解算法,并将该算法分别基于概率模型检测器PRISM和SMT求解器进行了代码实现.实验结果表明,基于马尔可夫链的概率可监控性求解算法是正确的,且基于SMT求解器实现的算法效率明显高于基于PRISM实现的算法效率.
-
单位南京航空航天大学; 工业和信息化部
