More Web Proxy on the site http://driver.im/

article

Formal semantics of static and temporal state-oriented OCL constraints

Authors:

Wolfgang MuellerAuthors Info & Claims

Software and Systems Modeling (SoSyM), Volume 2, Issue 3

Pages 164 - 186

https://doi.org/10.1007/s10270-003-0026-x

Published: 01 October 2003 Publication History

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.

References

[1]

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

[2]

v. d. Beeck, M.: A Structured Operational Semantics for UML-Statecharts. Software and Systems Modeling (SoSyM) 1(2): 130---141, Springer, December 2002

[3]

Booch, G., Rumbaugh, J., Jacobson, I.: The Unified Modeling Language User Guide. Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, USA, 1999

Digital Library

[4]

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

[5]

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

[6]

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

[7]

Clark, T., Warmer, J., editors. Object Modeling with the OCL, LNCS, vol. 2263. Springer, Heidelberg, Germany, February 2002

[8]

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

[9]

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)

[10]

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

[11]

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

[12]

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

[13]

Douglass, B.P.: Doing Hard Time: Developing Real Time Systems with UML, Objects, Frameworks, and Patterns. Addison-Wesley, 2000

[14]

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

Digital Library

[15]

Ebert, J., Engels, G.: Observable or Invocable Behaviour: You have to Choose. Technical report, Universität Koblenz, Koblenz, Germany, 1994

[16]

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

[17]

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

[18]

Flake, S., Mueller, W.: An OCL Extension for Real-Time Constraints. In: Clark, T., Warmer, J. {7}, pp. 150---171

[19]

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

[20]

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

[21]

Harel, D.: Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming 8(3): 231---274, June 1987

Digital Library

[22]

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

[23]

Knapman, J.: Statistical Constraints and Verification. In: Clark, T., Warmer, J. {7}, pp. 172---188

[24]

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

[25]

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

[26]

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

[27]

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)

[28]

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

[29]

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)

[30]

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

[31]

Richters, M.: A Precise Approach to Validating UML Models and OCL Constraints. PhD thesis, Universität Bremen, Bremen, Germany, 2001

[32]

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

[33]

Richters, M., Gogolla, M.: OCL: Syntax, Semantics, and Tools. In: Clark, T., Warmer, J. {7}, pp. 42---68

[34]

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

[35]

Ruf, J.: RAVEN: Real-Time Analyzing and Verification Environment. Journal on Universal Computer Science (J.UCS), Springer, 7(1): 89---104, February 2001

[36]

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

[37]

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

[38]

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)

[39]

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

[40]

Selic, B., Rumbaugh, J.: Using UML for Modeling Complex Real-Time Systems. White Paper, 1998. http://www.rational.com/media/whitepapers/umlrt.pdf

[41]

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

[42]

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

[43]

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

[44]

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

[45]

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)

Cited By

Storey VLukyanenko RCastellanos A(2023)Conceptual Modeling: Topics, Themes, and Technology TrendsACM Computing Surveys10.1145/358933855:14s(1-38)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1145/3589338
Lail MRosales ACardenas HHamann LPerez AKühn TSousa V(2022)Transformation of TOCL temporal properties into OCLProceedings of the 25th International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings10.1145/3550356.3563132(899-907)Online publication date: 23-Oct-2022
https://dl.acm.org/doi/10.1145/3550356.3563132
Shirole MKumar R(2013)UML behavioral model based test case generationACM SIGSOFT Software Engineering Notes10.1145/2492248.249227438:4(1-13)Online publication date: 12-Jul-2013
https://dl.acm.org/doi/10.1145/2492248.2492274
Show More Cited By

Formal semantics of static and temporal state-oriented OCL constraints
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages

Recommendations

Real-Time Constraints with the OCL
ISORC '02: Proceedings of the Fifth IEEE International Symposium on Object-Oriented Real-Time Distributed Computing

In recent years, the Unified Modeling Language (UML) has received increasing attention from designers of real-time systems. Several approaches apply and enrich the UML notation for modeling of real-time applications. In addition to that, UML modelers ...
UML statecharts' PTL formal semantics
IITA'09: Proceedings of the 3rd international conference on Intelligent information technology application

An approach for transforming UML statecharts into Projection Temporal Logic(PTL) formal models for system's simulation and verification is presented in this paper. UML Statechart is a graphic tool used to describe systems' behaviors, but it lacks formal ...
UML Statecharts' PTL Formal Semantics
IITA '09: Proceedings of the 2009 Third International Symposium on Intelligent Information Technology Application - Volume 01

An approach for transforming UML statecharts into Projection Temporal Logic(PTL) formal models for system's simulation and verification is presented in this paper. UML Statechart is a graphic tool used to describe systems' behaviors, but it lacks formal ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Software and Systems Modeling (SoSyM)

Software and Systems Modeling (SoSyM) Volume 2, Issue 3

October 2003

60 pages

ISSN:1619-1366

Issue’s Table of Contents

Copyright © Copyright © 2003 Springer-Verlag.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 October 2003

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Storey VLukyanenko RCastellanos A(2023)Conceptual Modeling: Topics, Themes, and Technology TrendsACM Computing Surveys10.1145/358933855:14s(1-38)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1145/3589338
Lail MRosales ACardenas HHamann LPerez AKühn TSousa V(2022)Transformation of TOCL temporal properties into OCLProceedings of the 25th International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings10.1145/3550356.3563132(899-907)Online publication date: 23-Oct-2022
https://dl.acm.org/doi/10.1145/3550356.3563132
Shirole MKumar R(2013)UML behavioral model based test case generationACM SIGSOFT Software Engineering Notes10.1145/2492248.249227438:4(1-13)Online publication date: 12-Jul-2013
https://dl.acm.org/doi/10.1145/2492248.2492274
Küster-Filipe JAnderson S(2006)On a time enriched OCL liveness templateInternational Journal on Software Tools for Technology Transfer (STTT)10.5555/3220898.32211018:2(156-166)Online publication date: 1-Apr-2006
https://dl.acm.org/doi/10.5555/3220898.3221101
Elamkulam JGlazberg ZRabinovitz IKowlali GGupta SKohli SDattathrani SMacia C(2006)Detecting design flaws in UML state charts for embedded softwareProceedings of the 2nd international Haifa verification conference on Hardware and software, verification and testing10.5555/1763218.1763228(109-121)Online publication date: 23-Oct-2006
https://dl.acm.org/doi/10.5555/1763218.1763228
Pradella MRossi MMandrioli D(2005)ArchiTRIOProceedings of the 25th IFIP WG 6.1 international conference on Formal Techniques for Networked and Distributed Systems10.1007/11562436_28(381-395)Online publication date: 2-Oct-2005
https://dl.acm.org/doi/10.1007/11562436_28
Pradella MRossi MMandrioli D(2005)A UML-Compatible formal language for system architecture descriptionProceedings of the 12th international conference on Model Driven10.1007/11506843_17(234-246)Online publication date: 20-Jun-2005
https://dl.acm.org/doi/10.1007/11506843_17

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents