Energy shields are adaptive probabilistic controllers using energy functions to ensure runtime fairness with short-term safety and long-term liveness guarantees.
Real-time Stream-based Monitoring
2 Pith papers cite this work. Polarity classification is still indexing.
abstract
We introduce RTLola, a new stream-based specification language for the description of real-time properties of reactive systems. The key feature is the integration of sliding windows over real-time intervals with aggregation functions into the language. Using sliding windows we can detach fixed-rate output streams from the varying rate input streams. We provide an efficient evaluation algorithm of the sliding windows by partitioning the windows into intervals according to a given monitor frequency. For useful aggregation functions, the intervals allow a more efficient way to compute the aggregation value by dynamically reusing interval summaries. In general, the number of input values within a single window instance can grow arbitrarily large disallowing any guarantees on the expected memory consumption. Assuming a fixed monitor output rate, we can provide memory guarantees which can be computed a-priori. Additionally, for specifications using certain classes of aggregation functions, we can perform a more precise, better memory analysis. We demonstrate the applicability of the new language on practical examples.
verdicts
UNVERDICTED 2representative citing papers
Authors introduce abstract event streams for gaps in non-synchronized timed traces and a translation of TeSSLa specs that propagates uncertainty to produce sound outputs on partial information.
citing papers explorer
-
Energy Shields for Fairness
Energy shields are adaptive probabilistic controllers using energy functions to ensure runtime fairness with short-term safety and long-term liveness guarantees.
-
Runtime Verification For Timed Event Streams With Partial Information
Authors introduce abstract event streams for gaps in non-synchronized timed traces and a translation of TeSSLa specs that propagates uncertainty to produce sound outputs on partial information.