基于构件的形式化方法在软件开发中的应用研究
摘要
基于构件的软件开发是提高软件生产率、提高软件质量、解决软件危机的重要方法,是软件复用领域的研究热点;解决软件危机的另一方面是如何建立严格的数学方法,如何进行形式化软件开发。如何将基于构件的软件开发和形式化方法相结合是软件开发发展的重要方向。
鉴于基于构件的软件开发缺少严密的数学推理,没有形式化的规格说明,大部分开发过程采用自然语言进行描述,本文给出了基于构件的形式化软件开发模型,重点研究该模型中需求分析的形式化、设计阶段软件体系结构、形式化构件模型及形式化构件交互。针对传统软件开发中需求分析不准确和二义性等问题,使用Z语言对需求分析形式化表示进行了扩充,并通过实例对形式化表示进行了说明,其具有消除需求分析的二义性和不一致性的能力。需求分析关注如何刻画问题空间,软件体系结构关注如何刻画解空间,如何根据需求分析获得软件体系结构没有定论,文中给出了一种基于功能和三层开发框架获取概要设计软件体系结构的方法。针对现阶段构件接口定义中构件行为和交互协议信息缺乏,利用形式化语言session type定义了构件、连接子以及构件交互语义,完成了详细设计阶段软件体系结构的精化,增强了构件接口信息的描述能力。
最后,将基于构件的形式化软件开发模型应用于某公司OA中的办公用品管理系统开发,结果表明该模型具有一定的可行性和适用性,且具有一定的实际应用价值。
Component-based software development is an important method to improve software productivity and quality, and solve software crisis. It is a research focus of the area of software reuse, and its key technology is the software architecture and component model. It is the other way to solve software crisis how to establish a strict mathematical methods to conduct formal software development. It is an important direction of software development that how to combine component-based software development and formal methods.
Component-based software development lacks rigorous mathematical reasoning, and has no formal specification. Most of the development process is described using natural language. So this paper presents a component-based formal software development model. It focuses on formal requirements analysis, software architecture of design phase and formal component model and interaction. Requirements analysis is inaccurate and ambiguous in the traditional software development. The paper expands formal requirements analysis using the Z language, and describes it through examples. It has capacity to eliminate ambiguity and inconsistency of requirements analysis. Requirements analysis is concerned about how to describe the problem space, while software architecture concerned about how to describe the solution space, so it is a problem that how to get software architecture from requirements analysis. The paper presents a method to implement it based on function and three-tier development framework. Because of lack of component behavior and interaction protocol in its interface definition for this stage, the paper defines components, connectors and a semantic of component interactive. The definition enhances description capacity of information of component interface.
Finally, the component-based formal software development model is applied to development of office supplies management system of a OA system of some company. The results show that the model has a certain feasibility, applicability, and practical value.
鉴于基于构件的软件开发缺少严密的数学推理,没有形式化的规格说明,大部分开发过程采用自然语言进行描述,本文给出了基于构件的形式化软件开发模型,重点研究该模型中需求分析的形式化、设计阶段软件体系结构、形式化构件模型及形式化构件交互。针对传统软件开发中需求分析不准确和二义性等问题,使用Z语言对需求分析形式化表示进行了扩充,并通过实例对形式化表示进行了说明,其具有消除需求分析的二义性和不一致性的能力。需求分析关注如何刻画问题空间,软件体系结构关注如何刻画解空间,如何根据需求分析获得软件体系结构没有定论,文中给出了一种基于功能和三层开发框架获取概要设计软件体系结构的方法。针对现阶段构件接口定义中构件行为和交互协议信息缺乏,利用形式化语言session type定义了构件、连接子以及构件交互语义,完成了详细设计阶段软件体系结构的精化,增强了构件接口信息的描述能力。
最后,将基于构件的形式化软件开发模型应用于某公司OA中的办公用品管理系统开发,结果表明该模型具有一定的可行性和适用性,且具有一定的实际应用价值。
Component-based software development is an important method to improve software productivity and quality, and solve software crisis. It is a research focus of the area of software reuse, and its key technology is the software architecture and component model. It is the other way to solve software crisis how to establish a strict mathematical methods to conduct formal software development. It is an important direction of software development that how to combine component-based software development and formal methods.
Component-based software development lacks rigorous mathematical reasoning, and has no formal specification. Most of the development process is described using natural language. So this paper presents a component-based formal software development model. It focuses on formal requirements analysis, software architecture of design phase and formal component model and interaction. Requirements analysis is inaccurate and ambiguous in the traditional software development. The paper expands formal requirements analysis using the Z language, and describes it through examples. It has capacity to eliminate ambiguity and inconsistency of requirements analysis. Requirements analysis is concerned about how to describe the problem space, while software architecture concerned about how to describe the solution space, so it is a problem that how to get software architecture from requirements analysis. The paper presents a method to implement it based on function and three-tier development framework. Because of lack of component behavior and interaction protocol in its interface definition for this stage, the paper defines components, connectors and a semantic of component interactive. The definition enhances description capacity of information of component interface.
Finally, the component-based formal software development model is applied to development of office supplies management system of a OA system of some company. The results show that the model has a certain feasibility, applicability, and practical value.
引文
[1]杨芙清.构件技术引领软件开发新潮流.中国计算机用户.2005,2,(6):42-43页
[2] Li Ke-qin,Guo Li-feng,Mei Hong. An overview of JB (Jade Bird) component library system JBCL. In: Chen Jian,Li Ming-shu,Christine Minginset aleds. Proceedings of the 24th International Conference TOOLS Asia. California:IEEE Computer Society Press,1997:261-267P
[3]任洪敏,钱乐秋.构件组装及其形式化推导研究.软件学报.2003,14,(6):1066-1074页
[4]李阳,吴朝晖.一种形式化构件集成语义的研究.浙江大学学报(工学版).2004,38,(2):135-140页
[5]钟林辉,谢冰,邵维忠.扩充CDL支持基于构件的系统组装与演化.计算机研究与发展.2002,1139,(110):1361-1365页
[6]刘辉,缪淮扣,刘静.基于虚构件的软件开发研究.应用科学学报.2004,22,(2):211-216页
[7]刘奕明.基于特征模型和构件语义的概念体系结构设计.软件学报.2006,17,(6):1307-1317页
[8]张世瑕,张文娟,常欣,王立福,杨芙清.基于软件体系结构的可复用构件制作和组装.软件学报.2001,12,(9):1351-1359页
[9]李欣,张路,谢冰,杨芙清.基于构件的软件版本管理系统.电子学报.2000,28[11]:119-121页
[10] ClementsP,BaehmannF,BassL,NordRL,GarlanD,IversJ,LittleR,NordR, StaffordJ. Documenting Software Arehiteetures : Viewsand Beyond[M] .Boston:Addison Wesley Professional,2002:20-60P
[11] Medvidovie N.,RichardNT. A classification and comparison frameworkforsoftware architecture description languages .IEEE Trans. On Software Engineering,2000,26(l):70-93 P
[12] Bruneton E,Coupaye T,Stefani JB. Reeursive and dynamic software composition with sharing. In : Proc. of the 7th Workshop on Component-Oriented Programming , http:// fractal. ow2. org/ current/ fractalWCOP02.pdf. 2002:1-7P
[13] DaiL,CooperK. Modeling and analysis of non-functional requirements as aspects in a UML based software architecture design. In:Proc. of the 6th International Conf. on Software Engineering , Artificial Intelligence , Networking and Parallel/Distributed Computing.2005:178-183 P
[14] Dobrica, NiemelaE E. A survey on Sortware architecture analysis methods . IEEE Trans. on Software Engineering, 2002,28(7):638-653 P
[15] Clements P, Kazman R, Klein M. Evaluating Software Architectures: Methods and Case Studies[M]. Boston: Addison Wesley Professional, 2002:18-30 P
[16] Magee J,Kramer J. Dynamic structure in software architectures. In: Kaise GE,ed. Proceedings of the ACM SIGSOFT’96: the 4th Symposium on the Foundations of Software Engineering . New York: ACM Press,1996:3-14 P
[17] Shaw M, DeLine R, Klen DV. Abstractions for software architecture and tools to support them. http://www.cs.toronto.edu/km/tropos/UniCon.pdf. 1995:2-5P
[18] D Garlan, R Monroe, D Wile. ACME: An architecture description interchange language. In: Proc of CASCON97. Toronto IBM Press, 1997: 169-183 P
[19] C L David, V James. An event-based architecture definition language. IEEE Trans on Software Engineering, 1995,21(9):717-734 P
[20]杨芙清,梅宏,李克勤.软件复用与软件构件技术.电子学报.1999,28[2] :68-75页
[21] Szyperski C, Gruntz D, Murer S. Component Software: Beyond Object–Oriented Programming. New Jersey: Addison Wesley, 2002:50-53P
[22] Hazleen Aris1 , Siti Salwah Salim. Refinement of Component Model Standards and Conventions. ICSR 2008, LNCS 5030, 2008 :278-281P
[23] Box D. Essential COM.New Jersey:Addison-Wesley,1998:50-53P
[24]陈波,李舟军,陈火旺.构件模型研究综述.计算机工程与科学.2008,30[1] :105-109页
[25]王社伟,宋敏.COM组件技术的原理及应用探讨.2005,10:34-35页
[26] Wang N, Schmit D C, O’Ryan C O.Overview of CORBA Component Model . New Jersey: Addison-Wesley,2000:3-5P
[27] OMG.CORBA Component Model Specification v4. 0 [S].2006:2-3P
[28] Plasil F, Balek D, Janecek R. SOFA/DCUP:Architecture for Component Trading and Dynamic Updating. http://dsrg.mff.cuni.cz/publications/ ICCDS98.pdf,1998:5-6P
[29] Arbab F. Reo: A Channel-Based Coordination Model for Component Composition . Mathematical Structures in Computer Science, 2004,14(3):329-366P
[30]杨芙清,梅宏,李克勤,袁望洪,吴穹.支持构件复用的青鸟III型系统概述.1999,26,(5):50-55页
[31]贾育.基于演化构件的软件复用方法.中国科学院软件研究所博士学位论文.2002:48-51页
[32]陈火旺,王戟,董威.高可信软件工程技术.2003,31(12A):1933-1938页
[33]古天龙,董荣胜.软件开发的形式化方法.高等教育出版社,2005:159-162页
[34] Petri C A. Kommunikation mit automaten. Institute fur InstrumentelleMathematik, Schriften des IIM 2, Bonn, 1962:2-3P
[35] J.L.Peterson, Petri Net Theory and the Modeling of Systems, Prentice -Hall,1981:32-36P
[36]蒋忠远.基于Petri网的形式化软件开发方法研究.西华大学硕士学位论文.2008:25-36页
[37] C. A. R. Hoare, Communicating Sequential Processes. http://www.usingcsp. com/cspbook.pdf,2004: 2-3P
[38] Michal Spibey J. The Z Notation(2nd Edition). Prentiee Hall,1992:100-120P
[39] K. Honda. Types for Dyadic Interaction. In CONCUR’93, volume 715 of LNCS,. Springer-Verlag, 1993:509-523P
[40] Mariangiola Dezani-Ciancaglini, Dimitris Mostrous, Nobuko Yoshida, and Sophia Drossopoulou. Session Types for Object-Oriented Languages. LNCS 4067, 2006:328-352P
[41]林惠民,张文辉.模型检测:理论、方法与应用.电子学报.2002,30 (12A):1907-1912页
[42] Kevin J. Sullivan, John Socha, Mark Marchukov. Using Formal Methods to Reason about Architectural Standards. ACM 0-89791-914-9/97/05,1997: 5-9P
[43] Philip T Cox, Baoming Song. A Formal Model for Component-Based Software.http://www.cs.dal.ca/~pcox/publications/Components-HCC01.pdf. 2001: 6-8P
[44]陈波.基于软件体系结构的构件模型和语言研究.国防科学技术大学博士学位论文.2007:1-50页
[45]梅宏,申峻嵘.软件体系结构研究进展.软件学报.2006,17(6):1257-1275页
[46] Bass L, Clements P, Kazman R. Software Architecture in Practice.2nd ed. Boston: Addison Wesley Professional,2003:80-95P
[47] IEEE.IEEE recommended practice for architectural description of software -intensive systems.IEEE,IEEE 2000:1471-2000P
[48] P.Kruehien, H.ObbinLk, J.Stafford.ThePast, Present and Future of Software Architecture.IEEE Software,2006,23(2):22-30P
[49] E.W.Dijkstra.The Structure of the THE-MultiProgramming System. Communications of the ACM,1968,11(5):341-346P
[50] M.Shaw, R.DeLine, D.V.Klein, T.L.Ross, D.M.Young and G.Zelesnik. Abstractions for Software Architecture and Tools to Support Them. IEEE Transactions on Software Engineering,1995,21(4):314-335P
[51] R.Allen.A Formal Approach to Software Architecture. PhD Thesis, Carnegie Mellon University, CMU Technical Report CMU-CS-97-144,1997:20-28P
[52]梅宏,陈锋,冯耀东,杨杰.ABC:基于体系结构、面向构件的软件开发方法.软件学报.2003,14,(4):721-732页
[53] D.C.Luekham, J.Vera.An Event-Based Architecture Definition Language. IEEE Transactions on Software Engineering,1995,2(9):717-734P
[54] J.Magee, J.Kramer. Dynamic Structure in Software Architectures. In Proeeedings of Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering, SanFraneiseo,USA,October,1996,10:3-14P
[55] N.Medvidovie, D.S.Rosenblum, R.N.Taylor.A Language and Environment for Architecture-based Software Development and Evolution. In Proceedings of the 21st international conference on Software engineering. NewYork, ACMPress, May,1999:44-53P
[56] D.Garlan,R.Monroe, D.Wile. ACME:Architectural Description of Component- Based Systems.Foundations of Component-Based Systems, Cambridge University Press,2000:47-68P
[57] E.M.Dashofy, A.Hoek, R.N.Taylor. A Comprehensive Approach for the Development of Modular Software Architecture Deseription Languages.ACM Transactions on Software Engineering and Methodology,2005, 26(1):199-245P
[58] Medvidovic N.,Richard NT.A classification and comparison framework for software architecture description languages.IEEE Trans.on Software Engineering, 2000,26(1):70-93P
[59]杨金翠,袁玉宇.基于构件技术的软件开发模式研究.软件工程与标准化.2007,10:33-36页
[60]钱忠胜,缪淮扣.面向构件的系统开发及其形式化.计算机应用与软件.2008,25(3):99-101页
[2] Li Ke-qin,Guo Li-feng,Mei Hong. An overview of JB (Jade Bird) component library system JBCL. In: Chen Jian,Li Ming-shu,Christine Minginset aleds. Proceedings of the 24th International Conference TOOLS Asia. California:IEEE Computer Society Press,1997:261-267P
[3]任洪敏,钱乐秋.构件组装及其形式化推导研究.软件学报.2003,14,(6):1066-1074页
[4]李阳,吴朝晖.一种形式化构件集成语义的研究.浙江大学学报(工学版).2004,38,(2):135-140页
[5]钟林辉,谢冰,邵维忠.扩充CDL支持基于构件的系统组装与演化.计算机研究与发展.2002,1139,(110):1361-1365页
[6]刘辉,缪淮扣,刘静.基于虚构件的软件开发研究.应用科学学报.2004,22,(2):211-216页
[7]刘奕明.基于特征模型和构件语义的概念体系结构设计.软件学报.2006,17,(6):1307-1317页
[8]张世瑕,张文娟,常欣,王立福,杨芙清.基于软件体系结构的可复用构件制作和组装.软件学报.2001,12,(9):1351-1359页
[9]李欣,张路,谢冰,杨芙清.基于构件的软件版本管理系统.电子学报.2000,28[11]:119-121页
[10] ClementsP,BaehmannF,BassL,NordRL,GarlanD,IversJ,LittleR,NordR, StaffordJ. Documenting Software Arehiteetures : Viewsand Beyond[M] .Boston:Addison Wesley Professional,2002:20-60P
[11] Medvidovie N.,RichardNT. A classification and comparison frameworkforsoftware architecture description languages .IEEE Trans. On Software Engineering,2000,26(l):70-93 P
[12] Bruneton E,Coupaye T,Stefani JB. Reeursive and dynamic software composition with sharing. In : Proc. of the 7th Workshop on Component-Oriented Programming , http:// fractal. ow2. org/ current/ fractalWCOP02.pdf. 2002:1-7P
[13] DaiL,CooperK. Modeling and analysis of non-functional requirements as aspects in a UML based software architecture design. In:Proc. of the 6th International Conf. on Software Engineering , Artificial Intelligence , Networking and Parallel/Distributed Computing.2005:178-183 P
[14] Dobrica, NiemelaE E. A survey on Sortware architecture analysis methods . IEEE Trans. on Software Engineering, 2002,28(7):638-653 P
[15] Clements P, Kazman R, Klein M. Evaluating Software Architectures: Methods and Case Studies[M]. Boston: Addison Wesley Professional, 2002:18-30 P
[16] Magee J,Kramer J. Dynamic structure in software architectures. In: Kaise GE,ed. Proceedings of the ACM SIGSOFT’96: the 4th Symposium on the Foundations of Software Engineering . New York: ACM Press,1996:3-14 P
[17] Shaw M, DeLine R, Klen DV. Abstractions for software architecture and tools to support them. http://www.cs.toronto.edu/km/tropos/UniCon.pdf. 1995:2-5P
[18] D Garlan, R Monroe, D Wile. ACME: An architecture description interchange language. In: Proc of CASCON97. Toronto IBM Press, 1997: 169-183 P
[19] C L David, V James. An event-based architecture definition language. IEEE Trans on Software Engineering, 1995,21(9):717-734 P
[20]杨芙清,梅宏,李克勤.软件复用与软件构件技术.电子学报.1999,28[2] :68-75页
[21] Szyperski C, Gruntz D, Murer S. Component Software: Beyond Object–Oriented Programming. New Jersey: Addison Wesley, 2002:50-53P
[22] Hazleen Aris1 , Siti Salwah Salim. Refinement of Component Model Standards and Conventions. ICSR 2008, LNCS 5030, 2008 :278-281P
[23] Box D. Essential COM.New Jersey:Addison-Wesley,1998:50-53P
[24]陈波,李舟军,陈火旺.构件模型研究综述.计算机工程与科学.2008,30[1] :105-109页
[25]王社伟,宋敏.COM组件技术的原理及应用探讨.2005,10:34-35页
[26] Wang N, Schmit D C, O’Ryan C O.Overview of CORBA Component Model . New Jersey: Addison-Wesley,2000:3-5P
[27] OMG.CORBA Component Model Specification v4. 0 [S].2006:2-3P
[28] Plasil F, Balek D, Janecek R. SOFA/DCUP:Architecture for Component Trading and Dynamic Updating. http://dsrg.mff.cuni.cz/publications/ ICCDS98.pdf,1998:5-6P
[29] Arbab F. Reo: A Channel-Based Coordination Model for Component Composition . Mathematical Structures in Computer Science, 2004,14(3):329-366P
[30]杨芙清,梅宏,李克勤,袁望洪,吴穹.支持构件复用的青鸟III型系统概述.1999,26,(5):50-55页
[31]贾育.基于演化构件的软件复用方法.中国科学院软件研究所博士学位论文.2002:48-51页
[32]陈火旺,王戟,董威.高可信软件工程技术.2003,31(12A):1933-1938页
[33]古天龙,董荣胜.软件开发的形式化方法.高等教育出版社,2005:159-162页
[34] Petri C A. Kommunikation mit automaten. Institute fur InstrumentelleMathematik, Schriften des IIM 2, Bonn, 1962:2-3P
[35] J.L.Peterson, Petri Net Theory and the Modeling of Systems, Prentice -Hall,1981:32-36P
[36]蒋忠远.基于Petri网的形式化软件开发方法研究.西华大学硕士学位论文.2008:25-36页
[37] C. A. R. Hoare, Communicating Sequential Processes. http://www.usingcsp. com/cspbook.pdf,2004: 2-3P
[38] Michal Spibey J. The Z Notation(2nd Edition). Prentiee Hall,1992:100-120P
[39] K. Honda. Types for Dyadic Interaction. In CONCUR’93, volume 715 of LNCS,. Springer-Verlag, 1993:509-523P
[40] Mariangiola Dezani-Ciancaglini, Dimitris Mostrous, Nobuko Yoshida, and Sophia Drossopoulou. Session Types for Object-Oriented Languages. LNCS 4067, 2006:328-352P
[41]林惠民,张文辉.模型检测:理论、方法与应用.电子学报.2002,30 (12A):1907-1912页
[42] Kevin J. Sullivan, John Socha, Mark Marchukov. Using Formal Methods to Reason about Architectural Standards. ACM 0-89791-914-9/97/05,1997: 5-9P
[43] Philip T Cox, Baoming Song. A Formal Model for Component-Based Software.http://www.cs.dal.ca/~pcox/publications/Components-HCC01.pdf. 2001: 6-8P
[44]陈波.基于软件体系结构的构件模型和语言研究.国防科学技术大学博士学位论文.2007:1-50页
[45]梅宏,申峻嵘.软件体系结构研究进展.软件学报.2006,17(6):1257-1275页
[46] Bass L, Clements P, Kazman R. Software Architecture in Practice.2nd ed. Boston: Addison Wesley Professional,2003:80-95P
[47] IEEE.IEEE recommended practice for architectural description of software -intensive systems.IEEE,IEEE 2000:1471-2000P
[48] P.Kruehien, H.ObbinLk, J.Stafford.ThePast, Present and Future of Software Architecture.IEEE Software,2006,23(2):22-30P
[49] E.W.Dijkstra.The Structure of the THE-MultiProgramming System. Communications of the ACM,1968,11(5):341-346P
[50] M.Shaw, R.DeLine, D.V.Klein, T.L.Ross, D.M.Young and G.Zelesnik. Abstractions for Software Architecture and Tools to Support Them. IEEE Transactions on Software Engineering,1995,21(4):314-335P
[51] R.Allen.A Formal Approach to Software Architecture. PhD Thesis, Carnegie Mellon University, CMU Technical Report CMU-CS-97-144,1997:20-28P
[52]梅宏,陈锋,冯耀东,杨杰.ABC:基于体系结构、面向构件的软件开发方法.软件学报.2003,14,(4):721-732页
[53] D.C.Luekham, J.Vera.An Event-Based Architecture Definition Language. IEEE Transactions on Software Engineering,1995,2(9):717-734P
[54] J.Magee, J.Kramer. Dynamic Structure in Software Architectures. In Proeeedings of Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering, SanFraneiseo,USA,October,1996,10:3-14P
[55] N.Medvidovie, D.S.Rosenblum, R.N.Taylor.A Language and Environment for Architecture-based Software Development and Evolution. In Proceedings of the 21st international conference on Software engineering. NewYork, ACMPress, May,1999:44-53P
[56] D.Garlan,R.Monroe, D.Wile. ACME:Architectural Description of Component- Based Systems.Foundations of Component-Based Systems, Cambridge University Press,2000:47-68P
[57] E.M.Dashofy, A.Hoek, R.N.Taylor. A Comprehensive Approach for the Development of Modular Software Architecture Deseription Languages.ACM Transactions on Software Engineering and Methodology,2005, 26(1):199-245P
[58] Medvidovic N.,Richard NT.A classification and comparison framework for software architecture description languages.IEEE Trans.on Software Engineering, 2000,26(1):70-93P
[59]杨金翠,袁玉宇.基于构件技术的软件开发模式研究.软件工程与标准化.2007,10:33-36页
[60]钱忠胜,缪淮扣.面向构件的系统开发及其形式化.计算机应用与软件.2008,25(3):99-101页