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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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)
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)
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)
Object Management Group: Unified Modeling Language: Superstructure Version 2.0 (2005)
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)
Herrmann, P., Krumm, H.: A Framework for Modeling Transfer Protocols. Computer Networks 34(2), 317–337 (2000)
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)
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)
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)
Bræk, R.: Unified System Modelling and Implementation. In: International Switching Symposium, Paris, France, pp. 1180–1187 (1979)
SISU II Project, http://www.sintef.no/units/informatics/projects/sisu/
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)
Mitschele-Thiel, A.: Systems Engineering with SDL: Developing Performance-Critical Communication System. John Wiley & Sons, Inc., New York (2001)
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)
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)
Selic, B., Gullekson, G., Ward, P.T.: Real-Time Object-Oriented Modeling. John Wiley & Sons, Inc., New York (1994)
ISO: ESTELLE: A Formal Description Technique Based on an Extended State Transition Model. International Standard ISO/IEC 9074 edn. (1997)
ITU-T: Recommendation Z.100: Specification and Description Language (SDL) (2002)
Lim, S.B., Ferry, D.: JAIN SLEE 1.0 Specification, Final Release. Sun Microsytems, Inc. and Open Cloud Ltd. (2004)
Haugen, Ø., Møller-Pedersen, B.: JavaFrame — Framework for Java Enabled Modelling. In: Proceedings of Ericsson Conference on Software Engineering (2000)
Bræk, R., Haugen, Ø.: Engineering Real Time Systems: An Object-Oriented Methodology Using SDL. The BCS Practitioner Series. Prentice Hall International, Englewood Cliffs (1993)
Bræk, R., Husa, K.E., Melby, G.: ServiceFrame Whitepaper, Ericsson NorARC, Asker, Norway (2002)
Melby, G., Husa, K.E.: ActorFrame Developers Guide, Ericsson NorARC, Asker, Norway (2005)
Melby, G.: Using J2EE Technologies for Implementation of ActorFrame Based UML 2.0 Models. Master’s thesis, Agder University College, Grimstad, Norway (2003)
Kraemer, F.A., Samset, H.: Ramses User Guide. Avantel Technical Report 1/2006, Department of Telematics, NTNU, Trondheim, Norway (2006)
Kraemer, F.A.: Rapid Service Development for Service Frame. Master’s thesis, University of Stuttgart (2003)
Støyle, A.K.: Service Engineering Environment for AMIGOS. Master’s thesis, Norwegian University of Science and Technology (2004)
Kraemer, F.A.: Profile for Service Engineering: Executable State Machines. Avantel Technical Report 2/2006, Department of Telematics, NTNU, Trondheim, Norway (2006)
Lamport, L.: Specifying Systems. Addison-Wesley, Reading (2002)
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)
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)
Lamport, L.: Refinement in State-Based Formalisms. Technical Report 1996-001, Digital Equipment Corporation, Systems Research Center, Palo Alto, California (1996)
Alpern, B., Schneider, F.B.: Defining Liveness. Information Processing Letters 21(4), 181–185 (1985)
Kurki-Suonio, R.: A Practical Theory of Reactive Systems. Springer, Heidelberg (2005)
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)
Pitkänen, R.: Tools and Techniques for Specification-Driven Software Development. PhD thesis, Tampere University of Technology (2006)
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)