Towards Formal but Flexible Scenarios
Bikram Sengupta, Rance Cleaveland · 2003
We argue that the evident utility of scenario-based modeling can be greatly enhanced when enriched with a mathematically precise notion of conditionality and partiality, such as that found in Triggered Message Sequence Charts (TMSCs). Unlike traditional Message Sequence Charts, the TMSC formalism allows scenarios to be conditional and partial, supports logical as well as behavioral operators for scenario composition, and is equipped with a refinement notion drawn from traditional process theory that provides a rigorous basis for stepwise development of specifications. This paper illustrates these points via the Center TRACON Automation System for flight control.