Abstract
With their revision in the UML 2.x standard, activities have been extended with streaming parameters. This facilitates a reuse-oriented specification style, in which dedicated functions can be contributed by self-contained activities as building blocks: Using streaming parameters, activities can be composed together in a quite powerful manner, since streaming parameters may also pass information while activities are executing. However, to compose them correctly, we must know in which sequence an activity may emit or accept these streaming parameters. Therefore, we propose special UML state machines that specify the externally visible behavior of activities. Further, we develop an algorithm to construct these state machines automatically for an activity based on model checking. Using these behavioral contracts, activities can then be composed without looking at their internal details. Moreover, the contracts can be used during system verification to reduce the complexity of the analysis.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Object Management Group. Unified Modeling Language: Superstructure, version 2.0, formal/2005-07-05 (2005)
Kraemer, F.A.: Engineering Reactive Systems: A Compositional and Model-Driven Method Based on Collaborative Building Blocks. PhD thesis, Norwegian University of Science and Technology (2008)
Kraemer, F.A., Herrmann, P.: Service Specification by Composition of Collaborations — An Example. In: Proceedings of the 2006 WI-IAT Workshops (2006 IEEE/WIC/ACM International Conference on Web Intelligence and Intelligent Agent Technology), pp. 129–133. IEEE Computer Society, Los Alamitos (2006)
Kraemer, F.A., Slåtten, V., Herrmann, P.: Model-Driven Construction of Embedded Applications based on Reusable Building Blocks – An Example. In: Bilgic, A., Gotzhein, R., Reed, R. (eds.) SDL 2009. LNCS, vol. 5719, pp. 1–19. Springer, Heidelberg (2009)
Herrmann, P., Kraemer, F.A.: Design of Trusted Systems with Reusable Collaboration Models. In: Etalle, S., Marsh, S. (eds.) Trust Management. IFIP International Federation for Information Processing, vol. 238, pp. 317–332. Springer, Heidelberg (2007)
Kraemer, F.A., Samset, H., Bræk, R.: An Automated Method for Web Service Orchestration based on Reusable Building Blocks. In: Proceedings of the 7th International IEEE Conference on Web Services (ICWS), pp. 262–270. IEEE Computer Society, Los Alamitos (2009)
Kraemer, F.A., Bræk, R., Herrmann, P.: Compositional Service Engineering with Arctis. Telektronikk, vol. 1.2009 (2009)
Kraemer, F.A., Slåtten, V., Herrmann, P.: Engineering Support for UML Activities by Automated Model-Checking — An Example. In: Proceedings of the 4th International Workshop on Rapid Integration of Software Engineering Techniques, RISE (2007)
Kraemer, F.A., Bræk, R., Herrmann, P.: Synthesizing Components with Sessions from Collaboration-Oriented Service Specifications. In: Gaudin, E., Najm, E., Reed, R. (eds.) SDL 2007. LNCS, vol. 4745, pp. 166–185. Springer, Heidelberg (2007)
Kraemer, F.A., Herrmann, P.: Transforming Collaborative Service Specifications into Efficiently Executable State Machines. In: Ehring, K., Giese, H. (eds.) Proceedings of the 6th International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2007). Electronic Communications of the EASST, vol. 7. EASST (2007)
Kraemer, F.A.: Rapid Service Development for Service Frame. Master’s thesis, University of Stuttgart (2003)
Merha, B.T.: Code Generation for Executable State Machines on Embedded Java Devices. Project Thesis, Norwegian University of Science and Technology, Trondheim, Norway (2008)
Parlay Group. Parlay X Web Services Specification, Version 2.1 - Short Messaging, http://www.parlay.org/en/specifications/pxws.asp
PATS Lab Website, http://www.pats.no
Lamport, L.: Specifying Systems. Addison-Wesley, Reading (2002)
Kraemer, F.A., Herrmann, P.: Formalizing Collaboration-Oriented Service Specifications using Temporal Logic. In: Networking and Electronic Commerce Research Conference 2007 (NAEC 2007), pp. 194–220. ATSMA Inc. (2007)
Kraemer, F.A., Slåtten, V., Herrmann, P.: Tool Support for the Rapid Composition, Analysis and Implementation of Reactive Services. Journal of Systems and Software (to appear, 2009)
Slåtten, V.: Automatic Detection and Correction of Flaws in Service Specifications. Master’s thesis, Norwegian University of Science and Technology (2008)
Kathayat, S.B., Bræk, B.: Platform Support for Situated Collaborative Learning. In: Proceedings of the 2009 International Conference on Mobile, Hybrid, and On-line Learning, Cancun, Mexico, pp. 53–60. IEEE Press, Los Alamitos (2009)
Beugnard, A., Jézéquel, J.-M., Noël, P., Watkins, D.: Making Components Contract Aware. IEEE Computer 32(7), 38–45 (1999)
Gaffney, J.E., Durek, T.A.: Software Reuse – Key to Enhanced Productivity: Some Quantitative Models. Information and Software Technology 31(5), 258–267 (1989)
D’Souza, D.F., Wills, A.C.: Objects, Components, and Frameworks with UML: the Catalysis Approach. Addison-Wesley, Reading (1999)
Frakes, W., Terry, C.: Software Reuse: Metrics and Models. ACM Computing Surveys 28(2), 415–435 (1996)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
Slåtten, V.: Model Checking Collaborative Service Specifications in TLA with TLC. Project Thesis, Norwegian University of Science and Technology, Trondheim, Norway (2007)
Holzmann, G.: Design and Validation of Computer Protocols. Prentice Hall Software Series. Prentice-Hall, Englewood Cliffs (1991)
Arctis Website, http://arctis.item.ntnu.no
Eclipse Modeling Project, http://www.eclipse.org/modeling
Abadi, M., Lamport, L.: The Existence of Refinement Mappings. Theoretical Computer Science 82(2), 253–284 (1991)
Yu, Y., Manolios, P., Lamport, L.: Model Checking TLA +  Specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54–66. Springer, Heidelberg (1999)
Selic, B., Gullekson, G., Ward, P.T.: Real-Time Object-Oriented Modeling. John Wiley & Sons, Inc., New York (1994)
Mencl, V.: Specifying Component Behavior with Port State Machines. Electronic Notes in Theoretical Computer Science 101, 129–153 (2004)
Floch, J.: Towards Plug-and-Play Services: Design and Validation using Roles. PhD thesis, Norwegian University of Science and Technology (2003)
SIMS Project Website, http://www.ist-sims.org
Kellomäki, P., Mikkonen, T.: Design Templates for Collective Behavior. In: Bertino, E. (ed.) ECOOP 2000. LNCS, vol. 1850, pp. 277–295. Springer, Heidelberg (2000)
Järvinen, H.-M., Kurki-Suonio, R., Sakkinen, M., Systä, K.: Object-Oriented Specification of Reactive Systems. In: Proceedings of the 12th International Conference on Software Engineering, pp. 63–71. IEEE Computer Society Press, Los Alamitos (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kraemer, F.A., Herrmann, P. (2009). Automated Encapsulation of UML Activities for Incremental Development and Verification. In: Schürr, A., Selic, B. (eds) Model Driven Engineering Languages and Systems. MODELS 2009. Lecture Notes in Computer Science, vol 5795. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04425-0_44
Download citation
DOI: https://doi.org/10.1007/978-3-642-04425-0_44
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04424-3
Online ISBN: 978-3-642-04425-0
eBook Packages: Computer ScienceComputer Science (R0)