基于π演算的软件体系结构形式化研究
详细信息    本馆镜像全文|  推荐本文 |  |   获取CNKI官网全文
摘要
伴随计算机软件系统的规模和复杂程度不断提高,软件系统的结构变得日益复杂,软件设计重心从“算法+数据结构”设计转变成为体系结构设计。软件体系结构已经成为决定软件系统质量的重要因素,是软件产品线开发的关键技术之一,并因此成为当前软件工程领域的一个研究热点。
     体系结构规约是软件体系结构重要的研究课题。运用自然语言和图表描述体系结构存在众多不足,难以有效实现软件体系结构预期的诸多好处。于是众多学者开始运用通用的形式化方法、提出专门的体系结构描述语言描述软件体系结构,这两类方法具有各自的特点和不足,并且它们通常在软件体系结构的演化、精化、分析和实现等方面缺乏支持,从而阻碍了软件体系结构在实践当中的应用。
     据此,基于移动进程理论π演算,结合体系结构形式化方法和体系结构描述语言,我们提出软件体系结构形式化描述语言πADL,并以此作为基础,展开软件体系结构演化、精化、实现和分析等课题的探索和研究。具体如下:
     1.基于移动进程代数π演算,提出软件体系结构形式化描述语言πADL,形式化描述软件系统的结构和行为。提出端口组装和六种构件组装机制及相应的组装推导算法,以有效支持体系结构层次化配置。
     2.对动态体系结构进行研究,提出πADL描述动态体系结构的方法和相应的形式语义。该方法运用独立的π进程描述动态配置行为并,并与系统的计算行为交互,能够描述动态体系结构的诸多要素,包括动态演化的起因、时间、操作、非瞬时特性、断点继续执行等。
     3.对体系结构精化进行研究,指出复合构件层次规约存在的不足,提出复合行为和体系结构行为精化的概念、规约的方法和法则及推导算法,确保精化过程中高层体系结构的行为特性得到保持,并自动生成低层体系结构。
     4.对体系结构实现进行研究,指出运用现有构件技术实现体系结构存在的问题,分析体系结构领域和构件技术领域中软件构件的特点,提出面向体系结构的构件接口模型AOCIM,形式化给出AOCIM两级接口行为协议规约的方法,用以支持体系结构的实现。
     5.对体系结构分析进行研究,基于π演算基本理论,结合体系结构领域的需求和特点,形式化定义有关概念和多种进程关系,并以此作为理论基础,提出πADL规约的8种静态检测方法,用以提高体系结构规约和系统组装的质量。
     运用πADL及其相关研究工作,能够准确描述软件体系结构、推导系统的行为属性和分析系统规约的一致性,从而能够更好地支持体系结构驱动的软件开发方法,提升运用构件技术组装生成的软件系统的质量,向可预测系统组装这一
    
    软件工程的宏伟目标迈进一步。
As the size and complexity of software increase, the overall system structure is becoming more and more complicated. Consequently, software design has its focus shifted from algorithm and data structure to software architecture. Software architecture has become one of the important factors in assuring software system qualities and one of the key technologies to the development of software product line. Therefore, it is emerging as a discipline of intense research in software engineering.
    Architectural specification is an important research subject in software architecture. Current representation of software architecture is in terms of natural languages and box-and-arrow drawings, which is a great disadvantage for implementing what software architecture promises as a separate discipline. Now a large amount of researchers begin both exploiting general formal methods and developing special architecture description languages to characterize software architecture precisely. Both approaches have important benefits and some weakness, that is, none of them can alone provide sufficient basis for architectural description. Moreover, they usually provide little supports for architecture evolution, refinement, analysis, implementation, etc., thereby significantly hamper software architecture application in practice.
    A formal architecture description language, πADL, therefore, is proposed as groundwork in this dissertation, based on mobile process theory π calculus and combining formal methods and architecture description languages. Then a series of architectural subjects, such as evolution, refinement, analysis, etc. are explored and studied systematically. Specifically, major contributions are as follows:
    Firstly, a formal architecture description language πADL is proposed based on process algebra π calculus, to express the structure and behavior of software architecture in a precise and practical way. Furthermore, port composition and six component composition mechanisms as well as their compositional reasoning algorithms are provided to support hierarchical configurations of software architecture effectively.
    Secondly, an π ADL modeling approach and corresponding formal semantics for dynamic software architecture are developed, which independently models both architectural computation behaviors and dynamic reconfiguration behaviors, with responsibility for the interactions between them as well. It, therefore, can specify
    
    
    
    many aspects of dynamic architecture, including cause, time, operations and non-instantaneous change, etc.
    Thirdly, based on an insight into deficiencies in current architecture hierarchical configuration, ideas of composite behavior and architectural behavior refinement, related specification methods, principles and reasoning algorithm are proposed. They can ensure preserving the higher-level architectural behavior properties across refinement and generating lower-level architectures automatically and correctly.
    Fourthly, after illustrating of obstacles to implement software architecture according to today's component technologies, the characteristics of software components in both software architecture field and component technology field are analyzed. Then, an architecture-oriented component interface model (AOCIM) is proposed and a two-level formal specification method of AOCIM component behavior protocols is developed in order to support architecture implementation effectively.
    Finally, based on the theory of π calculus and aiming at the characteristics and requirements of software architecture, a collection of concepts and process relationships are defined formally as a theory foundation, then eight static check methods to determine consistency of π ADL architecture specifications are developed, to raise qualities of architectural specifications and system composition,
    Briefly, in terms of πADL and related research, software architecture can be described precisely, system behavior properties can be reasoned formally and architectural specification can be analyzed rigorousl
引文
[ 1 ] Shaw M, Garlan D. Software architecture: perspectives on an emerging discipline. Prentice Hall, Inc., Simon & Schuster Bejing Office, Tsinghua University Press, 1996.
    [2] 孙昌爱,金茂忠,刘超.软件体系结构研究综述.软件学报, 2002, 13(7) : 1228-1237.
    [3] Perry, D.E. Software engineering and software architecture. In: Feng, Yu-lin, ed. Proceedings of the International Conference on Software: Theory and Practice. Beijing: Electronic Industry Press, 2000. 1-4.
    [4] Boehm, B. Engineering context (for software architecture), invited talk, In: Garlan D., ed. Proceedings of the 1st International Workshop on Architecture for Software Systems Seattle. New York: ACM Press, 1995. 1-8.
    [5] Clements, P.C., Weiderman, N. Report on the 2nd international workshop on development and evolution of software architectures for product families. Technique Report, CMU/SEI-98-SR-003, Carnegie Mellon University, 1998.
    [6] Robert Allen and David Garlan. A formal approach to software architectures. In Jan van Leeuwen, editor, Proceedings of IFIP'92, pages 134-41. Elsevier Science Publishers B.V., September 1992.
    [7] MarkMoriconi and Xiaolei Qian. Correctness and composition of software architectures. In Proceedings of SIGSOFT '94: 2nd ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 164-74, New Orleans, LA, December 1994.
    [8] Paola Inverardi and Alex Wolf. Formal specification and analysis of software architectures using the chemical, abstract machine model. IEEE Transactions on Software Engineering, 21(4) :373-386, April 1995.
    [9] Mary Shaw, Robert DeLine, Daniel V. Klein, Theodore L. Ross, David M. Young, and Gregory Zelesnik. Abstractions for software architecture and tools to support them. IEEE Transactions on Software Engineering, 21(4) :314-335, April 1995.
    [10] J. Magee, N. Dulay, S. Eisenbach, and J. Kramer. Specifying distributed software architectures. In Proceedings of the Fifth European Software Engineering Conference, ESEC'95, September 1995.
    [11] Talor R N, Medvidovic N, Anderson K M et al. A component-and message-based architectural style for GUI software. IEEE Transactions on Software Engineering,
    
    1996,22(6) :390-406
    [12] David C Luckham, Lary M. Augustin, John J. Kenney, James Vera, Doug Bryan, and Walter Mann. Specification and analysis of system architecture using Rapide. IEEE Transactions on Software Engineering, 21(4) :336-355, April 1995.
    [13] R.Allen. A formal approach to software architecture. PhD thesis, Carnegie Mellon Univ., CMU Technical Report CMU-CS-97-114,May 1997.
    [14] Nenad Medvidovic, Richard N. Taylor. A classification and comparison framework for software architecture description languages. IEEE Transactions on Software Engineering, 2000 ,26(1) :70-93
    [15] James Rumbaugh, Michael Blaha, William Premeriani, Frederick Eddy, and William Lorenson. Object-Oriented Modeling and Design. Prentice Hall, Englewood Cliffs, NJ, 1991.
    [16] Grady Booch. Object-Oriented Analysis and Design with Applications. Benjamin/ Cummings, Redwood City, CA, 1993.
    [17] Rational Software Corporation. Unified modeling language (UML). Available at http://www.rational.com/uml/.
    [18] David Garlan and Mary Shaw. An introduction to software architecture. In V. Ambriola and G. Tortora, editors, Advances in Software Engineering and Knowledge Engineering, pages 1-39, Singapore, 1993. World Scientific Publishing Company.
    [19] Mary Shaw and David Garlan. Characteristics of higher-level languages for software architecture. Technical Report CMU-CS-94-210, Carnegie Mellon University, School of Computer Science, 1994. Also printed as CMU Software Engineering Institute Technical Report SEI-94-TR-23, ESC-TR-94-023.
    [20] Mary Shaw and David Garlan. Formulations and formalisms in software architecture. In Jan van Leeuwen, editor, Computer Science Today: Recent Trends and Developments, Lecture Notes in Computer Science, Volume 1000. Springer-Verlag, 1995.
    [21] Dewayne E. Perry and Alexander L. Wolf. Foundations for the study of software architecture. ACM SIGSOFT Software Engineering Notes, 17(4) :40-52, October 1992.
    [22] G.Berry and GBoudol. The chemical abstract machine. TheoreticalComputer Science, 96:217-248, 1992.
    [23] Sprivery J. The Notation: A Reference Manual. Englewood Cliffs: Prentice Hall,
    
    1989.
    [24] Norman Delisle and David Garlan. Applying formal specification to industrial problems: A specification of an oscilloscope. IEEE Software, 7(5) :29-37, September 1990.
    [25] David Garlan and David Notkin. Formalizing design spaces: Implicit invocationmechanisms. In VDM"91: Formal Software DevelopmentMethods. pages 31-44, Noordwijkerhout, The Netherlands, October 1991. Springer-Verlag, LNCS 551.
    [26] Kevin J. Sullivan, John Socha, andMarkMarchukov. Using formal methods to reason about architectural standards. In Proceedings of the 19th International. Conference on Software Engineering, Boston, MA, May 1997.
    [27] Gregory Abowd, Robert Allen, and David Garlan. Using style to understand descriptions of software architecture. In Proceedings of SIGSOFT'93: Foundations of Software Engineering, Software Engineering Notes 18(5) , pages 9-20. ACM Press, December 1993.
    [28] Gregory Abowd, Robert Allen, and David Garlan. Formalizing style to understand descriptions of software architecture. ACM Transactions on Software Engineering and Methodology, 4(4) :319-64, October 1995.
    [29] M. Moriconi, X. Qian, and R. Riemenschneider. Correct architecture refinement. IEEE Transactions on Software Engineering, 21(4) :356-372, April 1995.
    [30] GailC.Murphy, David Notkin, and Kevin Sullivan. Software reflexion models: Bridging the gap between source and high-level models. In Proceedings of SIGSOFT '95: Third ACM SIGSOFT Symposium on Foundations of Software Engineering, Software Engineering Notes 20(4) , pages 18-28, Washington, DC, October 1995. ACM Press.
    [31] Jeff Magee and Jeff Kramer. Dynamic structure in software architectures. In Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 3-14, San Fransisco, CA, October 1996.
    [32] V. R. Pratt. Modeling concurrency with partial orders. International Journal of Parallel Programming, 15(1) :33-71, February 1986.
    [33] R. Allen and D. Garlan. A formal basis for architectural connection. ACM Trans. on Software Engineering and Methodology, 6(3) :213-49, July 1997.
    [34] C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.
    
    
    [35] 焦文品,史忠植.用XYZ/E形式化体系结构风格.2000,11(3):410-415.
    [36] 骆华俊,唐稚松,郑建丹.可视化体系结构描述语言XYZ/ADL.软件学报,2000,11(8):1024—1029.
    [37] 唐稚松等.时序逻辑程序设计与软件工程(上册).北京:科学出版社,1999.
    [38] David Garlan, Robert T. Monroe, and David Wile. ACME: An architecture description interchange language, submitted for publication, January 1997.
    [39] David Garlan, Robert Allen, and John Ockerbloom. Exploiting style in architectural design environments. In Proceedings of SIGSOFT '94: 2nd ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 175-88, New Orleans, LA, December 1994. ACM Press.
    [40] 冯铁,张家晨,陈伟,等.基于框架和角色模型的软件体系结构规约.软件学报,2000,11(8):1078—1086.
    [41] 张家晨,冯铁,陈伟,等.基于主动连接的软件体系结构及其描述方法.软件学报,2000,11(8):1047-1052。
    [42] R. Milner, J. Parrow, and D.Walker. A calculus of mobile processes. Journal of Information and Computation,100:1-77, 1992.
    [43] Robin Milner. Communicating and Mobile Systerms:the π-Calculus. Cambridge University Press, 1999.
    [44] Davide Sangiorgi, David Walker. the π-Calculus: a Theory of Mobile Process. Cambridge University Press,2001.
    [45] 许文,方海,林惠民.π演算互模拟判定算法的优化和实现.软件学报,2001,12(2):159-166.
    [46] 杨芙清,梅宏,李克勤.软件复用与软件构件技术.电子学报.1999,27(2):68~75.
    [47] Luckham,D.,Vera, J.,Meldal,S.Three concepts of system architecture. Technical Report. CSL-TR-95-674, Stanford University, 1995.
    [48] 张世琨,张文娟,常欣,王立福,杨芙清.基于软件体系结构的可复用构件制作和组装.软件学报.2000,12(9):1351~1359.
    [49] 杨芙清,梅宏,李克勤,袁望洪,吴穹.支持构件复用的青鸟Ⅲ型系统概述.计算机科学,1999,26(5):50~55.
    [50] 梅宏,陈锋,冯耀东,杨杰.ABC:基于体系结构、面向构件的软件开发方法.2003,14(4):721-732.
    [51] Mei H, Chang JC, Yang FQ. Software component composition based on ADL and middleware. Science in China (F), 2001,44(2):136-151.
    
    
    [52] S.Ling, H.W.Schmidt, R.Fletcher. Constructing interoperable components in distributed systems. Proceedings of the TOOLS32 conference, 1999,274-284.
    [53] Murali Sitaraman Compositional performance reasoning. In: Proceedings of ICSE CBSE4. IEEE. 2001.
    [54] Q.-W. Xu and M. Swarup. Compositional reasoning using assumption commitment paradigm. In: H.Langmaack, A.Pnueli, W.-P.de Roever, ed. International Symposium, Compositionality-The Significant Difference. Springer-Verlag, 1998.
    [55] H. Schmidt. Trusted Components: Towards Automated Assembly with Predictable Properties. In: Proceedings of ICSE CBSE4. IEEE. 2001
    [56] J. Stafford and K. Wallnau. Predicting feature interactions in component-based systems. In Proceedings of the Workshop on Feature Interaction of Composed Systems, June 2001.
    [57] Bass,L.,Clements,,P.,Kazman,R. Software Architecture in Practice. Reading, MA:Addison Wesley, 1998
    [58] Kiczales,G.,Lamping,J.,Mendhekar,A.,et al. Aspect-Oriented programming. In: Bosch,J.,Mitchell,S.,eds. Proceedings of ECOOP'97,LNCS 1241. Berlin: Springer-Verlang, 1998. 220-242
    [59] A.W. Brown (Ed.). Component-Based Software Engineering. IEEE Computer Soc. Press, Los Alamitos CA, 1996
    [60] K. Bergner, A. Rausch, M. Sihling. Componentware:The Big Picture. International Workshop on Component-Based Software Engineering, Kyoto, 1998.
    [61] Object Management Group,Inc. The Common Object Request Broker: Architecture and Specification. Revision 2. 0,1995
    [62] R.Sessions. COM and DCOM: Microsoft's Vision for Distributed Objects. John Wiley & Sons, Inc., NY, 1997.
    [63] N.Mehta, N.Medvidovic, S.Phadke. Toward a taxonomy of Software Commectors. Proc. Of ICSE 2000
    [64] B.Spitznagel, David Garlan. A Compositional Approach for Constructing Connectors. The Working IEEE/IFIP Conference on Software Architecture, Royal Netherlands Academy of Arts and Sciences Amsterdam, The Netherlands, August 28-31,2001.
    [65] A.Lopes,M.Wermelinger J.Fideiro. Higher-Order Architectural Connectors. 2001.
    
    http:// www-ctp.di.fct.unl.pt/-mw/pubs/2001/bighocs.pdf.
    [66] C. Gacek and B. W. Boehm. Composing Components: How Does One Detect Potential Architectural Mismatches? Workshop on Compositional Software Architectures, Monterey, CA, January 1998
    [67] D. Garlan, R. Allen, and J. Ockerbloom. Architectural Mismatch, or, Why It's Hard to Build Systems out of Existing Parts. In Proceedings of the 17th International Conference on Software Engineering, Seattle, WA, April 1995
    [68] D.Garlan.Higher-order Connectors. In: Proceedings of Workshop on Compositional Software Architectures. California, 1998. 3-12
    [69] G.Denker, J.Meseguer, C.Talcott. Rewriting Semantics of Metaobjects and Composable Distributed Services.Internet report, Computer Science Laboratory, SRI International, 1999.
    [70] B.Spitznagel, David Garlan. A Compositional Approach for Constructing Connectors. The Working IEEE/IFIP Conference on Software Architecture, Royal Netherlands Academy of Arts and Sciences Amsterdam, The Netherlands, August 28-31,2001.
    [71] M.Wermelinger, A.Lopes and J.L.Fiadeiro, Superposing Connectors.In Proc. 10th International Workshop on Software Specification and Design, pp. 87-94, IEEE Computer Society Press 2000.
    [72] Chris Salzmann. Managing shared business objects. In W. Emmerich, editor, Proceedings of ICSE 21: Workshop on Engineering Distributed Objects, 1999.
    [73] D.Garlan. Software Architecture: a Roadmap. In: A. Finkelstein, Ed. Proceedings of The Future of Software Engineering. ACM Press, 2000. 93-101
    [74] SUN Chang-ai, JIN Mao-zhong, LIU Chao. Overviews on Software Architecture Research. Journal of Software. 2002, 13(7) :1228-1237
    [75] Bernhard Deifel and Chris Salzmann. Requirements and conditions for dynamics in evolutionary software systems. In Proceedings of the IWPSE'99 Intl. Workshop on Principles of Software Evolution, 1999.
    [76] Chris Salzmann and Maurice Schoenmakers. Dynamics and mobility in software architecture. In Jan Bosch, editor, Proceedings of NOSA 99-Second Nordic Workshop on Software Architecture, 1999. 184.
    [77] R.J.Allen, R.Douence, D.Garlan. Specifying and Analyzing Dynamic Software Architectures.In: Proceedings of the Fundamental Approaches to Software Engineering. Springer-Verlag , 1998. 21-37.
    
    
    [78] Peyman Oreizy. Issues in Modeling and Analyzing Dynamic Software Architectures. In: Proceedings of the International Workshop on the Role of Software Architecture in Testing and Analysis. 1998.
    [79] P. Binns, M. Engelhart, M. Jackson, and S. Vestal. Domain-Specific Software Architectures for Guidance, Navigation, and Control. International Journal of Software Engineering and Knowledge Engineering, vol. 6, no. 2, 1996.
    [80] M. M. Gorlick and R. R. Razouk. Using Weaves for Software Construction and Analysis. In Proceedings of the 13th International Conference on Software Engineering (ICSE13) , pages 23-34, Austin, TX, May 1991.
    [81] M. Moriconi, X. Qian, and R. A. Riemenschneider. Correct Architecture Refinement. IEEE Transactions on Software Engineering, pages 356-372, April 1995.
    [82] D. Garlan. Style-Based Refinement for Software Architecture. In A. L. Wolf, ed., Proceedings of the Second International Software Architecture Workshop (ISAW-2) , pages 72-75, San Francisco, CA, October 1996
    [83] Ivica Crnkovic.Component-based Software Engineering New Challenges in Software Development. http://www.mrtc.mdh.se/publications/0328. pdf.
    [84] Oriezy, P., Gorlick, M.M., et al. An Architecture-Based Approach to Self-Adaptive Software. IEEE Intelligent Systems. 1999, 14(3) :54-62.
    [85] J. Han. Temporal logic based specification of component interaction protocols. In: Proceedings of New Issues of Object Interoperability. Springer-Verlag, 2000. 43-52
    [86] R. H. Reussner. Enhanced component interfaces to support dynamic adaptation and extension. In: Proceedings of 34th Hawaii International Conference on System Sciences. IEEE Press, 2001. 76-86
    [87] H. Giese. Contract-based component system design. In J. Ralph and H. Sprague: Proceedings of 33rd Hawaii International Conference on System Sciences. IEEE Press.2000. 143-153
    [88] C. Canal, L. Fuentes, et al. Extending CORBA Interfaces with Protocols. The Computer Journal, 2001, 44(5) : 448-462
    [89] A. Vallecillo, J. Hernandez, and J. M. Troya. Object interoperability. In: Proceedings of Object-Oriented Technology: COOP' 99 Workshop Reader. Springer-Verlag, 1999. 1-21.
    [90] Plasil, F., Visnovsky, S., Besta, M. Bounding Component Behavior via Protocols.
    
    In: Proceedings of TOOLS USA '99. Santa Barbara, USA, 1999. 387-398
    [91] Peyman Oreizy, Nenad Medvidovic, et al. Software Architecture and Component Technologies: Bridging the Gap. In: Proceedings of the OMG-DARPA Workshop on Compositional Software Architectures.1998.
    [92] R. Natarajan, D.S. Rosenblum. Supporting Architectural Concerns in Component Interoperability. IEE Proceedings-Software. 2000,147(6):215-223.
    [93] P.Tarr, H. Ossher. Multi-Dimensional Separation of Concerns and The Hyperspace Approach. In: M. Aksit: Proceedings of the Symposium on Software Architectures and Component Technology:The State of the Art in Software Development. Kluwer Academic Publishers,2000.293-323.
    [94] AT&T. Best Current Practices: Software Architecture Validation. AT&T, 1993.
    [95] Rick Kazrnan, Len Bass, Gregory Abowd, and MikeWebb. SAAM: A method for analyzing the properties of software architecture. In Proceedings of the 16th International Conference on Software Engineering, pages 81-90, Sorrento. Italy,May 1994.
    [96] Marlo, R., Barbacci, S., Jeromy, C., et al. Steps in an architecture tradeoff analysis method: quality attribute models and analysis. Techical Report,CMU/SEI-97-TR-029, Carnegie Mellon University, 1997.
    [97] Debra, J.R., Alexander, L.W. Software testing at the architecture level. In:Proceedings of the ISAW. 1996.68-71. http://www, ics.uci.edu/-djr/papers.html.
    [98] 云晓春,方滨兴.基于构件设计的正确性验证.小型微型计算机系统,1999,20(5):330-334.
    [99] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes---parts I and Ⅱ. Information and Computation, 100:1-77, 1992.
    [100] 梅宏,陈锋,冯耀东,杨杰.ABC:基于体系结构、面向构件的软件开发方法.软件学报,2003,14(4):721-732

© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号

地址:北京市海淀区学院路29号 邮编:100083

电话:办公室:(+86 10)66554848;文献借阅、咨询服务、科技查新:66554700