Rigorous development of component-based systems using component metadata and patterns. (English) Zbl 1348.68167

Summary: In previous work we presented a CSP-based systematic approach that fosters the rigorous design of component-based development. Our approach is strictly defined in terms of composition rules, which are the only permitted way to compose components. These rules guarantee the preservation of properties (particularly deadlock freedom) by construction in component composition. Nevertheless, their application is allowed only under certain conditions whose verification via model checking turned out impracticable even for some simple designs, and particularly those involving cyclic topologies. In this paper, we address the performance of the analysis and present a significantly more efficient alternative to the verification of the rule side conditions, which are improved by carrying out partial verification on component metadata throughout component compositions and by using behavioural patterns. The use of metadata, together with behavioural patterns, demands new composition rules, which allow previous exponential time verifications to be carried out now in linear time. Two case studies (the classical dining philosophers, also used as a running example, and an industrial version of a leadership election algorithm) are presented to illustrate and validate the overall approach.


68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Full Text: DOI Link


[1] Aldini A, Bernardo M (2003) A general approach to deadlock freedom verification for software architectures. In: International symposium of formal methods Europe. Lecture notes in computer science, vol 2805. Springer, New York, pp 658-677
[2] Aldrich J, Chambers C, Notkin D (2002) Archjava: connecting software architecture to implementation. In: International conference on software engineering. ACM Press, New York · Zbl 1049.68745
[3] Allen R, Douence R, Garlan D (1998) Specifying and analyzing dynamic software architectures. In: Conference on fundamental approaches to software engineering (FASE). Lecture notes in computer science, vol 1382, Lisbon
[4] Allen R (1997) A formal approach to software architecture. Ph.D. thesis, Carnegie Mellon University, CMU Technical Report CMUU-CS-97-144
[5] Antonino PRG, Oliveira MVM, Sampaio ACA, Kristensen KE, Bryans JW (2014) Leadership election: an industrial sos application of compositional deadlock verification. In: NASA formal methods - 6th international symposium (NFM’14).Lecture notes in computer science, vol 8430. Springer, New York, pp 31-45
[6] Arbab, F, Reo: a channel-based coordination model for component composition, Math Struct Comput Sci, 14, 329-366, (2004) · Zbl 1085.68552
[7] Antonino PRG, Sampaio A, Woodcock J (2014) A refinement based strategy for local deadlock analysis of networks of csp processes. In: FM 2014: formal methods. Lecture notes in computer science, vol 8430 pp 62-77 · Zbl 1286.68098
[8] Bensalem, S; Bozga, M; Nguyen, T-H; Sifakis, J, Compositional verification for component-based systems and application, IET Softw, 4, 181-193, (2010) · Zbl 1183.68364
[9] Bernardo, M; Ciancarini, P; Donatiello, L, Architecting families of software systems with process algebras, ACM Trans Softw Eng Methodol, 11, 386-426, (2002)
[10] Bruneton, E; Coupaye, T; Leclercq, M; Quéma, V; Stefani, JB, The FRACTAL component model and its support in Java, Softw Pract Exp, 36, 1257-1284, (2006)
[11] Basu A, Gallien M, Lesire C, Nguyen T-H, Bensalem S, Ingrand F, Sifakis J (2008) Incremental component-based construction and verification of a robotic system. In: 18th European conference on artificial intelligence. Frontiers in artificial intelligence and applications, vol 178. IOS, pp 631-635 Press
[12] Bensalem S, Griesmayer A, Legay A, Nguyen T-H, Sifakis J, Yan R (2011) D-finder 2: towards efficient correctness of incremental design. In: NASA formal methods. Lecture notes in computer science, vol 6617. Springer, New York, pp 453-458
[13] Bures T, Hnetynka P, Plasil F (2006) SOFA 2.0: balancing advanced features in a hierarchical component model. In: 4th international conference on software engineering research, management and applications. IEEE, pp 40-48
[14] Brada P (2002) Metadata support for safe component upgrades. In: 26th international computer software and applications conference. IEEE, pp 1017-1021
[15] Brada, P, Enhanced type-based component compatibility using deployment context information, Electron Notes Theor Comput Sci, 279, 17-31, (2011)
[16] Beyer D, Wendler P (2013) Reuse of verification results. In: Model checking software. Lecture notes in computer science, vol 7976. Springer, New York, pp 1-17
[17] Cheung, E; Chen, X; Hsieh, H; Davare, A; Sangiovanni-Vincentelli, A; Watanabe, Y, Runtime deadlock analysis for system level design, Des Autom Embed Syst, 13, 287-310, (2009)
[18] Chi Z (2009) Components composition compatibility checking based on behavior description and roles division. In: International conference on management of e-commerce and e-government. IEEE, pp 262-265
[19] Chen X, He J, Liu Z, Zhan N (2007) A model of component-based programming. In: International symposium on fundamentals of software engineering. Lecture notes in computer science, vol 4767. Springer, New York, pp 191-206 · Zbl 1141.68363
[20] Cheung, S; Kramer, J, Context constraints for compositional reachability analysis, ACM Trans Softw Eng Methodol, 5, 334-377, (1996)
[21] Cordy M, Schobbens P, Heymans P, Legay A (2012) Towards an incremental automata-based approach for software product-line model checking. In: 16th international software product line conference. ACM, New York, pp 74-81
[22] Craig DC, Zuberek WM (2007) Compatibility of software components-modeling and verification. In: International conference on dependability of computer systems. IEEE, pp 11-18 · Zbl 1184.68260
[23] DeMichiel L, Keith M (2006) Enterprise javabeans specification, version 3.0. Technical Report JSR 220, Sun Microsystems
[24] Dias MS, Richardson DJ (2002) Identifying cause and effect relations between events in concurrent event-based components. In: 17th IEEE international conference on automated software engineering. IEEE, pp 245-248
[25] Dihego, J, Sampaio ACA, Oliveira MVM (2015) Constructive extensibility of trustworthy component-based systems. In: Proceedings of the 30th annual ACM symposium on applied computing (SAC’15). ACM, New York
[26] Fitzgerald J, Foster S, Ingram C, Larsen PG, Woodcock J (2013) Model-based engineering for systems of systems: the compass manifesto. Technical report, COMPASS. http://www.compass-research.eu/Project/Publications/MBESoS.pdf. Accessed 22 Apr 2016
[27] Farias, A; Guéhéneuc, Y, On the coherence of component protocols, Electron Notes Theor Comput Sci, 82, 42-53, (2003)
[28] Findler, RB; Latendresse, M; Felleisen, M, Behavioral contracts and behavioral subtyping, ACM SIGSOFT Softw Eng Notes, 26, 229-236, (2001)
[29] Formal Systems (Europe) Ltd. (1998) Process behaviour explorer—ProBE user manual
[30] Formal Systems Ltd. (2012) FDR2: user manual, version 2.94 · Zbl 1118.68049
[31] George, B, Mascot 3: an informal introductory tutorial, Softw Eng J, 1, 95-102, (1986)
[32] Gößler G, Graf S, Majster-Cederbaum M, Martens M, Sifakis J. (2006) Ensuring properties of interaction systems. In: Theory and practice on program analysis and compilation. Lecture notes in computer science, vol 4444. Springer, New York, pp 201-224 · Zbl 1149.68352
[33] Gößler G, Graf S, Majster-Cederbaum M, Martens M, Sifakis J (2007) An approach to modelling and verification of component based systems. In: Current trends in theory and practice of computer science. Lecture notes in computer science, vol 4362. Springer, New York, pp 295-308 · Zbl 1131.68474
[34] Ghezzi C (2012) Evolution, adaptation, and the quest for incrementality. In: Large-scale complex it systems. Development, operation and management. Springer, New York, pp 369-379
[35] Gibson-Robinson T, Armstrong P, Boulgakov A, Roscoe AW (2014) FDR3—a modern model checker for CSP. In: Erika Ábrahám, Klaus Havelund (eds) Tools and algorithms for the construction and analysis of systems. Lecture notes in computer science, vol 8413, pp 187-201 · Zbl 1392.68300
[36] Hepner, M; Gamble, R; Kelkar, M; Davis, L; Flagg, D, Patterns of conflict among software components, J Syst Softw, 79, 537-551, (2006)
[37] Hennicker, R; Janisch, S; Knapp, A, On the observable behaviour of composite components, ENTCS, 260, 125-153, (2010)
[38] He, J; Li, X; Liu, Z, Rcos: a refinement calculus of object systems, Theor Comput Sci, 365, 109-142, (2006) · Zbl 1118.68049
[39] He, J; Li, X; Liu, Z, A theory of reactive components, Electron Notes Theor Comput Sci, 160, 173-195, (2006)
[40] Hoare CAR (1985) Communicating sequential processes. Prentice-Hall, USA · Zbl 0637.68007
[41] Ivers J, Moreno G (2008) PACC starter kit: developing software with predictable behavior. In: ICSE companion. ACM, New York, pp 949-950
[42] Kwiatkowska XWM (2007) Compositional state space reduction using untangled actions. In: 13th international workshop on expressiveness in concurrency. Electron Notes Theor Comput Sci 175:27-46
[43] Lazić R (1999) A semantic study of data-independence with applications to the mechanical verification of concurrent systems. Ph.D. thesis, Oxford University, Oxford
[44] Leavens G, Dhara K (2000) Concepts of behavioral subtyping and a sketch of their extension to Component-Based systems. In: Foundations of component-based systems. Cambridge University Press, Cambridge, pp 113-135
[45] Leveson N (1995) Safeware: system safety and computers. Addison-Wesley, Menlo Park
[46] Lambertz C, Majster-Cederbaum ME (2010) Port protocols for deadlock-freedom of component systems. In: Bliudze S, Bruni R, Grohmann D, Silva A (eds) ICE. EPTCS, vol 38, pp 7-11
[47] Lau K-K, Ukis V (2005) Component metadata in component-based software development: a survey. Preprint CSPP-34, School of Computer Science, The University of Manchester, Manchester
[48] Liskov BH, Wing JM (1994) A behavioural notion of subtyping. ACM Trans Program Lang Syst 16(6):1811-1841
[49] Mahoney, M, The roots of software engineering, CWI Q, 3, 325-334, (1990) · Zbl 0732.01029
[50] Martin JMR (1996) The design and construction of deadlock-free concurrent systems. Ph.D. thesis, University of Buckingham, Buckingham
[51] Majster-Cederbaum M, Martens M (2007) Robustness in interaction systems. In: 27th international conference on formal methods for networked and distributed systems. Lecture notes of computer science, vol 4574. Springer, New York, pp 325-340 · Zbl 1215.68068
[52] Majster-Cederbaum M, Martens M (2008) Compositional analysis of deadlock-freedom for tree-like component architectures. In: 8th ACM international conference on embedded software. ACM, New York, pp 199-206
[53] Majster-Cederbaum M, Martens M, Minnameier C (2007) A polynomial-time checkable sufficient condition for deadlock-freedom of component-based systems. In: SOFSEM 2007: theory and practice of computer science, pp 888-899 · Zbl 1131.68304
[54] Majster-Cederbaum, M; Martens, M; Minnameier, C, Liveness in interaction systems, Electron Notes Theor Comput Sci, 215, 57-74, (2008) · Zbl 1161.68625
[55] Merson P, Hissam S (2005) Predictability by construction. In: 20th annual ACM SIGPLAN conference on object-oriented programming, systems, languages, and applications. ACM, New York, pp 134-135
[56] Microsoft Developer Network (2011) Component object model technologies. Technical report. http://www.microsoft.com. Accessed 22 Apr 2016
[57] Minnameier, C, Local and global deadlock-detection in component-based systems are NP-hard, Inf Process Lett, 103, 105-111, (2007) · Zbl 1184.68260
[58] Mota A, Jesus J, Gomes A, Ferri F, Watanabe E (2010) Evolving a safe system design iteratively. In: 29th international conference computer safety, reliability, and security. Lecture notes in computer science, vol 6351. Springer, New York, pp 361-374
[59] Magee J, Kramer J (1996) Dynamic structures in software architecture. In: 4th symposium on the foundations of software engineering. ACM, New York, pp 3-14
[60] Medvidovic, N; Taylor, R, A classification and comparison framework for software architecture description languages, Trans Softw Eng, 26, 70-93, (2000)
[61] Martin, JMR; Welch, PH, A design strategy for deadlock-free concurrent systems, Transput Commun, 3, 215-232, (1997)
[62] Nierstrasz, O, Regular types for active objects, ACM Sigplan Not, 28, 1-15, (1993)
[63] Object Management Group (2007) Unified modeling language, superstructure, V2.1.2. Technical report formal/2007-11-02, OMG, 2007. OMG adopted specification
[64] Orso, A; Do, H; Rothermel, G; Harrold, MJ; Rosenblum, DS, Using component metadata to regression test component-based software, Softw Test Verif Reliab, 17, 61-94, (2007)
[65] OMG (2012) OMG systems modeling language (OMG SysML), version 1.3. Technical report, Object Management Group
[66] Ouaknine J, Palikareva H, Roscoe AW, Worrell J (2013) A static analysis framework for livelock freedom in CSP. Log Methods Comput Sci 9(3):1-53 · Zbl 1274.68250
[67] Oliveira MVM, Sampaio ACA, Antonino PRG, Ramos RT, Cavancalti ALC, Woodcock JCP (2013) Compositional analysis and design of CML models. Technical report D24.1, COMPASS deliverable. http://www.compass-research.eu/. Accessed 22 Apr 2016
[68] Papadopoulos, G; Arbab, F, Coordination models and languages, Adv Comput Eng Large Syst, 46, 330-401, (1998)
[69] Plasil F (2005) Enhancing component specification by behavior description: the SOFA experience. In: 4th international symposium on Information and communication technologies. Trinity College, Dublin, p 190 · Zbl 1118.68049
[70] Plasil, F; Visnovsky, S, Behavior protocols for software components, IEEE Trans Softw Eng, 28, 1056-1076, (2002)
[71] Roscoe AW (1998) The theory and practice of concurrency. In: Prentice-Hall series in computer science. Prentice-Hall, USA
[72] Roscoe AW (2005) The pursuit of buffer tolerance. Technical report, Oxford University, Oxford
[73] Roscoe, AW, Confluence thanks to extensional determinism, Electron Notes Theor Comput Sci, 162, 305-309, (2006) · Zbl 1316.68106
[74] Roscoe AW (2010) Understanding concurrent systems, 1st edn. Springer, New York · Zbl 1211.68205
[75] Ryan, P; Schneider, S, Process algebra and non-interference, J Comput Secur, 9, 75-103, (2001)
[76] Ramos RT, Sampaio ACA, Mota AC (2006) Transformation laws for UML-RT. In: 8th IFIP international conference on formal methods for open object-based distributed systems. Lecture notes in computer science, vol 4037. Springer, New York, pp 123-138
[77] Ramos RT, Sampaio ACA, Mota AC (2009) Systematic development of trustworthy component systems. In: 2nd world congress on formal methods. Lecture notes in computer science, vol 5850. Springer, New York, pp 140-156
[78] Ramos, RT; Sampaio, ACA; Mota, AC, Conformance notions for the coordination of interaction components, Sci Comput Program, 75, 350-373, (2010) · Zbl 1200.68072
[79] Selic B, Gullekson G, Ward P (1994) Real-time object-oriented modeling. Wiley, New York · Zbl 0821.68128
[80] Sifakis J (2010) Component-based construction of heterogeneous real-time systems in bip. In: The future of software engineering, p 150
[81] Sampaio, A; Nogueira, S; Mota, A; Isobe, Y, Sound and mechanised compositional verification of input-output conformance, Softw Test Verif Reliab, 24, 289-319, (2014)
[82] Spitznagel B (2004) Compositional transformation of software connectors. Ph.D. thesis, Carnegie Mellon University, Number: CMU-CS-04-128.
[83] Selic B, Rumbaugh J (1998) Using UML for modeling complex RealTime systems. Technical report, Rational Software Corporation
[84] Sinha N, Singhania N, Chandra S, Sridharan M (2012) Alternate and learn: finding witnesses without looking all over. In: Computer aided verification. Springer, New York, pp 599-615
[85] Szyperski C (2002) Component software: beyond object-oriented programming. Addisonn-Wesley, USA · Zbl 1033.68729
[86] Wallnau KC (2003) Volume III: a technology for predictable assembly from certifiable components. Technical Report CMU/SEI-2003-TR-009, Software Engineering Institute, Carnegie Mellon University, Pittsburgh
[87] Wehrheim H (2000) Specification of an automatic manufacturing system: a case study in using integrated formal methods. In: 3rd internationsl conference fundamental approaches to software engineering. Lecture notes in computer science, vol 1783. Springer, New York, pp 334-348
[88] Zhan, N; Kang, E; Liu, Z, Component publications and compositions, Unifying Theor Program, 5713, 238-257, (2010) · Zbl 1286.68098
[89] Zeng H, Miao H (2010) Deadlock detection for parallel composition of components. In: Computer and information science, pp 23-34
[90] Zuberek W (2011) Incremental composition of software components. In: Dependable computer systems, pp 301-311
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.