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

Författare och institution:

Christian Colombo (-); Gordon J. Pace (-); Gerardo Schneider (Institutionen för tillämpad informationsteknologi (GU))

Antal sidor:

Publikationstyp:

Rapport

Förlag:

University of Malta

Förlagsort:

Malta

Publiceringsår:

2009

Språk:

engelska

Fulltextlänk:

http://folk.uio.no/gerardo/report-Malta-CS2009-01.pdf

Sammanfattning (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 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.

Ämne (baseras på Högskoleverkets indelning av forskningsämnen):

NATURVETENSKAP ->
Data- och informationsvetenskap ->
Datavetenskap (datalogi)
NATURVETENSKAP ->
Data- och informationsvetenskap ->
Datavetenskap (datalogi) ->
Datalogi

Postens nummer:

102888

Posten skapad:

2009-12-06 10:40

Visa i Endnote-format

Utskriftsformat