Title: Time in message sequence charts: A formal approach
Abstract: Message Sequence Charts (MSC) is a graphical trace language for description and specification of communication behaviour of system components and their environment by means of message interchange. The goal of this paper is to provide a formal semantics for time aspects of MSC. Proposed semantics is based on Timed Maude which is an object-oriented real-time language. It extends a Maude semantics designed for the “untimed” part of basic MSC. We show how Timed Maude can be used to specify timers, and how they can be used to specify timing of an action, and timing imposed on message deliverance.