ABSTRACT. Advances in computation and communication technologies have fueled the recent rise in intelligent cyber-physical systems. Such systems with interconnected computational, or cyber, elements able to sense and control their physical environment now increasingly have a level of artificial intelligence embedded in them. With these advances in autonomy, such systems will be able to cooperate and collaborate with humans and other artificial agents, potentially in situations they have never encountered before. Examples include autonomous cars coming up with ad hoc rules of collaboration at run time in order to navigate an intersection. For such systems, ensuring not just their correct design but their correct operation in presence of all unforeseen operating scenarios will be a research grand-challenge. Traditional pre-deployment model-based design and formal analysis approaches need to be broadened to ensure post-deployment model-based operation in presence of online reconfigurations and the unknowns. On the other hand, runtime simulation and analysis approaches such as the use of digital twins provide new opportunities for creating value via workflows such as simulation of what-if scenarios and predictive maintenance, while the system is already in operation. In this talk we outline research challenges in this domain, survey some promising recent work particularly from the formal specification and simulation-based approaches in the research literature that has recently made its way to industry tools, and where there are opportunities to bridge the gap between research and practice.

ABSTRACT. In Runtime Verification (RV), monitoring a program means checking an execution trace of the program for satisfactions and violations of properties. The question of which properties can be effectively monitored over ideal channels has mostly been answered by prior work. However, program monitoring is often deployed for remote systems where communications may be unreliable. In this work, we address the question of what properties are monitorable over an unreliable communication channel. We describe the different types of mutations that may be introduced to an execution trace and examine their effects on program monitoring. We propose a fixed-parameter tractable algorithm for determining the immunity of a finite automaton to a trace mutation and show how it can be used to classify omega-regular properties as monitorable over channels with that mutation.

ABSTRACT. We consider the problem of Runtime Verification (RV) based on Propositional Linear Temporal Logic (LTL) with both future and past temporal operators. We generalize the framework to monitor partially observable systems using models of the system under scrutiny (SUS) as assumptions for reasoning on the non-observable or future behaviors of the SUS. The observations are generic predicates over the SUS, thus supporting both static and dynamic sets of observables. Furthermore, the monitors are \emph{resettable}, i.e. able to evaluate the monitoring properties at arbitrary positions of the input trace (roughly speaking, [u,i |= phi] can be evaluated for any u and i with the underlying assumptions taken into account). We present a symbolic monitoring algorithm that can be efficiently implemented in BDD. It is proved correct and the output monitor is double-checked by model checking. As a by-product, we also give the first automata-based monitoring algorithm for Past-Time LTL. Beside showing the feasibility and effectiveness of our RV approach, we also demonstrate that, under certain assumptions the resulting monitors are predictive.

ABSTRACT. Runtime Verification (RV) studies how to analyze execution traces of a system under observation. Stream Runtime Verification (SRV) applies stream transformations to obtain information from observed traces. Incomplete traces with information missing in gaps pose a common challenge when applying RV and SRV techniques to real world systems as RV approaches typically require the complete trace without missing parts. This paper presents a solution to perform SRV on incomplete traces based on abstraction. We use TeSSLa as specification language for non-synchronized timed event streams and define abstract event streams representing the set of all possible traces that could have occurred during gaps in the input trace. We show how to translate a TeSSLa specification to its abstract counterpart that can propagate gaps through the transformation of the input streams and thus generate sound outputs even if the input streams contain gaps and events with imprecise values. The solution has been implemented as a set of macros for the original TeSSLa and an empirical evaluation shows the feasibility of the approach.

ABSTRACT. We study the problem of decentralized monitoring of stream runtime verification specifications. % Decentralized monitoring consists of organizing a monitoring activity to be performed by distributed components that communicated using a synchronous network, a communication setting common in many cyber-physical systems like automotive CPSs. % Previous approaches to decentralized monitoring were restricted to LTL and similar logics whose monitors compute Boolean verdicts. % We present here an algorithm that solves the decentralized monitoring problem for the more general setting of stream runtime verification. % Additionally, our algorithm handles network topologies were previous work assumed a network in which all nodes can communicate directly.

Our algorithm is able to reach verdicts efficiently by exploiting partial evaluation strategies, expression simplifiers and advanced communication strategies. % Finally, we present the results of an empirical evaluation of an implementation and compare the expressive power and efficiency against state-of-the-art decentralized monitoring tools like Themis.