Felipe Gorostiaga, PhD Student, IMDEA Software Institute
Stream Runtime Verification (SRV) is a specification formalism for temporal properties of reactive systems where observations are described as streams of data computed from input streams of data, which allows a clean separation between the temporal dependencies between incoming events, and the concrete operations that are performed during the monitoring.
However, Stream Runtime Verification languages typically assume that all streams share a global synchronous clock and input events arrive in a synchronous manner. We generalize the time assumption to cover streams whose events are stamped from a real-time domain, but keep the essential explicit time dependencies present in previous synchronous SRV languages.
In this talk I will present Striver, a formalism which shares the simplicity with SRV, mainly due to the separation between the timing reasoning and the data domain.