Runtime monitoring of duration calculus assertions for real-time applications

Abstract

An open question which is commonly asked in software development is whether the implemented artefact follows the requirements specified. From the early days of computing, a number of projects, ideas and techniques have been proposed to prove software correctness. One of these techniques is validation, which verifies the system during execution. Duration Calculus is a powerful logic notation that evaluates property satisfaction by applying the Reimann integral over property values within an interval. Therefore, Duration Calculus not only determines whether a property is being satisfied but also the duration of the property satisfiability. Duration Calculus notation considers time as a real valued variable, which together with the evaluation of calculi formulae becomes undecidable. In this dissertation, we restrict the notation to a subset that is decidable, discrete-time and deterministic. The decidability property is important in order to evaluate the system correctness at runtime. On the other hand, the restriction to discrete-time together with the determinism of the notation reduce the side-effects of the inserting observers in the actual system thus guaranteeing the correctness of the verified program. After restricting Duration Calculus notation to the suitable subset of operators, we propose a framework for defining monitors and integrating them with the system code. Our framework allows monitors to be defined using the mathematical notation, which through a pre-compiler is converted to its Lustre semantics and stored inside Abstract Syntax Trees. The synchronous data-flow programming language Lustre is used for the notation semantics because the resource requirements for the monitors can be predetermined. To keep the benefits obtained by using Lustre, the monitoring platform is also defined in Lustre. The final step before executing the system is to integrate the monitors inside the code. The weaving of monitors with the system is performed through the concept of annotated assertions, which are converted into function calls to the Lustre based evaluation engine to determine the properties satisfiability. We conclude our research by showing the concept of Interval Temporal Logic validation as an aspect, within the Aspect-Oriented Programming (AOP) framework. This concept can be used to facilitate the design of more robust and flexible validation engine simply by defining notation semantics.