Please use this identifier to cite or link to this item:
Title: An LTL proof system for runtime verification
Authors: Cini, Clare
Francalanza, Adrian
Keywords: Aspect-oriented programming
Computer software -- Development
Real-time data processing
Computer programs -- Verification
Discrete-time systems
Object-oriented methods (Computer science)
Issue Date: 2015
Publisher: Springer Berlin Heidelberg
Citation: Cini, C., & Francalanza, A. (2015). An LTL proof system for runtime verification. 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, London. 1-15.
Abstract: We propose a local proof system for LTL formalising deductions within the constraints of Runtime Verification (RV), and show how such a system can be used as a basis for the construction of online runtime monitors. Novel soundness and completeness results are proven for this system. We also prove decidability and incrementality properties for a monitoring algorithm constructed from it. Finally, we relate its expressivity to existing symbolic analysis techniques used in RV.
Appears in Collections:Scholarly Works - FacICTCS

Files in This Item:
File Description SizeFormat 
tacas2015.pdf412.33 kBAdobe PDFView/Open

Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.