The good, the bad, and the ugly, but how ugly is ugly?

被引:0
|
作者
Bauer, Andreas [1 ]
Leucker, Martin [2 ]
Schallhart, Christian [2 ]
机构
[1] Natl ICT Australia, Canberra, ACT, Australia
[2] Tech Univ Munich, Inst Informat, D-80290 Munich, Germany
来源
RUNTIME VERIFICATION | 2007年 / 4839卷
关键词
D O I
暂无
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
When monitoring a system wrt. a property defined in some temporal logic, e. g., LTL, a major concern is to settle with an adequate interpretation of observable system events; that is, models of temporal logic formulae are usually infinite streams of events, whereas at runtime only prefixes are available. This work defines a four-valued semantics for LTL over finite traces, which extends the classical semantics, and allows to infer whether a system behaves (1) according to the monitored property, (2) violates the property, (3) will possibly violate the property in the future, or (4) will possibly conform to the property in the future, once the system has stabilised. Notably, (1) and (2) correspond to the classical semantics of LTL, whereas (3) and (4) are chosen whenever an observed system behaviour has not yet lead to a violation or acceptance of the monitored property. Moreover, we present a monitor construction for RV-LTL properties in terms of a Moore machine signalising the semantics of the so far obtained execution trace.
引用
收藏
页码:126 / +
页数:3
相关论文
共 50 条