Using Message Sequence Charts for Component-Based Formal Verification
Bernd Finkbeiner and Ingolf Krüger
Message sequence charts (MSCs) are are a popular tool to informally explain the behavioral embedding of a component in its environment. In this paper we investigate if MSCs can also serve as a specification and reasoning technique for the composition of systems from components. We identify three challenges: (1) Semantic Duality: MSCs express global coordination properties as well as requirements on individual components for their correct participation in an interaction pattern. We show that the two semantics do not always agree and suggest syntactic constraints that ensure the represented property can be decomposed. (2) Completeness: we define a decompositional proof rule based on MSCs. We show that the rule is incomplete and discuss reasons and possible improvements. (3) Compositionality: in component-oriented system development, the different parts of the system are designed independently of each other. We suggest a composition operator for MSC specifications of such components and outline differences to operators used for the composition of scenarios.
Specification and Verification of Component-Based Systems (SAVCBS). Workshop at OOPSLA 2001 (SAVCBS 2001).