Abstract
The textual Object Constraint Language (OCL) is primarily intended to specify restrictions over UML class diagrams, in particular class invariants, operation pre-, and postconditions. Based on several improvements in the definition of the language concepts in last years, a proposal for a new version of OCL has recently been published [43]. That document provides an extensive OCL semantic description that constitutes a tight integration into UML. However, OCL still lacks a semantic integration of UML Statecharts, although it can already be used to refer to states in OCL expressions.
This article presents an approach that closes this gap and introduces a formal semantics for such integration through a mathematical model. It also presents the definition of a temporal OCL extension by means of a UML Profile based on the metamodel of the latest OCL proposal. Our OCL extension enables modelers to specify behavioral state-oriented real-time constraints. It provides an intuitive understanding and readability at application level since common OCL syntax and concepts are preserved. A well-defined formal semantics is given through the mapping of temporal OCL expressions to temporal logics formulae.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Baar, T., Hähnle, R.: An Integrated Metamodel for OCL Types. In: France, R., Rumpe, B., Bruel, J.-M., Moreira, A., Whittle, J., Ober, I. (eds.) Refactoring the UML – In Search of the Core. Workshop at OOPSLA’2000, Minneapolis, MN, USA, October 2000
v. d. Beeck, M.: A Structured Operational Semantics for UML-Statecharts. Software and Systems Modeling (SoSyM) 1(2): 130–141, Springer, December 2002
Booch, G., Rumbaugh, J., Jacobson, I.: The Unified Modeling Language User Guide. Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, USA, 1999
Bradfield, J., Kuester Filipe, J., Stevens, P.: Enriching OCL Using Observational mu-Calculus. In: Kutsche, R.-D., Weber, H. (eds.) Fundamental Approaches to Software Engineering (FASE 2002), Grenoble, France, LNCS, vol. 2306. Springer, April 2002, pp. 203–217
Casanova, M., Wallet, T., D’Hondt, M.: Ensuring Quality of Geographic Data with UML and OCL. In: Evans, A., Kent, S., Selic, B. (eds.) UML 2000 – The Unified Modeling Language. Advancing the Standard. 3rd International Conference, York, UK, October 2000, LNCS, vol. 1939. Springer, 2000, pp. 225–239
Cengarle, M., Knapp, A.: Towards OCL/RT. In: Eriksson, L.-H. , Lindsay, P. (eds.) Formal Methods – Getting IT Right, International Symposium of Formal Methods Europe, Copenhagen, Denmark, LNCS, vol. 2391. Springer, July 2002, pp. 389–408
Clark, T., Warmer, J., editors. Object Modeling with the OCL, LNCS, vol. 2263. Springer, Heidelberg, Germany, February 2002
Conrad, S., Turowski, K.: Temporal OCL: Meeting Specifications Demands for Business Components. In: Siau, K., Halpin, T. (eds.) Unified Modeling Language: Systems Analysis, Design, and Development Issues. IDEA Group Publishing, 2001, pp. 151–165
Dangelmaier, W., Darnedde, C., Flake, S., Mueller, W., Pape, U., Zabel, H.: Graphische Spezifikation und Echtzeitverifikation von Produktionsautomatisierungssystemen. In: 4. Paderborner Frühlingstagung 2002, ALB-HNI-Verlagsschriftenreihe, Paderborn, Germany, April 2002. (in German)
David, A., Möller, M., Yi, W.: Formal Verification of UML Statecharts with Real-Time Extensions. In: Kutsche, R.-D., Weber, H. (eds.) 5th International Conference on Fundamental Approaches to Software Engineering (FASE 2002), April 2002, Grenoble, France, LNCS, vol. 2306. Springer, 2002, pp. 218–232
Demuth, B., Hussmann, H., Loecher, S.: OCL as a Specification Language for Business Rules in Database Applications. In: Gogolla, M., Kobryn, C. (eds.) UML 2001 – The Unified Modeling Language. Modeling Languages, Concepts, and Tools. 4th International Conference, Toronto, Canada, October 2001, LNCS, vol. 2185. Springer, 2001, pp. 104–117
Distefano, D., Katoen, J.-P., Rensink, A.: On a Temporal Logic for Object-Based Systems. In: Smith, S.F., Talcott, C.L. (eds.) Formal Methods for Open Object-Based Distributed Systems IV (FMOODS’2000), Stanford, CA, USA. Kluwer Academic Publishers, September 2000, pp. 285–304
Douglass, B.P.: Doing Hard Time: Developing Real Time Systems with UML, Objects, Frameworks, and Patterns. Addison-Wesley, 2000
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in Property Specifications for Finite-State Verification. In: Proceedings of the 21st International Conference on Software Engineering (ICSE99), May 1999, Los Angeles, CA, USA. ACM Press, May 1999, pp. 411–420
Ebert, J., Engels, G.: Observable or Invocable Behaviour: You have to Choose. Technical report, Universität Koblenz, Koblenz, Germany, 1994
Flake, S., Mueller, W.: A UML Profile for MFERT. Technical report, C-LAB, Paderborn, Germany, March 2002. http://www.c-lab.de/vis/flake/publications/index.html
Flake, S., Mueller, W.: A UML Profile for Real-Time Constraints with the OCL. In: Jézéquel, J.-M., Hussmann, H., Cook, S. (eds.) UML 2002 – The Unified Modeling Language. Model Engineering, Languages, Concepts, and Tools. 5th International Conference, Dresden, Germany, September/October 2002, LNCS, vol. 2460. Springer, 2002, pp. 179–195
Flake, S., Mueller, W.: An OCL Extension for Real-Time Constraints. In: Clark, T., Warmer, J. [7], pp. 150–171
Flake, S., Mueller, W.: Specification of Real-Time Properties for UML Models. In: Sprague, R.H., Jr. (ed.) Proceedings of the 35th Hawaii International Conference on System Sciences (HICSS-35), Hawaii, USA, IEEE Computer Society, January 2002
Flake, S., Mueller, W.: Expressing Property Specification Patterns with OCL. In: The 2003 International Conference on Software Engineering Research and Practice (SERP’03), Las Vegas, Nevada, USA, June 2003. CSREA Press, 2003
Harel, D.: Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming 8(3): 231–274, June 1987
Kleppe, A., Warmer, J.: Extending OCL to include Actions. In: Evans, A., Kent, S., Selic, B. (eds.) UML 2000 – The Unified Modeling Language. Advancing the Standard. 3rd International Conference, York, UK, October 2000, LNCS, vol. 1939. Springer, 2000, pp. 440–450
Knapman, J.: Statistical Constraints and Verification. In: Clark, T., Warmer, J. [7], pp. 172–188
Knapp, A., Merz, S., Rauh, C.: Model Checking Timed UML State Machines and Collaborations. In: Damm, W., Olderog, E.-R. (eds.) 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT 2002), Oldenburg, September 2002, LNCS, vol. 2469. Springer, 2002, pp. 395–416
Object Management Group (OMG). UML Profile for Schedulability, Performance, and Time Specification. OMG Document ptc/02-03-02, September 2002. http://cgi.omg.org/docs/ptc/02-03-02.pdf
Object Management Group (OMG). Unified Modeling Language 1.5 Specification. OMG Document formal/03-03-01, March 2003. http://www.omg.org/technology/documents/formal/uml.htm
Object Management Group Technology Committee, Analysis and Design Platform Task Force. UML 2.0 OCL RFP, May 2003. http://www.omg.org/techprocess/meetings/schedule/UML_2.0_OCL_RFP.html (visited June 7th, 2003)
Petersohn, C., Urbina, L.: A Timed Semantics for the STATEMATE Implementation of Statecharts. In: Fitzgerald, J., Jones, C., Lucas, P. (eds.) Proceedings of 4th Int. Symposium of Formal Methods Europe (FME’97): Industrial Applications and Strengthened Foundations of Formal Methods, September 1997, Graz, Austria, LNCS, vol. 1313. Springer, 1997, pp. 553–572
Quintanilla de Simsek, J.: Ein Verifikationsansatz für eine netzbasierte Modellierungsmethode für Fertigungssysteme. PhD thesis, Heinz Nixdorf Institute, HNI-Verlagsschriftenreihe, Band 87, Paderborn, Germany, 2001. (in German)
Ramakrishnan, S., McGregor, J.: Extending OCL to Support Temporal Operators. In: 21st International Conference on Software Engineering (ICSE99), Workshop on Testing Distributed Component-Based Systems, Los Angeles, CA, USA, May 1999
Richters, M.: A Precise Approach to Validating UML Models and OCL Constraints. PhD thesis, Universität Bremen, Bremen, Germany, 2001
Richters, M., Gogolla, M.: A Metamodel for OCL. In: France, R., Rumpe, B. (eds.) UML 1999 – The Unified Modeling Language. Beyond the Standard. Second International Conference, Fort Collins, CO, USA, LNCS, vol. 1723. Springer, 1999, pp. 156–171
Richters, M., Gogolla, M.: OCL: Syntax, Semantics, and Tools. In: Clark, T., Warmer, J. [7], pp. 42–68
Roubtsova, E.E., van Katwijk, J., Toetenel, W.J., de Rooij, R.C.M.: Real-Time Systems: Specification of Properties in UML. In: Proceedings of the 7th Annual Conference of the Advanced School for Computing and Imaging (ASCI 2001). Het Heijderbos, Heijen, The Netherlands, May 2001, pp. 188–195
Ruf, J.: RAVEN: Real-Time Analyzing and Verification Environment. Journal on Universal Computer Science (J.UCS), Springer, 7(1): 89–104, February 2001
Ruf, J., Kropf, T.: Symbolic Model Checking for a Discrete Clocked Temporal Logic with Intervals. In: Cerny, E., Probst, D. (eds.) Conference on Correct Hardware Design and Verification Methods (CHARME’97), Montreal, Canada. IFIP WG 10.5, Chapman and Hall, October 1997, pp. 146–166
Ruf, J., Kropf, T.: Modeling and Checking Networks of Communicating Real-Time Systems. In: Conference on Correct Hardware Design and Verification Methods (CHARME’99), Bad Herrenalb, Germany. IFIP WG 10.5, Springer, September 1999, pp. 265–279
Schneider, U.: Ein formales Modell und eine Klassifikation für die Fertigungssteuerung – Ein Beitrag zur Systematisierung der Fertigungssteuerung. PhD thesis, Heinz Nixdorf Institute, HNI-Verlagsschriftenreihe, Band 16, Paderborn, Germany, 1996. (in German)
Schrefl, M., Stumptner, M.: Behavior Consistent Specialization of Object Life Cycles. ACM Transactions of Software Engineering and Methodology (ACM TOSEM), ACM Press 11(1): 92–148, January 2002
Selic, B., Rumbaugh, J.: Using UML for Modeling Complex Real-Time Systems. White Paper, 1998. http://www.rational.com/media/whitepapers/umlrt.pdf
Sendall, S., Strohmeier, A.: Specifying Concurrent System Behavior and Timing Constraints Using OCL and UML. In: Gogolla, M., Kobryn, C. (eds.) UML 2001 – The Unified Modeling Language. Modeling Languages, Concepts, and Tools. 4th International Conference, Toronto, Canada, October 2001, LNCS, vol. 2185. Springer, 2001, pp. 391–405
Stumptner, M., Schrefl, M.: Behavior Consistent Inheritance in UML. In: Laender, A., Liddle, S., Storey, V. (eds.) Proceedings of the 19th International Conference on Conceptual Modeling (ER 2000), Salt Lake City, UT, USA, October 2000, LNCS, vol. 1920. Springer, 2000, pp. 527–542
Warmer, J., Ivner, A., Johnston, S., Knox, D., Rivett, P.: Response to the UML2.0 OCL RfP, Version 1.6 (Submitters: Boldsoft, Rational, IONA, Adaptive Ltd., et al.). OMG Document ad/03-01-07, January 2003
Ziemann, P., Gogolla, M.: An Extension of OCL with Temporal Logic. In: Jürjens, J., Cengarle, M.V., Fernandez, E.B., Rumpe, B., Sandner, R. (eds.) Critical Systems Development with UML. Technische Universität München, Institut für Informatik, 2002, pp. 53–62
Zschaler, S.: Evaluation der Praxistauglichkeit von OCL-Spezifikationen. Master’s thesis, Technical University of Dresden, Faculty of Computer Science, Dresden, Germany, August 2002. (in German)
Author information
Authors and Affiliations
Corresponding authors
Rights and permissions
About this article
Cite this article
Flake, S., Mueller, W. Formal semantics of static and temporal state-oriented OCL constraints. Softw Syst Model 2, 164–186 (2003). https://doi.org/10.1007/s10270-003-0026-x
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10270-003-0026-x