Architecting families of software systems with process algebras

ABSTRACT

Software components can give rise to several kinds of architectural mismatches when assembled together in order to form a software system. A formal description of the architecture of the resulting component-based software system may help to detect such architectural mismatches and to single out the components that cause the mismatches. In this article, we concentrate on deadlock-related architectural mismatches arising from three different causes that we identify: incompatibility between two components due to a single interaction, incompatibility between two components due to the combination of several interactions, and lack of interoperability among a set of components forming a cyclic topology. We develop a process algebra-based architectural description language called PADL, which deals with all three causes through an architectural compatibility check and an architectural interoperability check relying on standard observational equivalences. The adequacy of the architectural compatibility check is assessed on a compressing proxy system, while the adequacy of the architectural interoperability check is assessed on a cruise control system. We then address the issue of scaling the architectural compatibility and interoperability checks to architectural styles through an extension of PADL. The formalization of an architectural style is complicated by the presence of two degrees of freedom within the set of instances of the style: variability of the internal behavior of the components and variability of the topology formed by the components. As a first step towards the solution of the problem, we propose an intermediate abstraction called architectural type, whose instances differ only for the internal behavior of their components. We define an efficient architectural conformity check based on a standard observational equivalence to verify whether an architecture is an instance of an architectural type. We show that all the architectures conforming to the same architectural type possess the same compatibility and interoperability properties.

REFERENCES

• 1: Gregory D. Abowd , Robert Allen , David Garlan, Formalizing style to understand descriptions of software architecture, ACM Transactions on Software Engineering and Methodology (TOSEM), v.4 n.4, p.319-364, Oct. 1995 [doi>10.1145/226241.226244]
• 2: Robert Allen , David Garlan, A formal basis for architectural connection, ACM Transactions on Software Engineering and Methodology (TOSEM), v.6 n.3, p.213-249, July 1997 [doi>10.1145/258077.258078]
• 3: Robert Allen , David Garlan, A Case Study in Architectural Modelling: The AEGIS System, Proceedings of the 8th International Workshop on Software Specification and Design, p.6, March 22-23, 1996
• 4: Henrik Reif Andersen, Partial Model Checking, Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, p.398, June 26-29, 1995
• 5: Simonetta Balsamo , Marco Bernardo , Marta Simeoni, Combining stochastic process algebras and queueing networks for software architecture analysis, Proceedings of the 3rd international workshop on Software and performance, July 24-26, 2002, Rome, Italy [doi>10.1145/584369.584398]
• 6: Bernardo, M. 2002. TwoTowers 2.0 User Manual. http://www.sti.uniurb.it/bernardo/twotowers/.
• 7: Marco Bernardo , Paolo Ciancarini , Lorenzo Donatiello, On the formalization of architectural types with process algebras, Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications, p.140-148, November 06-10, 2000, San Diego, California, United States
• 8: Marco Bernardo , Paolo Ciancarini , Lorenzo Donatiello, Detecting Architectural Mismatches in Process Algebraic Descriptions of Software Systems, Proceedings of the Working IEEE/IFIP Conference on Software Architecture (WICSA'01), p.77, August 28-31, 2001 [doi>10.1109/WICSA.2001.948411]
• 9: Marco Bernardo , Lorenzo Donatiello , Paolo Ciancarini, Stochastic Process Algebra: From an Algebraic Formalism to an Architectural Description Language, Performance Evaluation of Complex Systems: Techniques and Tools, Performance 2002, Tutorial Lectures, p.236-260, January 2002
• 10: Marco Bernardo , Francesco Franzè, Architectural Types Revisited: Extensible And/Or Connections, Proceedings of the 5th International Conference on Fundamental Approaches to Software Engineering, p.113-127, April 08-12, 2002
• 11: Marco Bernardo , Francesco Franzè, Exogenous and Endogenous Extensions of Architectural Types, Proceedings of the 5th International Conference on Coordination Models and Languages, p.40-55, April 08-11, 2002
• 12: Bravetti, M. and Bernardo, M. 2000. Compositional asymmetric cooperations for process algebras with probabilities, priorities, and time. In Proceedings of the 1st International Workshop on Models for Time Critical Systems (MTCS 2000). ENTCS, vol. 39(3). Elsevier, Amsterdam, The Netherlands.
• 13: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 14: E. Clarke , D. Long , K. McMillan, Compositional model checking, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.353-362, June 1989, Pacific Grove, California, United States
• 15: Davio, M. 1981. Kronecker products and shuffle algebra. IEEE Trans. Comput. 30, 116--125.
• 16: Thomas R. Dean , James R. Cordy, A Syntactic Theory of Software Architecture, IEEE Transactions on Software Engineering, v.21 n.4, p.302-313, April 1995 [doi>10.1109/32.385969]
• 17: DeRemer, F. and Kron, H. H. 1976. Programming-in-the-large versus programming-in-the-small. IEEE Trans. Softw. Eng. 2, 80--86.
• 18: van Glabbeek, R. J. 2001. The linear time-branching time spectrum I. The semantics of concrete, sequential processes. In Handbook of Process Algebra, Bergstra, J. A., Ponse, A., and Smolka, S. A., Eds. Elsevier, 3--99.
• 19: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 20: Paola Inverardi , Sebastián Uchitel, Proving Deadlock Freedom in Component-Based Programming, Proceedings of the 4th International Conference on Fundamental Approaches to Software Engineering, p.60-75, April 02-06, 2001
• 21: Paola Inverardi , Alexander L. Wolf, Formal Specification and Analysis of Software Architectures Using the Chemical Abstract Machine Model, IEEE Transactions on Software Engineering, v.21 n.4, p.373-386, April 1995 [doi>10.1109/32.385973]
• 22: Paola Inverardi , Alexander L. Wolf , Daniel Yankelevich, Static checking of system behaviors using derived component assumptions, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.3, p.239-272, July 2000 [doi>10.1145/352591.352593]
• 23: Jeff Kramer , Jeff Magee, Exposing the Skeleton in the Coordination Closet, Proceedings of the Second International Conference on Coordination Languages and Models, p.18-31, September 01-03, 1997
• 24: Stephen S. Lavenberg, Computer Performance Modeling Handbook, Academic Press, Inc., Orlando, FL, 1983
• 25: Jeff Magee , Naranker Dulay , Susan Eisenbach , Jeff Kramer, Specifying Distributed Software Architectures, Proceedings of the 5th European Software Engineering Conference, p.137-153, September 25-28, 1995
• 26: R. Milner, Communication and Concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 27: Mark Moriconi , Xiaolei Qian , R. A. Riemenschneider, Correct Architecture Refinement, IEEE Transactions on Software Engineering, v.21 n.4, p.356-3, April 1995 [doi>10.1109/32.385972]
• 28: Dewayne E. Perry , Alexander L. Wolf, Foundations for the study of software architecture, ACM SIGSOFT Software Engineering Notes, v.17 n.4, p.40-52, Oct. 1992 [doi>10.1145/141874.141884]
• 29: Mary Shaw , Robert DeLine , Daniel V. Klein , Theodore L. Ross , David M. Young , Gregory Zelesnik, Abstractions for Software Architecture and Tools to Support Them, IEEE Transactions on Software Engineering, v.21 n.4, p.314-335, April 1995 [doi>10.1109/32.385970]
• 30: Mary Shaw , David Garlan, Software architecture: perspectives on an emerging discipline, Prentice-Hall, Inc., Upper Saddle River, NJ, 1996

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.11 Software Architectures
            Subjects: Patterns (e.g., client/server, pipeline, blackboard); Languages (e.g., description, interconnection, definition)

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Algebraic approaches to semantics

General Terms:
Design, Languages, Verification

Keywords:
Architectural mismatch detection, architectural styles, process algebras, software architectures