ABSTRACT Symbolic Message Sequence Charts

Message Sequence Charts (MSCs) are a widely used visual formalism for scenario-based specifications of distributed reactive systems. In its conventional usage, an MSC captures an interaction snippet between concrete objects in the system. This leads to voluminous specifications when the system contains several objects that are behaviorally similar. In this paper, we propose a lightweight syntactic and semantic extension of MSCs, called Symbolic MSCs or SMSCs, where an MSC lifeline can denote some/all objects from a collection. Our extensions give us substantially more modeling power. Moreover, we present a symbolic execution semantics for (structured collections of) our extended MSCs. This allows us to validate MSC-based system models capturing interactions between large, or even unbounded, number of objects. Since our extensions are only concerned with MSC lifelines, we believe that they can be integrated into existing standards such as UML 2.0