Assert and negate revisited: modal semantics for UML sequence diagrams

ABSTRACT

Live Sequence Charts (LSC) extend Message Sequence Charts (MSC), mainly by distinguishing possible from necessary behavior. They thus enable the specification of rich multi-modal scenario-based properties, such as mandatory, possible and forbidden scenarios. The sequence diagrams of UML 2.0 enrich those of previous versions of UML by two new operators, assert and negate, for specifying required and forbidden behaviors, which appear to have been inspired by LSC. The UML 2.0 semantics of sequence diagrams, however, being based on pairs of valid and invalid sets of traces, is inadequate, and prevents the new operators from being used effectively. We propose an extension of, and a different semantics for this UML language - Modal UML Sequence Diagrams (MUSD) - based on the universal/existential modal semantics of LSC. MUSD can be formally defined as a UML profile, thus paving the way to apply formal verification, synthesis, and scenario-based execution techniques from LSC to the mainstream UML standard.

REFERENCES

• 1: Y. Bontemps and P. Heymans. Turning high-level live sequence charts into automata. In Proc. SCESM workshop of the ICSE 2002, Orlando, FL, May 2002.
• 2: Grady Booch , James Rumbaugh , Ivar Jacobson, Unified Modeling Language User Guide, The (2nd Edition) (Addison-Wesley Object Technology Series), Addison-Wesley Professional, 2005
• 3: Annette Bunker , Ganesh Gopalakrishnan , Konrad Slind, Live sequence charts applied to hardware requirements specification and verification: A VCI bus interface model, International Journal on Software Tools for Technology Transfer (STTT), v.7 n.4, p.341-350, August 2005 [doi>10.1007/s10009-004-0145-x]
• 4: M. Cengarle and A. Knapp. Uml 2.0 interactions: Semantics and refinement. In J. Jrjens, et al. editors, CSDUML'04, pages 85--99, 2004.
• 5: P. Combes, D. Harel, and H. Kugler. Modeling and Verification of a Telecommunication Application Using Live Sequence Charts and the Play-Engine Tool, volume 3707 of em LNCS, pages 414--428. Springer-Verlag, 2005.
• 6: Werner Damm , David Harel, LSCs: Breathing Life into Message Sequence Charts, Formal Methods in System Design, v.19 n.1, p.45-80, July 2001 [doi>10.1023/A:1011227529550 ]
• 7: W. Damm and B. Westphal. Live and Let Die: LSC-based Verification of UML-Models. In Proc. FMCO'02, volume 2852 of LNCS, pages 99--135. Springer-Verlag, 2003.
• 8: Radu Grosu , Scott A. Smolka, Safety-Liveness Semantics for UML 2.0 Sequence Diagrams, Proceedings of the Fifth International Conference on Application of Concurrency to System Design, p.6-14, June 07-09, 2005 [doi>10.1109/ACSD.2005.31]
• 9: D. Harel and H. Kugler. Synthesizing State-Based Object Systems from LSC Specifications. Int. J. of Foundations of Computer Science, 13(1):5--51, February 2002.
• 10: D. Harel, H. Kugler, and A. Pnueli. Synthesis Revisited: Generating Statechart Models from Scenario-Based Requirements, volume 3393 of LNCS, pages 309--324. Springer-Verlag, 2005.
• 11: David Harel , Rami Marelly, Come, Let's Play: Scenario-Based Programming Using LSC's and the Play-Engine, Springer-Verlag New York, Inc., Secaucus, NJ, 2003
• 12: O. Haugen, K. E. Husa, R. K. Runde, and K. Stølen. Stairs towards formal design with sequence diagrams. Software and System Modeling (SoSyM), 4 (4):355--367, 2005.
• 13: ITU. International Telecommunication Union recommendation z.120: Message Sequence Charts. 1996.
• 14: H. Kugler, D. Harel, A. Pnueli, Y. Lu, and Y. Bontemps. Temporal logic for scenario-based specifications. In Proc. TACAS '05, volume 3440 of LNCS, pages 445--460, 2005.
• 15: Orna Kupferman , Moshe Vardi, Weak Alternating Automata Are Not That Weak, Proceedings of the Fifth Israel Symposium on the Theory of Computing Systems (ISTCS '97), p.147, June 17-19, 1997
• 16: Rami Marelly , David Harel , Hillel Kugler, Multiple instances and symbolic variables in executable sequence charts, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 17: David E. Muller , Ahmed Saoudi , Paul E. Schupp, Alternating automata, the weak monadic theory of trees and its complexity, Theoretical Computer Science, v.97 n.2, p.233-244, April 27, 1992 [doi>10.1016/0304-3975(92)90076-R ]
• 18: Ingo Schinz , Tobe Toben , Christian Mrugalla , Bernd Westphal, The Rhapsody UML Verification Environment, Proceedings of the Software Engineering and Formal Methods, Second International Conference on (SEFM'04), p.174-183, September 28-30, 2004 [doi>10.1109/SEFM.2004.44]
• 19: H. Störrle. Assert, negate and refinement in textscUML-2.0 interactions. In J. Jürjens, E. B. Fernández, R. France, and B. Rumpe, editors, Proc. CSDUML '04, pages 79--94, 2003.
• 20: H. Störrle. Trace semantics of UML 2.0 interactions. Technical report, University of Munich, February 2004.
• 21: UML. Unified modeling language superstructure specification, v2.0. OMG specification, OMG, August 2005.

INDEX TERMS

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

General Terms:
Design, Languages, Standardization

Keywords:
UML, inter-object approach, live sequence charts, scenarios, semantics, sequence diagrams, specification, visual formalisms