Scenarios, goals, and state machines: a winwin partnership for model synthesis

Models are increasingly recognized as an effective means for elaborating requirements and exploring designs. For complex systems, model building is far from an easy task. Efforts were therefore recently made to automate parts of this process, notably, by synthesizing behavior models from scenarios of interactions between the software-to-be and its environment. In particular, our previous interactive synthesizer generates labelled transition systems (LTS) from simple message sequence charts (MSC) provided by end-users. Compared with others, the synthesizer requires no additional input such as state or flowcharting information. User interactions consist in simple scenarios generated by the synthesizer that the user has to classify as example or counterexample of desired behavior. Experience with this approach showed that the number of such scenario questions may become fairly large in interaction-intensive applications such as web applications. In this paper, we extend our model synthesis technique by injecting additional information into the synthesizer, when available, in order to constrain induction and prune the inductive search space. Additional information may include global definitions of fluents that link interaction events and atomic assertions; declarative properties of the domain; behavior models of external components; and goals that the software system is expected to satisfy. We provide comparative data on increasingly complex examples to show how effective such constraints are in reducing the number of scenario questions and in increasing the adequacy of the synthesized model. As goals and domain properties might not be easily provided by users, the paper also shows how our synthesizer generates a significant class of them automatically from the available scenarios. As a side-effect, our work provides additional evidence on the synergistic links between scenarios, goals, and state machines for model-driven engineering of requirements and designs