Please use this identifier to cite or link to this item:
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.
Appears in Collections:Scholarly Works - FacICTCS

Files in This Item:
File Description SizeFormat 
Resource-Bounded_Runtime_Verification_of_Java_Prog.pdf191.81 kBAdobe PDFView/Open

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