[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Rigorous development of component-based systems using component metadata and patterns

  • Original Article
  • Published:
Formal Aspects of Computing

Abstract

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.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  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

  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 (2004) Reo: a channel-based coordination model for component composition. Math Struct Comput Sci 14(3): 329–366

    Article  MathSciNet  MATH  Google Scholar 

  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

  8. Bensalem S, Bozga M, Nguyen T-H, Sifakis J (2010) Compositional verification for component-based systems and application. IET Softw 4(12): 181–193

    Article  MATH  Google Scholar 

  9. Bernardo M, Ciancarini P, Donatiello L (2002) Architecting families of software systems with process algebras. ACM Trans Softw Eng Methodol 11(4): 386–426

    Article  Google Scholar 

  10. Bruneton E, Coupaye T, Leclercq M, Quéma V, Stefani JB (2006) The FRACTAL component model and its support in Java. Softw Pract Exp 36(11–12): 1257–1284

    Article  Google Scholar 

  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 (2011) Enhanced type-based component compatibility using deployment context information. Electron Notes Theor Comput Sci 279(2): 17–31

    Article  Google Scholar 

  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 (2009) Runtime deadlock analysis for system level design. Des Autom Embed Syst 13(4): 287–310

    Article  Google Scholar 

  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

  20. Cheung S, Kramer J (1996) Context constraints for compositional reachability analysis. ACM Trans Softw Eng Methodol 5(4): 334–377

    Article  Google Scholar 

  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

  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 (2003) On the coherence of component protocols. Electron Notes Theor Comput Sci 82(5): 42–53

    Article  Google Scholar 

  28. Findler RB, Latendresse M, Felleisen M (2001) Behavioral contracts and behavioral subtyping. ACM SIGSOFT Softw Eng Notes 26(5): 229–236

    Article  Google Scholar 

  29. Formal Systems (Europe) Ltd. (1998) Process behaviour explorer—ProBE user manual

  30. Formal Systems Ltd. (2012) FDR2: user manual, version 2.94

  31. George B (1986) Mascot 3: an informal introductory tutorial. Softw Eng J 1(7): 95–102

    Article  Google Scholar 

  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

  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

  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

  36. Hepner M, Gamble R, Kelkar M, Davis L, Flagg D (2006) Patterns of conflict among software components. J Syst Softw 79(4): 537–551

    Article  Google Scholar 

  37. Hennicker R, Janisch S, Knapp A (2010) On the observable behaviour of composite components. ENTCS 260: 125–153

    Google Scholar 

  38. He J, Li X, Liu Z (2006) rCOS: a refinement calculus of object systems. Theor Comput Sci 365(1–2): 109–142

    MathSciNet  MATH  Google Scholar 

  39. He J, Li X, Liu Z (2006) A theory of reactive components. Electron Notes Theor Comput Sci 160: 173–195

    Article  Google Scholar 

  40. Hoare CAR (1985) Communicating sequential processes. Prentice-Hall, USA

    MATH  Google Scholar 

  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 (1990) The roots of software engineering. CWI Q 3(4): 325–334

    MATH  Google Scholar 

  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

  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

  54. Majster-Cederbaum M, Martens M, Minnameier C (2008) Liveness in interaction systems. Electron Notes Theor Comput Sci 215: 57–74

    Article  MATH  Google Scholar 

  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 (2007) Local and global deadlock-detection in component-based systems are NP-hard. Inf Process Lett 103(3): 105–111

    Article  MathSciNet  MATH  Google Scholar 

  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 (2000) A classification and comparison framework for software architecture description languages. Trans Softw Eng 26(1): 70–93

    Article  Google Scholar 

  61. Martin JMR, Welch PH (1997) A design strategy for deadlock-free concurrent systems. Transput Commun 3(4): 215–232

    Google Scholar 

  62. Nierstrasz O (1993) Regular types for active objects. ACM Sigplan Not 28(10): 1–15

    Article  Google Scholar 

  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 (2007) Using component metadata to regression test component-based software. Softw Test Verif Reliab 17(2): 61–94

    Article  Google Scholar 

  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

  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 (1998) Coordination models and languages. Adv Comput Eng Large Syst 46: 330–401

    Google Scholar 

  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

  70. Plasil F, Visnovsky S (2002) Behavior protocols for software components. IEEE Trans Softw Eng 28(11): 1056–1076

    Article  Google Scholar 

  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 (2006) Confluence thanks to extensional determinism. Electron Notes Theor Comput Sci 162: 305–309

    Article  MATH  Google Scholar 

  74. Roscoe AW (2010) Understanding concurrent systems, 1st edn. Springer, New York

    Book  MATH  Google Scholar 

  75. Ryan P, Schneider S (2001) Process algebra and non-interference. J Comput Secur 9(1): 75–103

    Article  Google Scholar 

  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 (2010) Conformance notions for the coordination of interaction components. Sci Comput Program 75(5): 350–373

    Article  MathSciNet  MATH  Google Scholar 

  79. Selic B, Gullekson G, Ward P (1994) Real-time object-oriented modeling. Wiley, New York

  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 (2014) Sound and mechanised compositional verification of input-output conformance. Softw Test Verif Reliab 24(4): 289–319

    Article  Google Scholar 

  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

    MATH  Google Scholar 

  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 (2010) Component publications and compositions. Unifying Theor Program 5713: 238–257

    Article  MATH  Google Scholar 

  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

Download references

Author information

Authors and Affiliations

  1. Departamento de Informática e Matemática Aplicada, Universidade Federal do Rio Grande do Norte, CampusUniversitário, Lagoa Nova, Natal, RN, CEP 59078-970, Brazil

    M. V. M. Oliveira

  2. Centro de Informática, Universidade Federal de Pernambuco, Recife, Brazil

    P. Antonino, R. Ramos, A. Sampaio & A. Mota

  3. Department of Computer Science, University of Oxford, Oxford, UK

    A. W. Roscoe

Authors
  1. M. V. M. Oliveira
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. P. Antonino
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. R. Ramos
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. A. Sampaio
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. A. Mota
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. A. W. Roscoe
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to M. V. M. Oliveira.

Additional information

Eerke Albert Boiten and Jim Woodcock

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Oliveira, M.V.M., Antonino, P., Ramos, R. et al. Rigorous development of component-based systems using component metadata and patterns. Form Asp Comp 28, 937–1004 (2016). https://doi.org/10.1007/s00165-016-0375-1

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00165-016-0375-1

Keywords

Search

Navigation