Resource-bounded runtime verification of Java programs with real-time properties

摘要

Given the intractability of exhaustively verifying software, the use of runtime verification, to verify single execution pathsududat 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 usingududLustre to write security-critical properties, we exploit the language’sudguarantees on bounded resources. We translate these properties intoudthe existing monitoring framework Larva, making monitoring ofudprograms both easily applicable to Java programs and at the sameududtime guarantee to use bounded-resources. We use a subset of Quantified Discrete-time Duration Calculus (QDDC) as an alternativeududspecification notation for real-time properties because it is translatable into Lustre. Thus, QDDC also enjoys the same guarantees givenududwhen using Lustre.