The IMDEA Software Institute PhD Student, Felipe Gorostiaga, successfully defended his doctoral Thesis this morning at the UPM’s School of Computer Engineering (ETSIINF) at the Montegancedo Campus. Some of his colleagues were present to listen and show their support.
His Thesis, supervised by César Sánchez, is entitled: “Theory and Practice of Stream Runtime Verification for Sequences and Real-Time Event Based Systems”.
Felipe started the defense stating that software verification is the employment of formal methods to ensure the absence of errors in a program, but whose application is susceptible to become impractical for large and complex systems. By contrast, runtime verification is a technique for software assurance that consists of generating, from a formal specification, a monitor that analyses an execution trace online or offline and detects violations of the specification, which makes this technique more scalable than static verification.
Stream Runtime Verification (SRV) defines specifications declaratively in terms of input and output streams of events that carry data of rich types. One of the main concerns of SRV languages is the clean separation of temporal and data aspects of a specification. In this sense, Gorostiaga commented that most early SRV formalisms, such as the pioneer language Lola, are based on synchronous streams, where data observed at the same index in different streams are considered to have occurred simultaneously.
The first contribution of this Thesis is Striver, a novel SRV language inspired in Lola that handles non-synchronized timestamped event streams. He compared Striver with similar pre-existing formalisms and also exhibit the conditions under which Striver is equally expressive to Lola.
In his work, he shows an algorithm to translate to one another and studies the performance of the translated specifications both theoretically and empirically.
The second contribution of this Thesis is the implementation of Lola and Striver using “lift-deep embedding”, a novel technique that permits to effectively fulfill the promise of a straightforward addition and usage of arbitrary data types in the languages, which he demonstrates empirically employing the tools over a wide range of application domains.
Lastly, he also presented new extensions to both languages that amplify their expressive power and give rise to a new class of specifications.
