Monitoring Temporal Logic Specifications Combined with Time Series Constraints
MetadataShow full item record
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.
Showing items related by title, author, creator and subject.
On-line Monitoring of Metric Temporal Logic with Time- Series Constraints Using Alternating Finite Automata Drusinsky, Doron (2006);In this paper we describe a technique for monitoring and checking temporal logic assertions augmented with real-time and time-series constraints, or Metric Temporal Logic Series (MTLS). The method is based on Remote ...
Spectrum analysis of easterly waves in the tropical Pacific during two contrasting periods of sea-surface temperature anomalies Chang, C.-P.; Miller, Charles Robert (Monterey, California. Naval Postgraduate School, 1976-07); NPS-63Cj76071The structure and properties of the tropical easterly waves has been found to vary considerably between different regimes and time periods. This study investigates the possible roles played by the temporal and spatial ...
Drusinsky, Doron; Havelund, Klaus (2003-01);Execution-based model checking (EMC) is a verification technique based on executing a multi-threaded/multiprocess program repeatedly in a systematic manner in order to explore the different interleavings of the program. ...