We present hLola, an extensible Stream Runtime Verification (SRV) tool, that borrows from the functional language Haskell (1) rich types for data in events and verdicts; and (2) functional features for parametrization, libraries, high-order specification transformations, etc.

SRV is a formal dynamic analysis technique that generalizes runtime verification algorithms from temporal logics like LTL to stream monitoring, allowing the computation of verdicts richer than Booleans (quantitative values and beyond). The keystone of SRV is a clean separation between temporal dependencies and data computations, but in spite of this theoretical separation previous engines include hardwired implementations of just a few data types, requiring complex changes in the tool chain to incorporate new data types. Also, when previous tools implement features like parametrization these are implemented in a ad-hoc way.

In contrast, hLola implements these features in a natural way borrowing datatypes and functional aspects from Haskell, resulting in an extensible engine. We illustrate hLola through several examples, including a UAV monitoring infrastructure with predictive characteristics that has been validated in actual online runtime verification of mission planning.

HLola: a Very Functional Tool for Extensible Stream Runtime Verification

ETAPS is a confederation of several conferences, each with its own Programme Committee and Steering Committee. ETAPS is the most important and visible annual European event related to software sciences. Altogether, more than 500 researchers participate in this event every year. The confederated conferences cover various aspects of software systems, ranging from theoretical foundations to programming language developments, compiler advancements, analysis tools, formal approaches to software engineering, and security.

A gather.town room will be open during the whole conference, which can be found here:

https://gather.town/app/nSgVv0DDYoCkmdkP/ETAPS2021

Password: Luxembourg2021

This can be used to meet in the coffee breaks.

 PDF's of the papers are available on https://etaps.org/2021/programme