Runtime verification of fail-uncontrolled and ambient intelligence systems: A uniform approach

We propose an approach for designing, formalizing and implementing, on top of existing MultiAgent Systems and without interfering with them, sentinels that detect errors in fail-uncontrolled multiagent systems, and controllers that identify particular situations in ambient intelligence (AmI) systems. The formalism we use for representing the expected patterns of actions is that of trace expressions extended with features for dealing with exceptions, timeouts, and their handlers. In this paper we provide the syntax and semantics of the extended trace expressions formalism and examples of their use, in the different contexts of fail-uncontrolled and AmI systems