首页 | 本学科首页   官方微博 | 高级检索  
     


Runtime Verification of Timed LTL using Disjunctive Normalized Equation Systems
Authors:Kre Jelling Kristoffersen  Christian Pedersen  Henrik Reif Andersen
Affiliation:aDepartment of Innovation, IT University of Copenhagen, Copenhagen, 2400 NV, Denmark
Abstract:In this paper we present a new framework for runtime verification of properties of real time systems such as financial systems or backend databases. Such a systems has a semantics which resemples that of timed traces, namely a sequence of states where each state consists of predicates true in this state and then a timestamp explaining when the state is valid. We present a logic, LTLt, which is an extension of LTL with time constraints and a freeze quantifier and show how formulae in this logic are able to express properties of bounded liveness and safety which are ideal for these systems. It is shown how a formula in LTLt may be rewritten to a certain disjunctive normal form suitable for checking a real time system at runtime. The normal form captures the essential part of runtime verification by a set of mutually defined formula identifiers, each expressing two things: What should hold now and which formula identifiers that will need to hold in the next state. As part of the theoretical foundation for this work we propose a characterization of Runtime Verification and address the challenges in developing a method which is both sound and complete while at the same time efficient.
Keywords:Timed LTL  Disjunctive Normalized Equation Systems  Charaterization of Runtime Verification  Property Tranformation
本文献已被 ScienceDirect 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号