Please use this identifier to cite or link to this item:
https://www.um.edu.mt/library/oar/handle/123456789/24163| Title: | Resource-bounded runtime verification of Java programs with real-time properties |
| Authors: | Colombo, Christian Pace, Gordon J. Schneider, Gerardo |
| Keywords: | Aspect-oriented programming Computer software -- Development Real-time data processing Computer security |
| Issue Date: | 2009 |
| Publisher: | University of Malta. Faculty of Information and Communication Technology |
| Citation: | Colombo, C., Pace, G. J., & Schneider, G. (2009). Resource-bounded runtime verification of java programs with real-time properties. (No. CS2009-01). Msida. |
| Abstract: | Given the intractability of exhaustively verifying software, the use of runtime verification, to verify single execution paths at runtime, is becoming increasingly popular. Undoubtedly, the overhead introduced by runtime verification is a concern for system developers planning to introduce this technique in their work. By using Lustre to write security-critical properties, we exploit the language’s guarantees on bounded resources. We translate these properties into the existing monitoring framework Larva, making monitoring of programs both easily applicable to Java programs and at the same time guarantee to use bounded-resources. We use a subset of Quantified Discrete-time Duration Calculus (QDDC) as an alternative specification notation for real-time properties because it is translatable into Lustre. Thus, QDDC also enjoys the same guarantees given when using Lustre. |
| URI: | https://www.um.edu.mt/library/oar//handle/123456789/24163 |
| Appears in Collections: | Scholarly Works - FacICTCS |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| Resource-Bounded_Runtime_Verification_of_Java_Prog.pdf | 191.81 kB | Adobe PDF | View/Open |
Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.