Model Synthesis from Imprecise Specifications
Bill Mitchell, R. C. Thomson, Paul Bristow · ePrints Soton (University of Southampton) · 2004
Abstract. The paper defines a formal semantics for MSC scenarios that is a weakening of the state semantics from [6], whilst permitting some additional semantics in the spirit of Live Sequence Charts (LSCs) [4]. The semantics here differs from that of LSCs in that mandatory be-haviour is defined dynamically within the domain of possible scenarios. This permits a semantics which uses domain knowledge to define when compositions of imprecise requirements are valid. This has been imple-mented by Motorola UK Research Labs, and is being used in a pilot study for a new telecommunications mobile 3G handset. 1 Annotated Events Industrial MSC [7] scenarios have rather imprecise compositional semantics. The paper describes a weakening of standard model synthesis semantics ([1], [3], [6]) that permits valid composition of imprecise scenario specifications. This work has been applied to industrial requirements specifications in Motorola case studies. Consider the leftmost MSC in figure 1, which is a requirements scenario for a