Monitoring Temporal Logic Specifications Combined with Time Series Constraints

Doron Drusinsky (Naval Postgraduate School and Time-Rover, Inc., USA)

Man-Tak Shing (Naval Postgraduate School California, USA)

Abstract: Run-time monitoring of temporal properties and assertions is used for testing and as a component of execution-based model checking techniques. Traditional run-time monitoring however, is limited to observing sequences of pure Boolean propositions. This paper describes tools for observing temporal properties over time series, namely, sequences of propositions with constraints on data value changes over time. Using such Temporal Logic with time Series (TLS), it is possible to monitor important properties such as stability, monotonicity, temporal average and sum values, and temporal min/max values. The specification and monitoring of linear time temporal logic with real-time and time series constraints are supported by the Temporal Rover and the DBRover, which are in-process and remote run-time monitoring tools. The novel TLS extension described in this paper is based on practical experience and feedback provided by NASA engineers after using the DBRover to verify flight code. The paper also presents a novel hybrid approach to verify timing properties in rapid system prototyping that combines the traditional schedulability analysis of the design and the monitoring of timing constraint satisfaction during prototype execution based on a time-series temporal logic. The effectiveness of the approach is demonstrated with a prototype of the fish farm control system software.

Keywords: Execution-based Model Checking, Rapid Prototyping, Real-time Systems, Run-time Execution Monitoring, Temporal Logic

Categories: D.2.1, D.2.4, D.2.5, D.2.6, D.3.1, F.3.1