Monitoring Temporal Properties of Continuous Signals

Monitoring Temporal Properties of Continuous Signals

| Oded Maler and Dejan Nickovic
This paper introduces a variant of temporal logic tailored for specifying desired properties of continuous signals. The logic is based on a bounded subset of the real-time logic MITL, augmented with a static mapping from continuous domains into propositions. From formulae in this logic, property monitors are automatically generated to check whether a given signal of bounded length and finite variability satisfies the property. A prototype implementation was used to check properties of simulation traces generated by Matlab/Simulink. Temporal logic is a formalism for specifying desired behaviors of discrete systems. Verification involves checking whether all state-event sequences generated by a system satisfy a formula. Recently, PSL-Sugar has been adopted as a standard specification language in the hardware industry. For systems outside the scope of automatic verification tools, simulation/testing is preferred. Property monitors can be used to export specification components to simulation. The essence of this approach is the automatic construction of a monitor from the formula, which can be interfaced with the simulator to alert the user if a property is violated. This process is more reliable than manual inspection of simulation traces. Temporal logic has been used in monitoring tools like Temporal Rover, FoCs, Java PathExplorer, and MaCS. Unlike verification, monitoring is usually restricted to finite traces. This paper defines a temporal logic for specifying properties of dense-time real-valued signals and automatically generates property monitors for this language. The motivation is to improve validation methodology for continuous and hybrid systems. The paper introduces MITL_{[a,b]}, a restricted version of MITL, and describes an offline monitoring procedure for MITL_{[a,b]} formulae. It also introduces STL (Signal Temporal Logic), discusses its semantic domain, and shows how monitoring for its formulae can be reduced to monitoring MITL_{[a,b]} formulae via static Boolean abstraction. A prototype implementation on simulation traces generated by Matlab/Simulink is illustrated, followed by discussions of related and future work. The paper also discusses the monitoring of real-valued signals and the extension of the logic to handle such signals. It presents examples of monitoring continuous signals and discusses related work in the field.This paper introduces a variant of temporal logic tailored for specifying desired properties of continuous signals. The logic is based on a bounded subset of the real-time logic MITL, augmented with a static mapping from continuous domains into propositions. From formulae in this logic, property monitors are automatically generated to check whether a given signal of bounded length and finite variability satisfies the property. A prototype implementation was used to check properties of simulation traces generated by Matlab/Simulink. Temporal logic is a formalism for specifying desired behaviors of discrete systems. Verification involves checking whether all state-event sequences generated by a system satisfy a formula. Recently, PSL-Sugar has been adopted as a standard specification language in the hardware industry. For systems outside the scope of automatic verification tools, simulation/testing is preferred. Property monitors can be used to export specification components to simulation. The essence of this approach is the automatic construction of a monitor from the formula, which can be interfaced with the simulator to alert the user if a property is violated. This process is more reliable than manual inspection of simulation traces. Temporal logic has been used in monitoring tools like Temporal Rover, FoCs, Java PathExplorer, and MaCS. Unlike verification, monitoring is usually restricted to finite traces. This paper defines a temporal logic for specifying properties of dense-time real-valued signals and automatically generates property monitors for this language. The motivation is to improve validation methodology for continuous and hybrid systems. The paper introduces MITL_{[a,b]}, a restricted version of MITL, and describes an offline monitoring procedure for MITL_{[a,b]} formulae. It also introduces STL (Signal Temporal Logic), discusses its semantic domain, and shows how monitoring for its formulae can be reduced to monitoring MITL_{[a,b]} formulae via static Boolean abstraction. A prototype implementation on simulation traces generated by Matlab/Simulink is illustrated, followed by discussions of related and future work. The paper also discusses the monitoring of real-valued signals and the extension of the logic to handle such signals. It presents examples of monitoring continuous signals and discusses related work in the field.
Reach us at info@study.space