Monitoring Temporal Logic Specifications Combined with Time Series Constraints
Authors
Drusinsky, Doron
Shing, Man-Tak
Subjects
Temporal Logic
Run-time Execution Monitoring
Rapid Prototyping
Executionbased Model Checking
Real-time Systems
Run-time Execution Monitoring
Rapid Prototyping
Executionbased Model Checking
Real-time Systems
Advisors
Date of Issue
2003
Date
Publisher
Language
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.
Type
Article
Description
Series/Report No
Department
Computer Science (CS)
Organization
Identifiers
NPS Report Number
Sponsors
Funder
Format
Citation
Journal of Universal Computer Science, vol. 9, no. 11 (2003), 1261-1276
Distribution Statement
Rights
This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.