Observing timed systems by means of message sequence chart graphs

Abstract

Tools that feature MSC do not have the ability to check model or implementation executions against the specified behavior.In this paper, we present a method for observing the behavior of timed systems specified using Message Sequence Chart Graphs (MSC-Graphs) (a simplified version of ITU Z.120 notation [5]).We believe that a log-analyzer and a run-time monitor based on MSC-Graphs are practical and powerful tools to improve the quality of Real-Time systems. On one hand, the log analyzer can play the role of an Oracle while testing non-functional requirements. On the other hand, the run-time monitor can help in the verification of protocol assertions given in terms of message interchange annotated with time constraints.The work is built over a formal definition of the syntax and semantics of MSC-Graphs, which is similar to [1] (i.e. based on partial orders). Those MSC-Graphs are enriched with timers and delay intervals in a similar way to [2] and [3].The work will mainly feature:• An algorithm to check whether a time stamped log conforms a specification given by means of a MSC-Graph. The MSC-graph does not need to be safe realizable [4] or bounded [1] to be treated by our algorithm. The proof of coorectness is given incrementally following a series of is given incrementally following a series of enhancements, starting from a basic algorithm.• Software architecture and an implementation for a log analyzer and a monitoring system.Integration with existing tools supporting MSCs (i.e.: Teleogic Tau [6], Rational Rose Real Tiem [7], rhapsody [8], distributed middlewares, etc.).Coverage reporting over MSC-Graphs.