Abstract
In the UML, sequence diagrams are used to state scenarios, i.e., examples of interactions between objects. As such, sequence diagrams are being developed in the early design phases where requirements on the system are being captured. Their intuitively appealing character and conceptual simplicity makes them an ideal tool for formulating simple properties on a system, even for non-experts. Besides guiding the development of a UML model, sequence diagrams can thus furthermore be used as a starting point for the verification of the UML model.
In this paper, we show how the requirements on the system as stated in sequence diagrams can be (semi-automatically) validated for UML models consisting of class diagrams, state machines and structure diagrams. The sequence diagrams that we consider can be universally or existentially quantified or negated, i.e., state scenarios that should always, sometimes or never occur. For validating them in a UML model, we translate both model and sequence diagrams into a formal specification language (the process algebra CSP), and develop procedures for employing the standard CSP model checker (FDR) for checking their validity.
This research was partially supported by the DFG project ForMooS (grants OL98/3-2 and WE2290/5-1)
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bernardi, S., Donatelli, S., Merseguer, J.: From UML sequence diagrams and statecharts to analysable petri net models. In: WSOP’02, pp. 35–45. ACM Press, New York (2002)
Bolton, C., Davies, J.: Using relational and behavioural semantics in the verification of object models. In: FMOODS’00, pp. 163–182. Kluwer, Dordrecht (2000)
Bowman, H., Steen, M.W.A., Boiten, E.A., Derrick, J.: A formal framework for viewpoint consistency. Formal Methods in System Design 21, 111–166 (2002)
Brill, M., Buschermöhle, R., Damm, W., Klose, J., Westphal, B., Wittke, H.: Formal verification of LSCs in the development process. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 494–516. Springer, Heidelberg (2004)
Choi, Y., Bunse, C.: Behavioral consistency checking for component-based software development using the KobrA approach. In: Consistency Problems in UMLbased Software Development III, Lisbon, Portugal (revised papers) (October 2004)
Consistency problems in UML-based software development III – understanding and usage of dependency relationships, Lisbon, Portugal (October 2004)
Damm, W., Harel, D.: LSCs: Breathing life into Message Sequence Charts. In: Ciancarini, P., Gorrieri, R. (eds.) FMOODS’99. Kluwer, Dordrecht (1999)
Engels, G., Heckel, R., Küster, J.: Rule-based Specification of Behavioral Consistency based on the UML Meta-Model. In: Gogolla, M., Kobryn, C. (eds.) UML 2001. LNCS, vol. 2185, p. 272. Springer, Heidelberg (2001)
Fischer, C.: CSP-OZ: A combination of Object-Z and CSP. In: Bowman, H., Derrick, J. (eds.) FMOODS’97, vol. 2, pp. 423–438. Chapman and Hall, Boca Raton (1997)
Formal Systems (Europe) Ltd. Failures-Divergence Refinement – FDR2 User Manual, 4th edn. (August 1998)
Gehrke, T., Huhn, M., Rensink, A., Wehrheim, H.: An algebraic semantics for message sequence chart documents. In: Budkowski, S., Cavalle, A., Najm, E. (eds.) FORTE/PSTV’98, pp. 3–18. Kluwer, Dordrecht (1998)
Harel, D., Marelly, R.: Specifying and Executing Behavioral Requirements: The Play In/Play-Out Approach. Software and System Modeling 2, 82–107 (2003)
Hoare, C.A.R.: Communicating Sequential Processes. International Series in Computer Science. Prentice-Hall International. Prentice-Hall, Englewood Cliffs (1985)
International Organisation for Standardization. Information technology – Z formal specification notation – Syntax, type system and semantics, 1st edition, ISO/IEC 13568:2002 (E) International Standard (July 2002)
Ladkin, P.B., Leue, S.: Interpreting message flow graphs. Formal Aspects of Computing 7(5), 473–509 (1995)
Mauw, S., Reniers, M.A.: An Algebraic Semantics of Basic Message Sequence Charts. The Computer Journal 37(4), 269–277 (1994)
Möller, M., Olderog, E.-R., Rasch, H., Wehrheim, H.: Linking CSP-OZ with UML and Java: A case study. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 267–286. Springer, Heidelberg (2004)
Rasch, H., Wehrheim, H.: Checking Consistency in UML Diagrams: Classes and State Machines. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 229–243. Springer, Heidelberg (2003)
Roscoe, W.: The Theory and Practice of Concurrency. Series in Computer Science. Prentice Hall Europe. Prentice-Hall, Englewood Cliffs (1998)
Selic, B., Gullekson, G., Ward, P.T.: Real-Time Object-Oriented Modeling. John Wiley & Sons, Chichester (1994)
Smith, G.: The Object-Z Specification Language. Advances in Formal Methods. Kluwer, Dordrecht (2000)
Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Oriel College, Oxford (1998)
Störrle, H.: Semantics of Interactions in UML 2.0. In: Intl. Workshop on Visual Languages and Formal Methods, Auckland, NZ (2003)
Tsiolakis, A., Ehrig, H.: Consistency Analysis of UML Class and Sequence Diagrams using Attributed Graph Grammars. In: Ehrig, H., Taentzer, G. (eds.) GRATRA 2000, TU Berlin, FB Informatik, TR No. 2000-2, March 2000, pp. 77–86 (2000)
OMG Unified Modeling Language specification, version 1.5 (March 2003), http://www.omg.org
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 IFIP International Federation for Information Processing
About this paper
Cite this paper
Rasch, H., Wehrheim, H. (2005). Checking the Validity of Scenarios in UML Models. In: Steffen, M., Zavattaro, G. (eds) Formal Methods for Open Object-Based Distributed Systems. FMOODS 2005. Lecture Notes in Computer Science, vol 3535. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11494881_5
Download citation
DOI: https://doi.org/10.1007/11494881_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26181-0
Online ISBN: 978-3-540-31556-8
eBook Packages: Computer ScienceComputer Science (R0)