Skip to main content
SpringerLink
Log in

Aligning UML 2.0 State Machines and Temporal Logic for the Efficient Execution of Services

  • Conference paper
On the Move to Meaningful Internet Systems 2006: CoopIS, DOA, GADA, and ODBASE (OTM 2006)

Part of the book series: Lecture Notes in Computer Science ((LNISA,volume 4276))

Abstract

In our service engineering approach, services are specified by UML 2.0 collaborations and activities, focusing on the interactions between cooperating entities. To execute services, however, we need precise behavioral descriptions of physical system components modeling how a component contributes to a service. For these descriptions we use the concept of state machines which form a suitable input for our existing code generators that produce efficiently executable programs. From the engineering viewpoint, the gap between the collaborations and the components will be covered by UML model transformations. To ensure the correctness of these transformations, we use the compositional Temporal Logic of Actions (cTLA) which enables us to reason about service specifications and their refinement formally. In this paper, we focus on the execution of services. By outlining an UML profile, we describe which form the descriptions of the components should have to be efficiently executable. To guarantee the correctness of the design process, we further introduce the cTLA specification style cTLA/e which is behaviorally equivalent with the UML 2.0 state machines used as code generator input. In this way, we bridge the gap between UML for modeling and design, cTLA specifications used for reasoning, and the efficient execution of services, so that we can prove important properties formally.

An erratum to this chapter can be found at http://dx.doi.org/10.1007/11914952_55.

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

Access this chapter

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Sanders, R.T., Castejón, H.N., Kraemer, F.A., Bræk, R.: Using UML 2.0 Collaborations for Compositional Service Specification. In: ACM / IEEE 8th International Conference on Model Driven Engineering Languages and Systems (2005)

    Google Scholar 

  2. Rossebø, J.E.Y., Bræk, R.: Towards a Framework of Authentication and Authorization Patterns for Ensuring Availability in Service Composition. In: Proceedings of the 1st International Conference on Availability, Reliability and Security (ARES 2006), pp. 206–215. IEEE Computer Society Press, Los Alamitos (2006)

    Google Scholar 

  3. Castejón, H.N., Bræk, R.: A Collaboration-based Approach to Service Specification and Detection of Implied Scenarios. In: ICSE’s 5th Workshop on Scenarios and State Machines: Models, Algorithms and Tools (SCESM 2006) (2006)

    Google Scholar 

  4. Object Management Group: Unified Modeling Language: Superstructure Version 2.0 (2005)

    Google Scholar 

  5. Bræk, R., Floch, J.: ICT convergence: Modeling issues. In: Amyot, D., Williams, A.W. (eds.) SAM 2004. LNCS, vol. 3319, pp. 237–256. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  6. Herrmann, P., Krumm, H.: A Framework for Modeling Transfer Protocols. Computer Networks 34(2), 317–337 (2000)

    Article  Google Scholar 

  7. Mester, A., Krumm, H.: Composition and Refinement Mapping based Construction of Distributed Applications. In: Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Aarhus, Denmark, BRICS (1995)

    Google Scholar 

  8. Herrmann, P.: Formal Security Policy Verification of Distributed Component-Structured Software. In: König, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol. 2767, pp. 257–272. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  9. Herrmann, P.: Temporal Logic-Based Specification and Verification of Trust Models. In: Stølen, K., Winsborough, W.H., Martinelli, F., Massacci, F. (eds.) iTrust 2006. LNCS, vol. 3986, pp. 105–119. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  10. Bræk, R.: Unified System Modelling and Implementation. In: International Switching Symposium, Paris, France, pp. 1180–1187 (1979)

    Google Scholar 

  11. SISU II Project, http://www.sintef.no/units/informatics/projects/sisu/

  12. Bræk, R., Gorman, J., Haugen, Ø., Melby, G., Møller-Pedersen, B., Sanders, R.T.: Quality by Construction Exemplified by TIMe — The Integrated Methodology. Telektronikk 95(1), 73–82 (1997)

    Google Scholar 

  13. Mitschele-Thiel, A.: Systems Engineering with SDL: Developing Performance-Critical Communication System. John Wiley & Sons, Inc., New York (2001)

    Google Scholar 

  14. Pnueli, A.: Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends. Current Trends in Concurrency. Overviews and Tutorials, 510–584 (1986)

    Google Scholar 

  15. Floch, J., Bræk, R.: Towards Dynamic Composition of Hybrid Communication Services. In: SMARTNET 2000: Proceedings of the IFIP TC6 WG6.7 Sixth International Conference on Intelligence in Networks, Deventer, The Netherlands, pp. 73–92. Kluwer, B.V., Dordrecht (2000)

    Google Scholar 

  16. Selic, B., Gullekson, G., Ward, P.T.: Real-Time Object-Oriented Modeling. John Wiley & Sons, Inc., New York (1994)

    MATH  Google Scholar 

  17. ISO: ESTELLE: A Formal Description Technique Based on an Extended State Transition Model. International Standard ISO/IEC 9074 edn. (1997)

    Google Scholar 

  18. ITU-T: Recommendation Z.100: Specification and Description Language (SDL) (2002)

    Google Scholar 

  19. Lim, S.B., Ferry, D.: JAIN SLEE 1.0 Specification, Final Release. Sun Microsytems, Inc. and Open Cloud Ltd. (2004)

    Google Scholar 

  20. Haugen, Ø., Møller-Pedersen, B.: JavaFrame — Framework for Java Enabled Modelling. In: Proceedings of Ericsson Conference on Software Engineering (2000)

    Google Scholar 

  21. Bræk, R., Haugen, Ø.: Engineering Real Time Systems: An Object-Oriented Methodology Using SDL. The BCS Practitioner Series. Prentice Hall International, Englewood Cliffs (1993)

    MATH  Google Scholar 

  22. Bræk, R., Husa, K.E., Melby, G.: ServiceFrame Whitepaper, Ericsson NorARC, Asker, Norway (2002)

    Google Scholar 

  23. Melby, G., Husa, K.E.: ActorFrame Developers Guide, Ericsson NorARC, Asker, Norway (2005)

    Google Scholar 

  24. Melby, G.: Using J2EE Technologies for Implementation of ActorFrame Based UML 2.0 Models. Master’s thesis, Agder University College, Grimstad, Norway (2003)

    Google Scholar 

  25. Kraemer, F.A., Samset, H.: Ramses User Guide. Avantel Technical Report 1/2006, Department of Telematics, NTNU, Trondheim, Norway (2006)

    Google Scholar 

  26. Kraemer, F.A.: Rapid Service Development for Service Frame. Master’s thesis, University of Stuttgart (2003)

    Google Scholar 

  27. Støyle, A.K.: Service Engineering Environment for AMIGOS. Master’s thesis, Norwegian University of Science and Technology (2004)

    Google Scholar 

  28. Kraemer, F.A.: Profile for Service Engineering: Executable State Machines. Avantel Technical Report 2/2006, Department of Telematics, NTNU, Trondheim, Norway (2006)

    Google Scholar 

  29. Lamport, L.: Specifying Systems. Addison-Wesley, Reading (2002)

    Google Scholar 

  30. Graw, G., Herrmann, P., Krumm, H.: Verification of UML-Based Real-Time System Designs by means of cTLA. In: Proceedings of the 3rd IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC2K), Newport Beach, pp. 86–95. IEEE Computer Society Press, Los Alamitos (2000)

    Chapter  Google Scholar 

  31. Herrmann, P., Krumm, H.: A Framework for the Hazard Analysis of Chemical Plants. In: Proceedings of the 11th IEEE International Symposium on Computer-Aided Control System Design (CACSD 2000), Anchorage, pp. 35–41. IEEE CSS/Omnipress (2000)

    Google Scholar 

  32. Lamport, L.: Refinement in State-Based Formalisms. Technical Report 1996-001, Digital Equipment Corporation, Systems Research Center, Palo Alto, California (1996)

    Google Scholar 

  33. Alpern, B., Schneider, F.B.: Defining Liveness. Information Processing Letters 21(4), 181–185 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  34. Kurki-Suonio, R.: A Practical Theory of Reactive Systems. Springer, Heidelberg (2005)

    MATH  Google Scholar 

  35. Pitkänen, R.: A Specification-Driven Approach for Development of Enterprise Systems. In: Proceedings of the 11th Nordic Workshop on Programming and Software Development Tools and Techniques (NWPER 2004), Turku, Finland (2004)

    Google Scholar 

  36. Pitkänen, R.: Tools and Techniques for Specification-Driven Software Development. PhD thesis, Tampere University of Technology (2006)

    Google Scholar 

  37. Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)

    Book  MATH  Google Scholar 

  38. Burmester, S., Giese, H., Hirsch, M., Schilling, D.: Incremental Design and Formal Verification with UML/RT in the FUJABA Real-Time Tool Suite. In: Proceedings of the International Workshop on Specification and Validation of UML models for Real Time and Embedded Systems (SVERTS) (2004)

    Google Scholar 

  39. Burmester, S., Giese, H., Schäfer, W.: Model-Driven Architecture for Hard Real-Time Systems: From Platform Independent Models to Code. In: Hartman, A., Kreische, D. (eds.) ECMDA-FA 2005. LNCS, vol. 3748, pp. 25–40. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Telematics, Norwegian University of Science and Technology (NTNU), N-7491, Trondheim, Norway

    Frank Alexander Kraemer, Peter Herrmann & Rolv Bræk

Authors
  1. Frank Alexander Kraemer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Peter Herrmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Rolv Bræk
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. STARLab, Vrije Universiteit Brussel (VUB), Bldg G/10, Pleinlaan 2, 1050, Brussels, Belgium

    Robert Meersman

  2. School of Computer Science and Information Technology, RMIT University, Bld 10.10, 376-392 Swanston Street, VIC 3001, Melbourne, Australia

    Zahir Tari

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kraemer, F.A., Herrmann, P., Bræk, R. (2006). Aligning UML 2.0 State Machines and Temporal Logic for the Efficient Execution of Services. In: Meersman, R., Tari, Z. (eds) On the Move to Meaningful Internet Systems 2006: CoopIS, DOA, GADA, and ODBASE. OTM 2006. Lecture Notes in Computer Science, vol 4276. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11914952_41

Download citation

  • DOI: https://doi.org/10.1007/11914952_41

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-48283-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation