Seminar details

Abstract: Component-based design is the process leading from given requirements and a set of predefined components to a system meeting the requirements. Components are abstract building blocks encapsulating behavior. They can be composed in order to build composite components. Their composition should be rigorously defined so that it is possible to infer the behavior of composite components from the behavior of their constituents as well as global properties from the properties of individual components. It is, however, generally not possible to ensure or verify the desired property using static verification techniques such as model-checking or static analysis, either because of the state-space explosion problem or because the property can only be decided with information available at runtime (e.g., from the user or the environment). Runtime Verification (RV) is an umbrella term denoting the languages, techniques, and tools for the dynamic verification of system executions against formally-specified behavioral properties. In this context, a run of the system under scrutiny is analyzed using a decision procedure: a monitor. Generally, the monitor may be generated from a user-provided specification (e.g., a temporal-logic formula, an automaton), performs a step-by-step analysis of an execution captured as a sequence of system states, and produces a sequence of verdicts (truth-values taken from a truth-domain) indicating specification satisfaction or violation.
This thesis addresses the problem of runtime monitoring multi-threaded and distributed component-based systems with multi-party interactions (CBSs). Although, neither the exact model nor the behavior of the system is known (black box system), the semantic of such CBSs can be modeled with labeled transition systems (LTSs). Inspiring from conformance testing theory, we refer to this as the monitoring hypothesis. Our monitoring hypothesis makes our approach oblivious of (i) the behavior of the CBSs, and (ii) how this behavior is obtained. We consider a general abstract semantic model of CBSs consisting of a set of intrinsically independent components whose interactions are managed by several schedulers. Using such an abstract model, one can obtain systems with different degrees of parallelism, such as sequential, multi-threaded and distributed systems. When monitoring concurrent (multi-threaded and distributed) CBSs, the problem that arises is that a global state of the system is not available at runtime, since the schedulers execute interactions even by knowing the partial state of the system. Moreover, in distributed systems, the total ordering of the execution of the interaction is not observable. A naive solution to these problems would be to plug in a monitor which would, however, force the system to synchronize in order to obtain the sequence of global states as well as the total ordering of the executions at runtime Such a solution would defeat the whole purpose of having concurrent executions and distributed systems.
We define two approaches for the monitoring of multi-threaded and distributed CBSs. In both approaches, we instrument the system to retrieve the local events of the schedulers. Local events are sent to an online monitor which reconstructs on-the-fly the set of global traces that are i) compatible with the local traces of the schedulers, and ii) suitable for monitoring purposes, in a concurrency-preserving fashion.
Monitoring multi-threaded CBSs. In the multi-threaded setting, the interactions are executed concurrently with a centralized scheduler. In this setting, we address the problem of online monitoring of any logic-independent linear-time user-provided properties in multi-threaded CBSs described in the BIP (Behavior, Interaction, Priority) framework. BIP is an expressive framework for the formal construction of heterogeneous systems. Our technique reconstructs on-the-fly the global states by accumulating the partial states traversed by the system at runtime. We define transformations of components that preserve their semantics and concurrency and, at the same time, allow to monitor global-state properties. We present RVMT-BIP, a prototype tool implementing the transformations for monitoring multi-threaded BIP systems. Our experiments on several multi-threaded BIP systems show that RVMT-BIP induces a cheap runtime overhead.
Monitoring distributed CBSs. In the distributed setting the interactions are executed concurrently with several schedulers. Moreover, simultaneous execution of interactions by several schedulers is possible. In this setting, we address the problem of runtime monitoring of distributed CBSs against user-provided properties expressed in linear-temporal logic and referring to global states. In this context, the reconstruction of the global traces is done on-the-fly using a lattice of partial states encoding the global traces compatible with the locally-observed traces. We implemented our monitoring approach in a prototype tool called RVDIST. RVDIST executes in parallel with the distributed system and takes as input the events generated from each scheduler and outputs the evaluated computation lattice. Our experiments show that thanks to the optimization applied in the online monitoring algorithm, (i) the size of the constructed computation lattice is insensitive to the number of received events, (ii) the lattice size is kept reasonable and (iii) the overhead of the monitoring process is cheap.