Subscribe

Issue No.07 - July (2013 vol.39)

pp: 975-1001

German Emir Sibay , Imperial College London, London

Victor Braberman , University of Buenos Aires, Buenos Aires

Sebastian Uchitel , Imperial College London, London and University of Buenos Aires, Buenos Aires

Jeff Kramer , Imperial College, London

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2012.62

ABSTRACT

Synthesis of operational behavior models from scenario-based specifications has been extensively studied. The focus has been mainly on either existential or universal interpretations. One noteworthy exception is Live Sequence Charts (LSCs), which provides expressive constructs for conditional universal scenarios and some limited support for nonconditional existential scenarios. In this paper, we propose a scenario-based language that supports both existential and universal interpretations for conditional scenarios. Existing model synthesis techniques use traditional two-valued behavior models, such as Labeled Transition Systems. These are not sufficiently expressive to accommodate specification languages with both existential and universal scenarios. We therefore shift the target of synthesis to Modal Transition Systems (MTS), an extension of labeled Transition Systems that can distinguish between required, unknown, and proscribed behavior to capture the semantics of existential and universal scenarios. Modal Transition Systems support elaboration of behavior models through refinement, which complements an incremental elicitation process suitable for specifying behavior with scenario-based notations. The synthesis algorithm that we define constructs a Modal Transition System that uses refinement to characterize all the Labeled Transition Systems models that satisfy a mixed, conditional existential and universal scenario-based specification. We show how this combination of scenario language, synthesis, and Modal Transition Systems supports behavior model elaboration.

INDEX TERMS

Semantics, Analytical models, Online banking, Merging, Unified modeling language, Indexes, Cognition, partial behavior models, Scenarios, MTS, synthesis

CITATION

German Emir Sibay, Victor Braberman, Sebastian Uchitel, Jeff Kramer, "Synthesizing Modal Transition Systems from Triggered Scenarios",

*IEEE Transactions on Software Engineering*, vol.39, no. 7, pp. 975-1001, July 2013, doi:10.1109/TSE.2012.62REFERENCES

- [1] I. Kruger, "Distributed System Design with Message Sequence Charts," PhD dissertation, Technical Univ. of Munich, 2000.
- [2] S. Uchitel, J. Kramer, and J. Magee, "Incremental Elaboration of Scenario-Based Specifications and Behaviour Models Using Implied Scenarios,"
ACM Trans. Software Eng. and Methodology, vol. 13, no. 1, pp. 37-85, 2004.- [3] D. Harel and R. Marelly,
Come, Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, 2003.- [4] Y. Bontemps, P. Heymans, and P.-Y. Schobbens, "From Live Sequence Charts to State Machines and Back: A Guided Tour,"
IEEE Trans. Software Eng., vol. 31, no. 12, pp. 999-1014, Dec. 2005.- [5] T. Ziadi, L. Helouet, and J.-M. Jezequel, "Revisiting Statechart Synthesis with an Algebraic Approach,"
Proc. 26th IEEE Int'l Conf. Software Eng., pp. 242-251, 2004.- [6] ITU, "Recommendation z.120: Message Sequence Charts," 2000.
- [7] B. Sengupta and R. Cleaveland, "Triggered Message Sequence Charts,"
IEEE Trans. Software Eng., vol. 32, no. 8, pp. 587-607, Aug. 2006.- [8] W. Damm and D. Harel, "LSCs: Breathing Life into Message Sequence Charts,"
Proc. Third Int'l Conf. Formal Methods for Open ObjectBased Distributed Systems, vol. 139, 1999.- [9] K. Zachos, N. Maiden, and A. Tosar, "Rich-Media Scenarios for Discovering Requirements,"
IEEE Software, vol. 22, no. 5, pp. 89-97, Sept./Oct. 2005.- [10] R.M. Keller, "Formal Verification of Parallel Programs,"
Comm. ACM, vol. 19, pp. 371-384, July 1976.- [11] R. Milner,
Communication and Concurrency. Prentice-Hall, 1989.- [12] K. Larsen and B. Thomsen, "A Modal Process Logic,"
Proc. Third Ann. IEEE Symp. Logic in Computer Science, pp. 203-210, 1988.- [13] K. Larsen, B. Steffen, and C. Weise, "The Methodology of Modal Constraints,"
Formal Systems Specification, vol. 1169, pp. 405-435, 1996.- [14] M. Huth, R. Jagadeesan, and D.A. Schmidt, "Modal Transition Systems: A Foundation for Three-Valued Program Analysis,"
Proc. 10th European Symp. Programming Languages and Systems, pp. 155-169, 2001.- [15] K.G. Larsen, B. Steffen, and C. Weise, "A Constraint Oriented Proof Methodology Based on Modal Transition Systems,"
Proc. First Int'l Workshop Tools and Algorithms for Construction and Analysis of Systems, pp. 13-28, 1995.- [16] D. Fischbein and S. Uchitel, "On Correct and Complete Merging of Partial Behaviour Models,"
Proc. SIGSOFT Conf. Foundations of Software Eng., pp. 297-307, 2008.- [17] S. Uchitel, G. Brunet, and M. Chechik, "Synthesis of Partial Behavior Models from Properties and Scenarios,"
IEEE Trans. Software Eng., vol. 3, no. 35, pp. 384-406, May 2009.- [18] G. Brunet, M. Chechik, D. Fischbein, N. D'Ippolito, and S. Uchitel, "Weak Alphabet Merging of Partial Behaviour Models,"
ACM Trans. Software Eng. and Methodology,- [19] G. Bruns and P. Godefroid, "Generalized Model Checking: Reasoning about Partial State Spaces,"
Proc. 11th Int'l Conf. Concurrency Theory, pp. 168-182, 2000.- [20] D. Fischbein, N. D'Ippolito, G. Sibay, and S. Uchitel, "Modal Transition System Analyser (MTSA)," http://sourceforge.net/projectsmtsa/, 2012.
- [21] J. Magee and J. Kramer,
Concurrency—State Models and Java Programs. John Wiley, 1999.- [22] S. Uchitel and M. Chechik, "Merging Partial Behavioural Models,"
Proc. 12th ACM SIGSOFT Int'l Symp. Foundations of Software Eng., pp. 43-52, 2004.- [23] E. Clarke, O. Grumberg, and D. Peled,
Model Checking. MIT Press, 1999.- [24] G. Sibay, S. Uchitel, and V. Braberman, "Existential Live Sequence Charts Revisited,"
Proc. 30th Int'l Conf. Software Eng., pp. 41-50, 2008.- [25] D. Giannakopoulou and J. Magee, "Fluent Model Checking for Event-Based Systems,"
Proc. Ninth European Software Eng. Conf. Held Jointly with 11th ACM SIGSOFT Int'l Symp. Foundations of Software Eng., 2003.- [26] R. Alur, K. Etessami, and M. Yannakakis, "Inference of Message Sequence Charts,"
IEEE Trans. Software Eng., vol. 29, no. 7, pp. 623-633, July 2003.- [27] S. Mauw and M.A. Reniers, "High-Level Message Sequence Charts,"
Proc. Int'l Conf. System Design Languages, pp. 291-306, 1997.- [28] I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh, "Efficient Detection of Vacuity in ACTL Formulas,"
Proc. Ninth Int'l Conf. Computer-Aided Verification, pp. 279-290, 1997.- [29] N. D'Ippolito, D. Fishbein, H. Foster, and S. Uchitel, "MTSA: Eclipse Support for Modal Transition Systems Construction, Analysis and Elaboration,"
Proc. OOPSLA Workshop Eclipse Technology Exchange, pp. 6-10, 2007.- [30] R. van Ommering, F. van der Linden, J. Kramer, and J. Magee, "The Koala Component Model for Consumer Electronics Software,"
Computer, vol. 33, no. 3, pp. 78-85, 2000.- [31] W. Damm and D. Harel, "LSCs: Breathing Life into Message Sequence Charts,"
Formal Methods in System Design, vol. 19, no. 1, pp. 45-80, 2001.- [32] J. Magee, N. Pryce, D. Giannakopoulou, and J. Kramer, "Graphical Animation of Behavior Models,"
Proc. 22nd Int'l Conf. Software Eng, pp. 499-508, 2000.- [33] H. Kugler, M.J. Stern, and E.J.A. Hubbard, "Testing Scenario-Based Models,"
Proc. 10th Int'l Conf. Fundamental Approaches to Software Eng., pp. 306-320, 2007.- [34] K. Larsen and L. Xinxin, "Equation Solving Using Modal Transition Systems,"
Proc. Fifth Ann. IEEE Symp. Logic in Computer Science, pp. 108-117, 1990.- [35] Y. Bontemps, P.-Y. Schobbens, and C. Löding, "Synthesis of Open Reactive Systems from Scenario-Based Specifications,"
Fundamenta Informaticae, vol. 62, no. 2, pp. 139-169, 2004.- [36] D. Harel and H. Kugler, "Synthesizing State-Based Object Systems from LSC Specifications,"
Int'l J. Foundation of Computer Science, vol. 13, no. 1, pp. 5-51, 2002.- [37] I. Krka, Y. Brun, G. Edwards, and N. Medvidovic, "Synthesizing Partial Component-Level Behavior Models from System Specifications,"
Proc. Seventh Joint Meeting of the European Software Eng. Conf. and the ACM SIGSOFT Symp. Foundations of Software Eng. 2009.- [38] D. Pilone and N. Pitman,
UML 2.0 in a Nutshell. O'Reilly, 2005, http:/www.uml.org/, 2012.- [39] A. Antonik, M. Huth, K. Larsen, U. Nyman, and A. Wasowski, "20 Years of Modal and Mixed Specifications,"
Bull. EATCS, vol. 95, pp. 94-129, June 2008.- [40] D. Alrajeh, J. Kramer, A. Russo, and S. Uchitel, "Learning Operational Requirements from Goal Models,"
Proc. 31st IEEE Int'l Conf. Software Eng., pp. 265-275, 2009. |