References on this page have the following semantics: BX (resp. ChX, JX, CX) refers to the book, chapter, journal paper, conference paper with index X as in my Publications webpage.
Monitoring comprises the set of theories, techniques, and tools for the formal verification and enforcement of specifications on a system using runtime information [B1, Ch1-3]. Specifications are usually formalized as properties expressed in formal specification languages such as variants/extensions of finite-state automata, variants/extensions of linear temporal logic, or rewriting rules. While in runtime verification one is interested in providing verdicts reflecting the satisfaction/violation of the specification, in runtime enforcement [C8, Ch4] one tries to steer the system to ensure satisfaction and avoid violation of the specification. I am interested in both the theoretical aspects of runtime verification/enforcement and their applications to several sorts of systems such as component-based, distributed, and real-time systems, as well as systems used in industry and public systems.
My previous research activities can be organized into five topics.
Theoretical Aspects of Monitoring – Topic 1
We studied the expressiveness of techniques for verifying systems at runtime [Ch2] such as runtime verification [J3], runtime enforcement [J1], and testing [J2] and revisited the definitions and characterizations of monitorable, enforceable, and testable properties with respect to the safety-progress classification of properties. We also contributed to the definition of expressive specification formalisms and monitors with the definition of Quantified Event Automata [C11] which are monitors with transitions labeled by events that can carry data, internal variables, and advanced event matching mechanisms. We have also defined the first framework for certified runtime verification [C13] where one can obtain monitors that are certified by a theorem prover.
Decentralized Monitoring – Topic 2
We have introduced decentralized runtime verification [C12]. In this context, the system under scrutiny is composed of several entities and the classical central observation point required for monitoring does not exist. Instead, one has to attach local monitors to local entities and define communication strategies for monitors to exchange information. First, we investigated frameworks where monitors migrate across components of the system, first when monitors are encoded by LTL formulae [J9] or finite-state automata [C23]. Then, we defined frameworks where monitors follow choreography driven by the monitored specification [C24, J10]. Finally, we generalized previous work by defining the notion of a decentralized specification and an analytical framework to design and compare algorithms for decentralized runtime verification [C43].
Runtime Enforcement – Topic 3
We wrote a tutorial/survey on runtime enforcement [C8]. We have defined frameworks for untimed [J1, C5] and timed [C16, J6] runtime enforcement. Untimed runtime enforcement monitors are not sensitive to the time elapsing between events and only account for the logical time between events. Timed enforcement monitors account for the physical time which elapses between events and influences the truth value of the enforced property. Defining timed enforcement monitors involve studying more complex relationship involving physical time between the input and output traces of enforcement monitors. In [J8], we introduced models of enforcement monitors generalizing those available in the literature. We later extended the monitors in [J8] to account for uncontrollable events in [J2]. We used game theory as an alternative to synthesize the state space of enforcement monitors ahead of time (and thus reduce runtime computation) [C42]. We pioneered runtime enforcement for safety and co-safety timed properties in [C16] by defining enforcement monitors as delayers. We later extended enforcement monitoring to any regular timed property in [C21] and endowed enforcement monitors with suppression abilities. Optimal enforcement monitors for timed properties with uncontrollable events were introduced in [J16]. Our theoretical results on runtime enforcement of timed properties were implemented in the TiPeX tool [C31].
Monitoring Component-Based Systems – Topic 4
We have also contributed to the definition of runtime verification and enforcement for component-based systems (CBSs). CBSs consist of existing components composed using interactions. From a runtime verification perspective, dealing with CBSs offers the advantage of having a more precise description of the system under scrutiny. However, CBSs are endowed with more complex and subtle behavior than traditional monolithic systems. For CBSs, we defined a runtime verification framework for sequential [C10, J4] and multithreaded CBSs [J12], runtime enforcement of sequential CBSs [C29, J7], and efficient instrumentation techniques [C39, J20] where we ported aspect-oriented programming to CBSs.
Monitoring for Application Domains – Topic 5
I am also interested in applying runtime verification and enforcement principles to concrete application domains and case studies. I have also co-organized workshops on the specific topic of applications for runtime verification and enforcement. We defined runtime verification and enforcement approaches in security by defining monitors that verify and enforce the so-called notion of opacity of secrets [C19, J5]. We designed and implemented concrete verification and enforcement monitors for Android devices [C17, 32] by relying on an adaptation of aspect-oriented programming to Android [C14]. We conducted case studies on using these monitors for blocking advertisement and preserving user privacy in Android apps [C26]. Other applications of runtime verification and enforcement in which I was involved in include the mitigation of DMA races [C27], the enforcement of document life cycles [C40, J19], and the monitoring of electronic exams [C30, J15].