Proving and explaining the unfeasibility of message sequence charts for hybrid systems

Networks of Hybrid Automata are a clean modelling framework for complex systems with discrete and continuous dynamics. Message Sequence Charts (MSCs) are a consolidated language to describe desired behaviors of a network of interacting components. Techniques to analyze the feasibility of an MSC over a given HA network are based on specialized bounded model checking techniques, and focus on efficiently constructing traces of the network that witness the MSC behavior. Unfortunately, these techniques are unable to deal with the "unfeasibility" of the MSC, i.e. that no trace of the network satisfies the MSC. In this paper, we tackle the problem of MSC unfeasibility: first, we propose specialized techniques to prove that an MSC can not be satisfied by any trace of a given HA network; second, we show how to explain why an MSC is unfeasible. The approach is cast in an SMT-based verification framework, using a local time semantics, where the timescales of the automata in the network are synchronized upon shared events. In order to prove unfeasibility, we generalize k-induction to deal with the structure of the MSC, so that the simple path condition is localized to each fragment of the MSC. The explanations are provided as formulas in the variables representing the time points of the events of the MSCs, and are generated using unsatisfiable core extraction and interpolation. An experimental evaluation demonstrates the effectiveness of the approach in proving unfeasibility, and the adequacy of the automatically generated explanations.