Robert Allen
David Garlan
Abstract
As software systems become more complex, the overall system structure—or software architecture—becomes a central design problem. An important step toward an engineering discipline of software is a formal basis for describing and analyzing these designs. In the article we present a formal approach to one aspect of architectural design: the interactions among components. The key idea is to define architectural connectors as explicit semantic entities. These are specified as a collection of protocols that characterize each of the participant roles in an interaction and how these roles interact. We illustrate how this scheme can be used to define a variety of common architectural connectors. We further provide a formal semantics and show how this leads to a system in which architectural compatibility can be checked in a way analogous to type-checking in programming languages.
- ABOWD, G., ALLEN, R., AND GARLAN, D. 1995. Formalizing style to understand descriptions of software architecture. ACM Trans. Softw. Eng. Methodol. 4, 4 (Oct.). Google Scholar
- ALLEN, R. J. 1997. A formal approach to software architecture. Ph.D. thesis, School of Computer Science, Carnegie Mellon Univ., Pittsburgh, Pa., May. Google Scholar
- BROOKES, S. D. AND ROSCOE, A.W. 1985. An improved failures model for communicating processes. In Proceedings of the NSF-SERC Seminar on Concurrency. Lecture Notes in Computer Science, vol. 197. Springer-Verlag, Berlin. Google Scholar
- BURCH, J. R., CLARKE, E. M., MCMILLAN, K. L., DILL, D. L., AND HWANG, J. 1990. Symbolic model checking: 1020 states and beyond. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science. IEEE, New York.Google Scholar
- CAMERON, J. 1989. JSP and JSD: The Jackson Approach to Software Development. IEEE Computer Society Press, Los Alamitos, Calif. Google Scholar
- CLARKE, E., EMERSON, E. A., AND SISTLA, A.P. 1986. Automatic verification of finite state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8, 2 (Apr.), 244-263. Google Scholar
- DARPA. 1990. Proceedings of the Workshop on Domain-Specific Software Architectures. Software Engineering Institute, Pittsburgh, Pa.Google Scholar
- ESTRIN, G., FENCHELL, R. S., RAZOUK, R. R., AND VERNON, M. K. 1986. Sara (system architects apprentice): Modelling, analysis, and simulation support for design of concurrent systems. IEEE Trans. Softw. Eng. SE-12, 2 (Feb.), 293-311. Google Scholar
- FORMAL SYSTEMS. 1992. Failures Divergence Refinement: User Manual and Tutorial. 1.2~ ed. Formal Systems (Europe), Oxford, U.K.Google Scholar
- GARLAN, D., Ed. 1995. Proceedings of the 1st International Workshop on Architectures for Software Systems (Seattle, Wash., Apr.). Available as CMU Tech. Rep. CMU-CS-95-151. Apr.Google Scholar
- GARLAN, D. AND PERRY, D., Eds. 1995. Special issue on software architecture. IEEE Trans. Softw. Eng. 21, 4 (Apr.). Google Scholar
- GREEN, P. AND GRIFFIN, T. 1995. Specification for the RTIS HLA/RTI implementation. Tech. Rep. RTIS10951, The Real-Time Intelligent Systems Corp., Westborough, Mass., Oct.Google Scholar
- HAREL, D. 1987. Statecharts: A visual formalism for complex systems. Sci. Comput. Program. 8, 3, 231-274. Google Scholar
- HOARE, C. A. R. 1985. Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs, N.J. Google Scholar
- HOLZMANN, G.J. 1991. Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs, N.J. Google Scholar
- INVERARDI, P. AND WOLF, A. 1995. Formal specification and analysis of software architectures using the chemical, abstract machine model. IEEE Trans. Softw. Eng. 21, 4 (Apr.), 373-386. Google Scholar
- JACOB, J. 1989. Refinement of shared systems. In The Theory and Practice of Refinement, J. A. McDermid, Ed. Butterworths, London, U.K.Google Scholar
- JIFENG, H. 1990. Specification and design of the X.25 protocol: A case study in csp. In Developments in Concurrency and Communication, C. A. R. Hoare, Ed. Addison-Wesley, Reading, Mass. Google Scholar
- LAM, S. S. AND SHANKAR, A.U. 1994. A theory of interfaces and modules i--Composition theorem. IEEE Trans. Softw. Eng. 20, 1 (Jan.). Google Scholar
- LARSEN, K. G. AND MILNER, R. 1986. A complete protocol verification using relativized bisumulation. Tech. Rep. ECS-LFCS-86-13, Univ. of Edinburgh Laboratory for Foundations of Computer Science, Edinburgh, U.K.Google Scholar
- LUCKHAM, D. C., AUGUSTIN, L. M., KENNEY, J. J., VERA, J., BRYAN, D., AND MANN, W. 1995. Specification and analysis of system architecture using Rapide. IEEE Trans. Softw. Eng. 21, 4 (Apr.), 336-355. Google Scholar
- LYNCH, N. A. AND TUTTLE, M.R. 1988. An introduction to input/output automata. Tech. Rep. MIT/LCS/TM-373, MIT Laboratory for Computer Science, Cambridge, Mass.Google Scholar
- MAGEE, J., DULAY, N., EISENBACH, S., AND KRAMER, J. 1995. Specifying distributed software architectures. In Proceedings of the 5th European Software Engineering Conference, ESEC'95. Sept. Google Scholar
- METTALA, E. AND GRAHAM, M.H. 1992. The domain-specific software architecture program. Tech. Rep. CMU/SEI-92-SR-9, Software Engineering Institute, Pittsburgh, Pa.Google Scholar
- MILNER, R., FARROW, J., AND WALKER, D. 1992. A calculus of mobile processes. J. Inf. Comput. 100, 1-77. Google Scholar
- NIERSTRASZ, O. 1993. Regular types for active objects. In Proceedings of OOPSLA '93. ACM SIGPLAN Not. 28, 10 (Oct.), 1-15. Google Scholar
- NII, H.P. 1986a. Blackboard systems. Part 1. AI Mag. 7, 3, 38-53. Google Scholar
- NII, H.P. 1986b. Blackboard systems. Part 2. AI Mag. 7, 4, 62-69.Google Scholar
- PERRY, D.E. 1987. Software interconnection models. In Proceedings of the 9th International Conference on Software Engineering. IEEE Computer Society Press, Los Alamitos, Calif., 61-68. Google Scholar
- PETERSON, J.L. 1977. Petri nets. ACM Comput. Surv. 9, 3 (Sept.), 223-252. Google Scholar
- PRIETO-DIAZ, R. AND NEIGHBORS, J. M. 1986. Module interconnection languages. J. Syst. Softw. 6, 4 (Nov.), 307-334. Google Scholar
- PURTILO, J.M. 1994. The POLYLITH software bus. ACM Trans. Program. Lang. Syst. 16, 1 (Jan.), 151-174. Google Scholar
- REISS, S.P. 1990. Connecting tools using message passing in the Field Environment. IEEE Softw. 7, 4 (July), 57-66. Google Scholar
- REPS, T. AND TEITELBAUM, T. 1989. The Synthesizer Generator: A System for Constructing Language-Based Editors. Springer-Verlag, Berlin. Google Scholar
- SHAW, M. 1993. Procedure calls are the assembly language of system interconnection: Connectors deserve first-class status. In Proceedings of the Workshop on Studies of Software Design. May. Google Scholar
- SHAW, M. AND GARLAN, D. 1995. Formulations and formalisms in software architecture. In Computer Science Today: Recent Trends and Developments, J. van Leeuwen, Ed. Lecture Notes in Computer Science, vol. 1000. Springer-Verlag, Berlin.Google Scholar
- SHAW, M. AND GARLAN, D. 1996. Software Architecture: Perspectives on an Emerging Discipline. Prentice-Hall, Englewood Cliffs, N.J. Google Scholar
- SHAW, M., DELINE, R., KLEIN, D. V., ROSS, T. L., YOUNG, D. M., AND ZELESNIK, G. 1995. Abstractions for software architecture and tools to support them. IEEE Trans. Softw. Eng. 21, 4 (Apr.), 314-335. Google Scholar
- YELLIN, D. M. AND STROM, R.E. 1994. Interfaces, protocols, and the semi-automatic construction of software adaptors. In Proceedings of OOPSLA'94. ACM, New York. Google Scholar
Index Terms
- A formal basis for architectural connection
Recommendations
Errata: a formal basis for architectural connection
We present corrections to a previously published article which appeared in ACM Transaction on Software Engineering and Methodology 6, 3 (July 1997), pp. 213–249
Model Checking Software Architecture Design
HASE '12: Proceedings of the 2012 IEEE 14th International Symposium on High-Assurance Systems EngineeringSoftware Architecture plays an essential role in the high level description of a system design. Despite its importance in the software engineering practice, the lack of formal description and verification support hinders the development of quality ...
A Formal Specification of an Oscilloscope
This case study presents the development of an abstract oscilloscope specification, using Z notation. A description is given of the problem and its context. An abstract model of an oscilloscope that clarifies its user-accessible functions is described. ...
Reviews
Markus Wolf
Allen and Garlan present a formal approach to the description of the architectural design of interacting components of a software system. The intention of the approach is to extend traditional methods of formalizing architectural design (Interface Definition Languages and Module Interconnection Languages) to handle the interaction between communicating components. In the first few sections, this motivation is discussed extensively. These sections also distinguish between the common focus of design descriptions, which are based on hierarchical definition/use principles, and the needs of interactive systems, where the components act independently at the same hierarchical level. After a short discussion of the requirements that the authors expect a suitable formalism for interactive systems to fulfill, they describe the particular approach they have chosen and have embedded in an architectural description language called WRIGHT. The language divides a system into components and connectors, where the connectors serve as an abstraction of the interaction behavior of the system. The connectors consist of roles describing the expected local behavior of interacting components and a “glue” specification determining their interaction obligations. These concepts are illustrated by examples. A notation derived from CSP is used to describe roles and glues. CSP is also used as a semantic foundation for the language. Using CSP as a semantic foundation enables the authors to use existing analysis tools to prove such properties as deadlock freedom and compatibility of components. These technical issues are discussed extensively in the later sections. The paper finishes with a discussion of the design decisions of the proposed formalism. The paper explains the formalisms and concepts in clear, crisp language, and I could find only one typo (in Definition 10.2, P should be replaced by S ). At first sight, the discussions seem to be overly long, but the topic is relatively new, and a proper justification seems to be helpful.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments