Please use this identifier to cite or link to this item:
https://www.um.edu.mt/library/oar/handle/123456789/23158| 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. |
| URI: | https://www.um.edu.mt/library/oar//handle/123456789/23158 |
| Appears in Collections: | Scholarly Works - FacICTCS |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| tacas2015.pdf | 412.33 kB | Adobe PDF | View/Open |
Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.