Skip to main content
SpringerLink
Log in
Book cover

International Conference on the Unified Modeling Language

UML 2003: «UML» 2003 - The Unified Modeling Language. Modeling Languages and Applications pp 60–75Cite as

Formal Semantics of UML with Real-Time Constructs

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2863))

Abstract

This paper describes a formal framework for expressing the semantics of UML augmented with real-time constraints. Supported parts of UML include concurrent interacting statecharts and sequence diagrams, both with real-time constraints. The approach is compositional in the sense that semantics of real-time behavior is captured independently from traditional statechart semantics, thus allowing for simple adaptation to other semantic variations. This compositionality is supported through the use of a two-dimensional temporal logic to independently capture flow of control as well as flow of time. The paper defines this logic, and shows how the UML diagrams can be translated into this formalism. The goal is to provide a simple and intuitive compositional semantics that can be validated and used for further formal analysis.

This research was sponsored in part by PSC-CUNY grant 63389-00-32

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R.: Timed automata. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 8–22. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  2. Blackburn, P., Rijke, M.D.: Why combine logics? Studia Logica 59, 5–27 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  3. Clarke, E.M., Emerson, E., Sistla, A.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems (TOPLAS) 8(2), 244–263 (1986)

    Article  MATH  Google Scholar 

  4. Damm, W., Josko, B., Hungar, H., Pnueli, A.: A compositional real-time semantics of STATEMATE designs. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 186–238. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  5. David, A., Möller, O., Yi, W.: Formal verification of UML statecharts with real time extensions. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 218–232. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  6. Finger, M., Gabbay, D.: Adding a temporal dimension to a logic. Journal of Logic Language and Information 1, 203–233 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  7. Finger, M., Gabbay, D.: Combining temporal logic systems. Notre Dame Journal of Formal Logic, Special Issue on Combining Logics 37(2), 204–232 (1996)

    MATH  MathSciNet  Google Scholar 

  8. Harel, D.: Recurring dominoes: Making the highly undecidable highly understandable. In: Conference on Foundations of Computation Theory, pp. 177–194 (1983)

    Google Scholar 

  9. Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming 8, 231–274 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  10. Kracht, M., Wolter, F.: Properties of independently axiomatizable bimodal logics. Journal of Symbolic Logic 56(4), 1469–1485 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  11. Kroeger, F.: Temporal Logic of Programs. Springer, Heidelberg (1987)

    MATH  Google Scholar 

  12. Lavazza, L., Quaroni, G., Venturelli, M.: Combining UML and formal notations for modelling real-time systems. In: Joint European Software Engineering Conference (ESEC) and International Symposium on the Foundations of Software Engineering (FSE), pp. 196–206 (2001)

    Google Scholar 

  13. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, Heidelberg (1992)

    Google Scholar 

  14. Object Management Group. UML Profile for Schedulability, Performance, and Time Specification, Draft Adopted Specification (January 2002)

    Google Scholar 

  15. Owre, S., Rajan, S., Rushby, J., Shankar, N., Srivas, M.: PVS: Combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 411–414. Springer, Heidelberg (1996)

    Google Scholar 

  16. Shankar, S.: Formal Verification of VHDL Designs Using Temporal Logics. PhD thesis, University of Minnesota (1998)

    Google Scholar 

  17. Shankar, S.: A semantic model of real-time UML. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 573–577. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  18. Shankar, S., Slagle, J.: A polymodal semantics for VHDL. In: Advances in Hardware Design and Verification (CHARME), pp. 88–105. Chapman & Hall, Boca Raton (1997)

    Google Scholar 

  19. von der Beeck, M.: A comparison of statecharts variants. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 128–148. Springer, Heidelberg (1994)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. City University of New York (CUNY),  

    Subash Shankar & Sinan Asa

Authors
  1. Subash Shankar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sinan Asa
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Informatics, University of Edinburgh,  

    Perdita Stevens

  2. Computing Department - InfoLab21, Lancaster University, LA1 4WA, Lancaster, UK

    Jon Whittle

  3. IBM Rational, P.O. Box 9027, CO 80301-9027, Boulder, USA

    Grady Booch

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Shankar, S., Asa, S. (2003). Formal Semantics of UML with Real-Time Constructs. In: Stevens, P., Whittle, J., Booch, G. (eds) «UML» 2003 - The Unified Modeling Language. Modeling Languages and Applications. UML 2003. Lecture Notes in Computer Science, vol 2863. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45221-8_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-45221-8_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-20243-1

  • Online ISBN: 978-3-540-45221-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation