Observing timed systems by means of Message Sequence Chart Graphs

Summary form only given. Tools that feature MSC do not have the ability to check model or implementation executions against the specified behavior. 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). 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 (Alur and Yannakakis, 1999) (i.e. based on partial orders). Those MSC-Graphs are enriched with timers and delay intervals in a similar way to (Ben-Abdallah and Leue, 1997) and (Li and Lilius, 1999).