Safe Runtime Verification of Real-Time Properties

Abstract. Introducing a monitor on a system typically changes the system's behaviour by slowing the system down and increasing memory consumption. This may possibly result in creating new bugs, or possibly even `fixing' bugs, only to reappear as the monitor is removed. Properties written in a real-time logic, such as duration calculus, can be particularly sensitive to such changes induced through monitoring. The same problem occurs in other scenarios such as when a system is ported to a faster machine. In this paper, we identify a class of real-time properties, in duration calculus, which are monotonic under the slowing down (speeding up) of the underlying system. We apply this approach to the real-time runtime monitoring tool Larva, where we use duration calculus as a monitoring property specification language, so we automatically identify properties which can be shown to be monotonic with respect to system re-timing.

• Type: Conference
• Year: 2009
• Where: FORMATS
• Authors: Christian Colombo, Gordon J. Pace, Gerardo Schneider
• Keywords: Duration Calculus, Formal Methods, FORMATS 2009, Memory Consumption, System's Behaviour