Conferencia impartida por César Sánchez, del Instituto IMDEA Software, Madrid.

Tendrá lugar en el aula 3.0.8 de la ETSI Informática el día 15 de noviembre a las 16:00 h.

 

Título:

Online and Offline Stream Runtime Verification.

 

Resumen: In this talk I will revisit Stream Runtime Verification (SRV).  Stream runtime verification is a formalism to express monitors using streams, which results in a simple and expressive specification language that is not only restricted to describe correctness/failure assertions bit that can also collect richer information (including statistical measures) for system profiling and coverage analysis. The monitors generated in SRV are useful for testing, under actual deployment, and to analyze logs.

 The key idea of Stream Runtime Verification is that the steps in the algorithms to monitor logics (which generate Boolean verdicts) can be generalized to compute richer information if a different data domain is used.  Hence, the keystone of SRV is to separate the temporal dependencies in the monitoring algorithm with the concrete operations performed at each step.  We revisit the pioneer SRV specification language Lola and study online and offline monitoring algorithms.

 The algorithm for online monitoring Lola specifications uses a partial evaluation strategy, by incrementally constructing output streams from input streams, maintaining a store of partially evaluated expressions. We identify syntactically a class of specifications for which the online algorithm is trace length independent, that is, the memory requirement does not depend on the length of the input streams.  Then, we extend the principles of the online algorithm to create an efficient offline monitoring algorithm for large traces, which consist on scheduling trace length independent passes on a dumped log.

 We will finally discuss extensions of SRV to asynchronous (event-based) streams, theoretical results about Boolean SRV, modern implementations of synchronous and asynchronous SRV systems and current and future work.

 

Short bio:

Cesar Sanchez is full (research) professor at the IMDEA Software Institute in Madrid, Spain. He holds a PhD from Stanford University in 2007. He was a postdoc at University of California Santa Cruz before joining the IMDEA Software Institute in 2008.  His current research focuses on applications of logic to computer science and in formal methods for reactive systems, and in particular temporal logics for hyperproperties and runtime verification. His main practical interests are applications of runtime verification to autonomous systems and blockchain and smart-contract reliability.