This small grant for exploratory research investigates a promising new approach to checking the proper execution of software composed of components. An attractive method for developing new reactive software is to use ?off-the-shelf? third-party components that do not, or may not, exactly satisfy the desired requirements. To safely use such components, the use of run-time monitors is used to detect behaviors violating the requirements. Such requirements are usually composed of a safety part, whose run-time monitoring is well studied, and a liveness part, whose run-time monitoring is elusive. Most commonly, run-time monitors extract a safety property, that either over-approximates or under-approximate the original requirements, and thus tend to have a have high level of inaccuracy.
A novel class of methods is proposed that employs randomization for monitoring the liveness properties. Roughly speaking, the method occasionally tosses a coin to determine whether to give up achieving a liveness requirement. Such methods are highly accurate and enjoy the property of graceful degradation: the longer a liveness property is not satisfied, the more likely is it to be rejected by the monitor. The project also investigates novel methods for evaluating the accuracy of monitoring approaches to compare various algorithms. Finally, monitors are usually ?passive? -- they only observe the computation, but do not participate in them ? but this work explores ?active? monitors that cooperate with the component to generate a computation that satisfies the requirements.
