Monitoring modulo theories
Monitoring modulo theories
复制标题
监控模理论
DOI：
10.1007/s10009-015-0380-3
复制
发表时间：
2014
影响因子：
1.5
通讯作者：
Daniel Thoma
中科院分区：
文献类型：
--
作者：
Normann Decker;M. Leucker;Daniel Thoma
本文考虑了一种通用的方法来运行时验证的时间属性超过一阶理论。这特别允许多线程、面向对象系统的验证。它提出了一个一般框架提升监控综合过程命题时序逻辑的时序逻辑结构内的一些一阶理论。为了评估这样的规格SMT解决和经典的监测命题的时间属性相结合。监控程序实现的线性时间时序逻辑的基础上的Z3 SMT求解器和运行时性能进行评估。
This paper considers a generic approach to runtime verification of temporal properties over first-order theories. This allows especially for the verification of multi-threaded, object-oriented systems. It presents a general framework lifting monitor synthesis procedures for propositional temporal logics to a temporal logic over structures within some first-order theory. To evaluate such specifications SMT solving and classical monitoring of propositional temporal properties are combined. The monitoring procedure was implemented for linear-time temporal logic based on the Z3 SMT solver and evaluated regarding runtime performance.