Observing timed systems by means of messages sequence chart graphs

SEBASTIÁN BLAUSTEIN; FERNANDO OLIVETO; VICTOR BRABERMAN

Oregon, EEUU

Conferencia; Poster Session International Conference on Software Engineering; 2002

ACM

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.