Synthesizing partial component-level behavior models from system specifications

ABSTRACT

Initial system specifications, such as use-case scenarios and properties, only partially specify the future system. We posit that synthesizing partial component-level behavior models from these early specifications can improve software development practices. In this paper, we provide a novel algorithm for deriving a Modal Transition System (MTS) for individual system components from system-level scenario and property specifications. The generated MTSs capture the possible component implementations that (1) necessarily provide the behavior required by the scenarios, (2) restrict behavior forbidden by the properties, and (3) leave the behavior that is neither explicitly required nor forbidden as undefined. We also show how our algorithm helps to discover potential design flaws.

REFERENCES

• 1: J. Ackermann and K. Turowski. A library of OCL specification patterns for behavioral specification of software components. In Proc. of CAiSE, 2006.
• 2: D. Alarjeh et al. Learning operational requirements from goal models. In Proc. of ICSE, 2009.
• 3: C. Damas et al. Generating annotated behavior models from end-user scenarios. IEEE TSE, 31(12), 2005.
• 4: C. Damas et al. Scenarios, goals, and state machines: a win-win partnership for model synthesis. In Proc. of FSE, 2006.
• 5: W. Damm and D. Harel. LSCs: Breathing life into message sequence charts. Form. Meth. Syst. Des., 19(1), 2001.
• 6: G. de Caso et al. Validation of contracts using enabledness preserving finite state abstractions. In Proc. of ICSE, 2009.
• 7: D. Fischbein and S. Uchitel. On consistency and merge of modal transition systems. In Proc. of FSE, 2008.
• 8: D. Giannakopoulou and J. Magee. Fluent model checking for event-based systems. In Proc. of FSE, 2003.
• 9: D. Harel et al. Synthesis revisited: Generating statechart models from scenario-based requirements. Form. Meth. in Soft. and Sys. Modeling, 3393, 2005.
• 10: ITU. Message sequence charts, 2000.
• 11: I. Krka, G. Edwards, Y. Brun, and N. Medvidovic. From system specification to component behavioral models. In Proc. ICSE NIER, 2009.
• 12: K. G. Larsen and B. Thomsen. A modal process logic. Logic in Computer Science, 1988.
• 13: E. Mäkinen et al. MAS - an interactive synthesizer to support behavioral modeling in UML. In Proc. of ICSE, 2001.
• 14: R. Milner. Communication and concurrency. Prentice-Hall, 1989.
• 15: MTSGen. http://www-scf.usc.edu/~krka/MTSGen.zip.
• 16: D. Pilone and N. Pitman. UML 2.0 in a Nutshell. O'Reilly Media, Inc., 2005.
• 17: G. Sibay et al. Existential live sequence charts revisited. In Proc. of ICSE, 2008.
• 18: S. Uchitel et al. Behaviour model elaboration using partial labelled transition systems. In Proc. of ESEC/FSE, 2003.
• 19: S. Uchitel et al. Incremental elaboration of scenario-based specifications and behavior models using implied scenarios. ACM TOSEM, 13(1), 2004.
• 20: S. Uchitel et al. Behaviour model synthesis from properties and scenarios. In Proc. of ICSE, 2007.
• 21: J. Whittle and J. Schumann. Generating statechart designs from scenarios. In Proc. of ICSE, 2000.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.11 Software Architectures

General Terms:
Algorithms

Keywords:
behavior model synthesis, constraints, modal transition systems, partial specifications, scenarios