Abstract
Component Based Software Development (CBSD) is an established paradigm to build systems from reusable and loosely coupled units. However, it is still a challenge to ensure, in a scalable way, that desired properties hold for component integration. We present a component based model for UML, including a metamodel, well-formedness conditions and a formal semantics via translation into BRIC. We use (our previous work on) BRIC as an underlying (and totally hidden) component development framework so that our approach benefits from all the formal infrastructure developed for BRIC using CSP (Communicating Sequential Processes). Component composition, specified via UML structural diagrams, ensures, by construction, adherence to classical concurrent properties: our focus is on the preservation of deadlock freedom. Partial automated support is developed as a plug-in to the Astah modelling tool. We illustrate our overall approach with two case studies.
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
References
Arbab, F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comput. Sci. 14(3), 329–366 (2004)
Bonakdarpour, B., Bozga, M., Jaber, M., Quilbeuf, J., Sifakis, J.: A framework for automated distributed implementation of component-based models. Distrib. Comput. 25(5), 383–409 (2012)
Cavalcanti, A., Miyazawa, A., Sampaio, A., Li, W., Ribeiro, P., Timmis, J.: Modelling and verification for swarm robotics. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 1–19. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-98938-9_1
Change Vision, Inc.: Astah - software design tools for agile teams with UML, June 2018. http://astah.net/
Chen, Z., Liu, Z., Ravn, A.P., Stolz, V., Zhan, N.: Refinement and verification in component-based model-driven design. Sci. Comput. Program. 74(4), 168–196 (2009)
Chen, Z., Morisset, C., Stolz, V.: Specification and validation of behavioural protocols in the rCOS modeler. In: Arbab, F., Sirjani, M. (eds.) FSEN 2009. LNCS, vol. 5961, pp. 387–401. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11623-0_23
Fitzgerald, J., Larsen, P.G.: Modelling Systems: Practical Tools and Techniques in Software Development. Cambridge University Press, New York (2009)
Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 — a modern refinement checker for CSP. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 187–201. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_13
Grüninger, M., Menzel, C.: The process specification language (PSL) theory and applications. AI Mag. 24, 63–74 (2003)
Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231–274 (1987)
Jacobs, B., Rutten, J.: An introduction to (co) algebra and (co) induction. EATCS Bull. 62, 222–259 (1997)
Kim, H.Y., Jerath, K., Sheldon, F.: Assessment of high integrity software components for completeness, consistency, fault-tolerance, and reliability. In: Cechich, A., Piattini, M., Vallecillo, A. (eds.) Component-Based Software Quality. LNCS, vol. 2693, pp. 259–286. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45064-1_13
Lima, L., et al.: An integrated semantics for reasoning about sysml design models using refinement. Softw. Syst. Model. 16(3), 875–902 (2017)
Object Management Group (OMG): Meta-Object Facility (MOF) Specification, Version 2.5.1. OMG Document Number formal, 01 November 2016. http://www.omg.org/spec/MOF/2.5.1
Object Management Group (OMG): OMG System Modeling Language (OMG SysML), Version 1.5. OMG Document Number formal, 01 May 2017. https://www.omg.org/spec/SysML/1.5/
Object Management Group (OMG): Semantics of a Foundational Subset for Executable UML Models, Version 1.3. OMG Document Number formal/formal, 02 July 2017. https://www.omg.org/spec/FUML/1.3/
Oliveira, M.V.M., Antonino, P., Ramos, R., Sampaio, A., Mota, A., Roscoe, A.W.: Rigorous development of component-based systems using component metadata and patterns. Form. Aspects Comput. 28(6), 937–1004 (2016)
Ramos, R., Sampaio, A., Mota, A.: Systematic development of trustworthy component systems. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 140–156. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-05089-3_10
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River (1997)
Woodcock, J., Cavalcanti, A., Fitzgerald, J., Larsen, P., Miyazawa, A., Perry, S.: Features of CML: a formal modelling language for systems of systems. In: 2012 7th International Conference on System of Systems Engineering (SoSE), pp. 1–6, July 2012
Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall Inc., Upper Saddle River (1996)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Falcão, F., Lima, L., Sampaio, A. (2018). Safe and Constructive Design with UML Components. In: Massoni, T., Mousavi, M. (eds) Formal Methods: Foundations and Applications. SBMF 2018. Lecture Notes in Computer Science(), vol 11254. Springer, Cham. https://doi.org/10.1007/978-3-030-03044-5_15
Download citation
DOI: https://doi.org/10.1007/978-3-030-03044-5_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-03043-8
Online ISBN: 978-3-030-03044-5
eBook Packages: Computer ScienceComputer Science (R0)