System Monitoring with Extended Message

Abstract. Runtime verification is a lightweight formal verification tech-nique that checks the correctness of the behaviour of a system. A problem with this technique is that most monitoring specification languages are not actually used in practice by system designers. To avoid this prob-lem, we propose an monitoring approach on basis of an extension of live sequence charts (LSCs). We extend the standard LSCs as proposed by Damm and Harel by introducing the notation of “sufficient prechart”, and by adding concatenation and product of charts. In this approach, a monitor solves the word problem that whether an observed behaviour of the underlying system is accepted by an extended LSC (eLSC) property. An on-line monitoring algorithm will be presented in the full version of the paper. 1 Intorduction Runtime verification [3] is proposed for checking whether the behaviour of a system satisfies a correctness property. When compared to mode