Runtime verification of real-time event streams under non-synchronized arrival

作     者：Leucker, Martin Sanchez, Cesar Scheffel, Torben Schmitz, Malte Schramm, Alexander 

作者机构：Univ Lubeck Inst Software Engn & Programming Languages Lubeck Germany IMDEA Software Inst Madrid Spain 

出 版 物：《SOFTWARE QUALITY JOURNAL》 (软件质量杂志)

年 卷 期：2020年第28卷第2期

页      面：745-787页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：BMBF project ARAMIS II [01 IS 16025] EU H2020 project COEMS Madrid Regional Government [S2018/TCS-4339] Spanish National Project "BOSCO" [PGC2018-102210-B-100] EU H2020 project Elastest H2020 - Industrial Leadership Funding Source: H2020 - Industrial Leadership 

主　　题：Stream runtime verification Monitoring Real-time event streams Formal methods Parallel event processing 

摘      要：We study the problem of online runtime verification of real-time event streams. Our monitors can observe concurrent systems with a shared clock, but where each component reports observations as signals that arrive to the monitor at different speeds and with different and varying latencies. We start from specifications in a fragment of the TeSSLa specification language, where streams (including inputs and final verdicts) are not restricted to be Booleans but can be data from richer domains, including integers and reals with arithmetic operations and aggregations. Specifications can be used both for checking logical properties and for computing statistics and general numeric temporal metrics (and properties on these richer metrics). We present an online evaluation algorithm for the specification language and a concurrent implementation of the evaluation algorithm. The algorithm can tolerate and exploit the asynchronous arrival of events without synchronizing the inputs. Then, we introduce a theory of asynchronous transducers and show a formal proof of the correctness such that every possible run of the monitor implements the semantics. Finally, we report an empirical evaluation of a highly concurrent Erlang implementation of the monitoring algorithm.