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 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 guaranteed 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.

Ämnesord

NATURVETENSKAP  -- Data- och informationsvetenskap -- Datavetenskap (datalogi) (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Science -- Computer Science (hsv//eng)

Nyckelord

Datavetenskap

Computer science

Datalogi

Computer science

Publikations- och innehållstyp

rap (ämneskategori)

vet (ämneskategori)