基于π演算的软件体系结构求精研究
|
摘要
随着用户对软件产品性能需求的不断增加,软件规模越来越大,复杂性也越来越高。为保证软件质量、提高软件的可靠性,以软件体系结构为设计规范的开发方法越来越受到软件开发人员的关注。软件体系结构成为决定软件质量的主要因素,并发展成为软件工程领域的一个研究热点。然而,在软件开发过程中,从用户需求出发得到的体系结构初始模型的抽象粒度比较大,通常只反映了软件系统的某些主要的功能,很多的非功能属性以及实现细节都需要在逐步的细化过程中被添加到体系结构上,因此体系结构求精显得尤为重要。
体系结构求精是一项非常复杂而且困难的工作,不仅仅是简单地给出抽象体系结构的具体体系结构,而是要提供相关的规则和方法,保障体系结构正确求精。具体而言,体系结构求精关注两个方面:(1)体系结构求精方法,即采取何种手段、从哪个角度出发对体系结构求精,使得抽象的体系结构逐步细化为具体的体系结构;(2)体系结构求精规则,用于指导体系结构求精,为体系结构正确求精提供有力支持。
本文在D-ADL动态体系结构描述语言的形式框架规约下,提出基于π演算的体系结构求精方法。文章认为体系结构求精的关键在于求精结果应满足抽象系统与具体实现一致的约束。首先,从结构求精、行为求精和属性求精三个方面阐述了体系结构求精的方法、过程和规则;接着利用π演算的行为等价理论和检测工具MWB对该体系结构求精方法和规则进行验证。最后,以机票预定服务系统说明了上述求精方法、过程和规则的有效性。
Along with the adding of user’s requirement to software systems, the complexity of software systems becomes higher. In order to ensure the reliability of software systems, the developers set out to pay more and more attention to software architecture. Software architecture becomes the key factor of determining the software quality, and then becomes a hot topic in software engineer. But the initial software architecture just only contains some main functions of software, and another non-function attributes and details should be added to it as refinement is coming out, so that software refinement is seemed as a very important task.
Architecture refinement is such a complicated and difficult task that only giving the concrete software architecture to abstract software architecture is not enough. It should provide with rules to make sure that the architecture refinement is correct. To be more specific, architecture refinement concerns on two primary aspects. One is the method of architecture refinement. The appropriate method is to be used to get the concrete architecture from the abstract architecture with some approach. The other is the rules of software refinement. They are used to guide architecture refinement, and provide with powerful support for correct architecture refinement.
With the description framework of D-ADL, we propose the method of architecture refinement based on pi-calculus. At the same time, we think the key of software refinement is to make sure that the refinement satisfies for the constraints between the abstract system and concrete system. Firstly, it elaborates the refinement method, process and rules from the three sides namely structure, behavior and attribute. Secondly, it uses the behavior equivalence theory and MWB of pi-calculus to verify and detect the architecture refinement. Finally, it explains the validity of the above-mentioned refinement method with an ordering ticket system.
体系结构求精是一项非常复杂而且困难的工作,不仅仅是简单地给出抽象体系结构的具体体系结构,而是要提供相关的规则和方法,保障体系结构正确求精。具体而言,体系结构求精关注两个方面:(1)体系结构求精方法,即采取何种手段、从哪个角度出发对体系结构求精,使得抽象的体系结构逐步细化为具体的体系结构;(2)体系结构求精规则,用于指导体系结构求精,为体系结构正确求精提供有力支持。
本文在D-ADL动态体系结构描述语言的形式框架规约下,提出基于π演算的体系结构求精方法。文章认为体系结构求精的关键在于求精结果应满足抽象系统与具体实现一致的约束。首先,从结构求精、行为求精和属性求精三个方面阐述了体系结构求精的方法、过程和规则;接着利用π演算的行为等价理论和检测工具MWB对该体系结构求精方法和规则进行验证。最后,以机票预定服务系统说明了上述求精方法、过程和规则的有效性。
Along with the adding of user’s requirement to software systems, the complexity of software systems becomes higher. In order to ensure the reliability of software systems, the developers set out to pay more and more attention to software architecture. Software architecture becomes the key factor of determining the software quality, and then becomes a hot topic in software engineer. But the initial software architecture just only contains some main functions of software, and another non-function attributes and details should be added to it as refinement is coming out, so that software refinement is seemed as a very important task.
Architecture refinement is such a complicated and difficult task that only giving the concrete software architecture to abstract software architecture is not enough. It should provide with rules to make sure that the architecture refinement is correct. To be more specific, architecture refinement concerns on two primary aspects. One is the method of architecture refinement. The appropriate method is to be used to get the concrete architecture from the abstract architecture with some approach. The other is the rules of software refinement. They are used to guide architecture refinement, and provide with powerful support for correct architecture refinement.
With the description framework of D-ADL, we propose the method of architecture refinement based on pi-calculus. At the same time, we think the key of software refinement is to make sure that the refinement satisfies for the constraints between the abstract system and concrete system. Firstly, it elaborates the refinement method, process and rules from the three sides namely structure, behavior and attribute. Secondly, it uses the behavior equivalence theory and MWB of pi-calculus to verify and detect the architecture refinement. Finally, it explains the validity of the above-mentioned refinement method with an ordering ticket system.
引文
[1] 梅宏,申峻嵘.软件体系结构研究进展[J].软件学报,2006,17(6):1257-1258.
[2] 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 lndustry press,2000.1-4.
[3] Boehm.B.Engineering context (for software architecture),invited talk,In:GarlanD. ,ed.Proceedings of the 1st lnternational workshop on Architecture for Software Systems Seattle.Newyork:ACM Press,1995.1-8.
[4] 陈鑫.一种基于构件演算的主动构件精化方法[J].软件学报,2008,5,5(19):1134-1148.
[5] 曾红卫,缪淮扣.构件组合的抽象精化验证[J].软件学报,2008,5,5(19):1149-1159.
[6] 戎玫,张广泉.软件体系结构求精方法研究[J].计算机科学,2003,3(4):108-110.
[7] Luckham DC, Vera J. An event-based architecture definition language [J]. IEEE Transactions on Software Engineering, 1995, 21(9): 717-734.
[8] Moriconi M,Qian X , RiemeMchneider R . Correct Architecture Refinement[J].IEEE Tran.Soft.Eng.1995,21(4): 356-372.
[9] Garlen D.Style-Based Refinement for Software Architecture[J].ACM 0-89791-867-3.1996,10: 72-75.
[10] Lian Mo. Refinement methods for software architecture design using the software architecture model(D).Miami, Florida: Florida International University,2005.
[11] 张广泉.基于 XYZ/E 的软件体系结构描述语言研究[J].计算机科学,2000,27(9,专辑):155-157.
[12] 舒明.基于 XYZ/E 的软件体系结构描述和求精实例研究(D).北京:中国科学院软件研究所,2001.
[13] 晏荣杰,张广泉.一种基于构件的软件体系结构求精方法及其应用[J].重庆师范学院学报(自然科学版),2003,6(7):1-5.
[14] 李长云.基于体系结构的软件动态演化研究(D).浙江:浙江大学,2005.
[15] Victor B., Moller F..The mobility workbench: A tool for the pi-calculus. In: Processdings of the 6th International Conference on Computer Aided Verification, California, USA, 1994, 428-440.
[16] 冯冲,江贺,冯静芳编著.软件体系结构理论与实践(M).人民邮电出版社.2004.
[17] C. B. Jones. Systematic Software Development using VDM(M). Prentice-Hall, second edition, 1990. Out of print.
[18] J.-R. Abrial. The B-Book(M). Cambridge University Press, 1996.
[19] J. Woodcock and J. Davies. Using Z: Specification, Refinement, and Proof. Prentice-Hall, 1998.
[20] J. V. Guttag and J. J. Horning, editors. Larch: Languages and Tools for Formal Specification. Springer-Verlag, 1993. http://www.sds.lcs.mit.edu/spd/larch/.
[21] P. D. Mosses. CASL: A guided tour of its design. In J. L. Fiadeiro, editor, Recent Trends in Algebraic Development Techniques, WADT'98, volume 1589 of Lecture Notes in Computer Science, pages 216-240. Springer-Verlag, 1999.
[22] H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1985.
[23] C. George et al. The RAISE Specification Language. Prentice-Hall, 1992.
[24] R. Milner. Communication and Concurrency. Prentice-Hall, 1998.
[25] C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
[26] R. Milner. Communicating and Mobile Systems: the Pi-Calculus(M). Cambridge University Press, 1999.
[27] K. J. Turner, editor. Using Formal Description Techniques. John Wiley & Sons, 1993.
[28] C. George et al. The RAISE Development Method. Prentice-Hall, 1995.
[29] C. B. Jones. Systematic Software Development using VDM. Prentice-Hall, second edition, 1990. Out of print.
[30] J. A. Bergstra, A. Ponse, and S. A. Smolka, editors. Handbook of Process Algebra. Elsevier, 2001.
[31] Andreas Kerschbaumer. Behavioral Refinement of Software Architecture(D). Graz :Technischen University Graz, August 2002.
[32]R. Milner, J. Parrow, D. Walker, A Calculus Of Mobile Processes. Information and Computation, 1992, 100(1):1-40.
[33]D.Sangiorgi. Expressing Mobility in Process Algebras:First-Order and Higher-Order Paradigms. PhD Thesis, University of Edinburgh, 1992.
[34] Davide Sangiorgi, David Walker. the π -Calculus: a Theory of Mobile Process(M). Cambridge University Press, 2001.
[35]. Milner, R.: The polyadic π-Calculus: A tutorial. In Bauer, F.L., Brauer, W.,Schwichtenberg, H., eds.: Logic and Algebra of Specification, Berlin, Springer- Verlag (1993) 203-246.
[36] Parrow, J.: An Introduction to the π–Calculus. In Bergstra, J.A., Ponse, A., Smolka, S.A., eds.: Handbook of Process Algebra, Elsevier (2001) 479-543.
[37]田丽从,张莉,周伯生.软件体系结构的描述语言研究现状分析[J].计算机科学,2005,32(2):109-113.
[38]P. Oreizy, N. Medvidovic, R.N. Taylor. Architecture-Based Runtime Software Evolution. Proceedings of ICSE'20, Kyoto, Japan, IEEE Computer Society Press, 1998:177-186.
[39]M.Shaw, et al. Abstractions for Software Architecture and Tools to Support Them. IEEE Transactions on Software Engineering, 1995, 21(4): 314-335.
[40]D.Luckham, L.Augustin, J.Kenney. Specification and Analysis of System Architecture Using Rapide. IEEE Transactions on Software Engineering, 1995, 1(4):1-20.
[41]R.Allen. A Formal Approach to Software Architectures. PhD thesis, TR# CMU-CS-97-144, Carnegie Mellon University, School of Computer Science, May 1997.
[42]J.Magee, J.Kramer. Dynamic Structure in Software Architectures. Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering, 1996:3-13.
[43]D.Garlan, R.Monroe, D.Wile. ACME:Architectural Description of Component-Based Systems. Foundations of Component-Based Systems, G.T. Leavens, and M .Sitaraman, Cambridge University Press, 2000.
[44]骆华俊,唐稚松,郑建丹.可视化体系结构描述语言 XYZ/ADL[J].软件学报,2000,11(8):1024-1029.
[45]梅宏,陈锋,冯耀东,杨杰. ABC:基于体系结构、面向构件的软件开发方法[J].软件学报,2003,14(4):721-732.
[46]F.Oquendo, B.Warboys, R.Morrison, et al. ARCHWARE: Architecting Evolvable Software. EWSA 2004, 2004, LNCS 3047:257-271.
[47]F.Oquendo. π-ADL: an Architecture Description Language based on the higher-order typed π-calculus for specifying dynamic and mobile software architectures. ACM SIGSOFT Software Engineering Notes, May 2004,29(3): 1-14.
[48] 李长云,李赣生,何频捷.一种形式化的动态体系结构描述语言[J].软件学报,2006,17(6):1349-1359.
[49]任洪敏.基于π演算的软件体系结构形式化研究[D].复旦大学,上海,2003.
[50] J.Philipps, B.Rumpe. Refinement of Pipe and Filter Architectures. Proceedings of FM’99, 1999, LNCS 1708:96-115.
[51] D.Garlan. Style-based refinement for software architecture. Second International Software Architecture Workshop (ISAW-2).San Francisco,CA,October 1996:72-75.
[52] A.Egyed, R.N.Mehta, N.Medvidovic. Software Connectors and Refinement in Family Architectures. IW-SAPF 2000, Las Palmas de Gran Canaria, Spain, March 2000:96-106.
[53] D.Giannakopoulou. Model Checking for Concurrent Software Architectures. PhD Thesis, University of London, March 1999.
[54] Apple A.W. , MacQueen D.B.. Standard ML of New Jersey. In: Proceedings of the 3th Internetional Symposium on Programming Language Implementation and Logic Programming, New York, 1991, 1-13.
[55] Sala G. , Bordeaux L. , Schaerf M. . Describing and reasoning on Web services using process algebra. In: Proceedings of the 2nd IEEE Internetional conference on Web Services, San Diego, California, USA, 2004,43-50.
[56] Bjorn Victor. The Mobility Workbench User’s Guide Polyadic version 3.122. October 9, 1995.
[2] 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 lndustry press,2000.1-4.
[3] Boehm.B.Engineering context (for software architecture),invited talk,In:GarlanD. ,ed.Proceedings of the 1st lnternational workshop on Architecture for Software Systems Seattle.Newyork:ACM Press,1995.1-8.
[4] 陈鑫.一种基于构件演算的主动构件精化方法[J].软件学报,2008,5,5(19):1134-1148.
[5] 曾红卫,缪淮扣.构件组合的抽象精化验证[J].软件学报,2008,5,5(19):1149-1159.
[6] 戎玫,张广泉.软件体系结构求精方法研究[J].计算机科学,2003,3(4):108-110.
[7] Luckham DC, Vera J. An event-based architecture definition language [J]. IEEE Transactions on Software Engineering, 1995, 21(9): 717-734.
[8] Moriconi M,Qian X , RiemeMchneider R . Correct Architecture Refinement[J].IEEE Tran.Soft.Eng.1995,21(4): 356-372.
[9] Garlen D.Style-Based Refinement for Software Architecture[J].ACM 0-89791-867-3.1996,10: 72-75.
[10] Lian Mo. Refinement methods for software architecture design using the software architecture model(D).Miami, Florida: Florida International University,2005.
[11] 张广泉.基于 XYZ/E 的软件体系结构描述语言研究[J].计算机科学,2000,27(9,专辑):155-157.
[12] 舒明.基于 XYZ/E 的软件体系结构描述和求精实例研究(D).北京:中国科学院软件研究所,2001.
[13] 晏荣杰,张广泉.一种基于构件的软件体系结构求精方法及其应用[J].重庆师范学院学报(自然科学版),2003,6(7):1-5.
[14] 李长云.基于体系结构的软件动态演化研究(D).浙江:浙江大学,2005.
[15] Victor B., Moller F..The mobility workbench: A tool for the pi-calculus. In: Processdings of the 6th International Conference on Computer Aided Verification, California, USA, 1994, 428-440.
[16] 冯冲,江贺,冯静芳编著.软件体系结构理论与实践(M).人民邮电出版社.2004.
[17] C. B. Jones. Systematic Software Development using VDM(M). Prentice-Hall, second edition, 1990. Out of print.
[18] J.-R. Abrial. The B-Book(M). Cambridge University Press, 1996.
[19] J. Woodcock and J. Davies. Using Z: Specification, Refinement, and Proof. Prentice-Hall, 1998.
[20] J. V. Guttag and J. J. Horning, editors. Larch: Languages and Tools for Formal Specification. Springer-Verlag, 1993. http://www.sds.lcs.mit.edu/spd/larch/.
[21] P. D. Mosses. CASL: A guided tour of its design. In J. L. Fiadeiro, editor, Recent Trends in Algebraic Development Techniques, WADT'98, volume 1589 of Lecture Notes in Computer Science, pages 216-240. Springer-Verlag, 1999.
[22] H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1985.
[23] C. George et al. The RAISE Specification Language. Prentice-Hall, 1992.
[24] R. Milner. Communication and Concurrency. Prentice-Hall, 1998.
[25] C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
[26] R. Milner. Communicating and Mobile Systems: the Pi-Calculus(M). Cambridge University Press, 1999.
[27] K. J. Turner, editor. Using Formal Description Techniques. John Wiley & Sons, 1993.
[28] C. George et al. The RAISE Development Method. Prentice-Hall, 1995.
[29] C. B. Jones. Systematic Software Development using VDM. Prentice-Hall, second edition, 1990. Out of print.
[30] J. A. Bergstra, A. Ponse, and S. A. Smolka, editors. Handbook of Process Algebra. Elsevier, 2001.
[31] Andreas Kerschbaumer. Behavioral Refinement of Software Architecture(D). Graz :Technischen University Graz, August 2002.
[32]R. Milner, J. Parrow, D. Walker, A Calculus Of Mobile Processes. Information and Computation, 1992, 100(1):1-40.
[33]D.Sangiorgi. Expressing Mobility in Process Algebras:First-Order and Higher-Order Paradigms. PhD Thesis, University of Edinburgh, 1992.
[34] Davide Sangiorgi, David Walker. the π -Calculus: a Theory of Mobile Process(M). Cambridge University Press, 2001.
[35]. Milner, R.: The polyadic π-Calculus: A tutorial. In Bauer, F.L., Brauer, W.,Schwichtenberg, H., eds.: Logic and Algebra of Specification, Berlin, Springer- Verlag (1993) 203-246.
[36] Parrow, J.: An Introduction to the π–Calculus. In Bergstra, J.A., Ponse, A., Smolka, S.A., eds.: Handbook of Process Algebra, Elsevier (2001) 479-543.
[37]田丽从,张莉,周伯生.软件体系结构的描述语言研究现状分析[J].计算机科学,2005,32(2):109-113.
[38]P. Oreizy, N. Medvidovic, R.N. Taylor. Architecture-Based Runtime Software Evolution. Proceedings of ICSE'20, Kyoto, Japan, IEEE Computer Society Press, 1998:177-186.
[39]M.Shaw, et al. Abstractions for Software Architecture and Tools to Support Them. IEEE Transactions on Software Engineering, 1995, 21(4): 314-335.
[40]D.Luckham, L.Augustin, J.Kenney. Specification and Analysis of System Architecture Using Rapide. IEEE Transactions on Software Engineering, 1995, 1(4):1-20.
[41]R.Allen. A Formal Approach to Software Architectures. PhD thesis, TR# CMU-CS-97-144, Carnegie Mellon University, School of Computer Science, May 1997.
[42]J.Magee, J.Kramer. Dynamic Structure in Software Architectures. Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering, 1996:3-13.
[43]D.Garlan, R.Monroe, D.Wile. ACME:Architectural Description of Component-Based Systems. Foundations of Component-Based Systems, G.T. Leavens, and M .Sitaraman, Cambridge University Press, 2000.
[44]骆华俊,唐稚松,郑建丹.可视化体系结构描述语言 XYZ/ADL[J].软件学报,2000,11(8):1024-1029.
[45]梅宏,陈锋,冯耀东,杨杰. ABC:基于体系结构、面向构件的软件开发方法[J].软件学报,2003,14(4):721-732.
[46]F.Oquendo, B.Warboys, R.Morrison, et al. ARCHWARE: Architecting Evolvable Software. EWSA 2004, 2004, LNCS 3047:257-271.
[47]F.Oquendo. π-ADL: an Architecture Description Language based on the higher-order typed π-calculus for specifying dynamic and mobile software architectures. ACM SIGSOFT Software Engineering Notes, May 2004,29(3): 1-14.
[48] 李长云,李赣生,何频捷.一种形式化的动态体系结构描述语言[J].软件学报,2006,17(6):1349-1359.
[49]任洪敏.基于π演算的软件体系结构形式化研究[D].复旦大学,上海,2003.
[50] J.Philipps, B.Rumpe. Refinement of Pipe and Filter Architectures. Proceedings of FM’99, 1999, LNCS 1708:96-115.
[51] D.Garlan. Style-based refinement for software architecture. Second International Software Architecture Workshop (ISAW-2).San Francisco,CA,October 1996:72-75.
[52] A.Egyed, R.N.Mehta, N.Medvidovic. Software Connectors and Refinement in Family Architectures. IW-SAPF 2000, Las Palmas de Gran Canaria, Spain, March 2000:96-106.
[53] D.Giannakopoulou. Model Checking for Concurrent Software Architectures. PhD Thesis, University of London, March 1999.
[54] Apple A.W. , MacQueen D.B.. Standard ML of New Jersey. In: Proceedings of the 3th Internetional Symposium on Programming Language Implementation and Logic Programming, New York, 1991, 1-13.
[55] Sala G. , Bordeaux L. , Schaerf M. . Describing and reasoning on Web services using process algebra. In: Proceedings of the 2nd IEEE Internetional conference on Web Services, San Diego, California, USA, 2004,43-50.
[56] Bjorn Victor. The Mobility Workbench User’s Guide Polyadic version 3.122. October 9, 1995.