UC San Diego

The Message Sequence Chart (MSC) is a widely used formalism for specifying behaviors and properties of a component-based system. While they are primarily seen as a design and validation phase artifact in the software development process, their information can play a larger role. In most cases, as the system reaches the implementation phase of development, the gap between the semantics of the implementation and the specification widens. Through component synthesis and verification based on the composition and reuse of MSC artifacts, the system's implementation and specification defects can be captured early on in the development process; thus, reducing the high cost of uncovering a defect at a latter stage. To demonstrate this we use MSCs to verify the implementation of a system in an integrated development environment using a generic state-of-the-art model checker combined with a verification tool we developed