动态软件体系结构建模与模型验证方法的研究
摘要
随着科技的发展,软件系统所处的环境也随之改变,传统的静态软件体系结构已不再适应当前用户的需求,而动态软件体系结构不仅能够增强用户的自定义性和可扩展性,也能降低系统开发的费用和减少系统所面临的风险,同时还具有为用户提供更新系统属性的服务,因此动态软件体系结构的开发与研究已成为软件工程研究的热点。
近年来,动态软件体系结构研究的主要内容集中在建模和模型验证等两方面。动态软件体系结构建模是成功设计软件系统的基础；而动态软件体系结构模型验证是保证动态软件体系结构质量的关键因素。两者缺一不可。
动态软件体系结构建模和模型验证具有一定的特殊性,目前对此研究还很不完善,缺少统一的建模和验证方法。由此可知,针对动态软件体系结构建模和模型验证方法的研究具有重要意义,未来此领域将拥有更广阔的发展空间。
本文凝聚了作者多年来在软件系统开发领域中的研究成果,结合实践提出对动态软件体系结构建模和模型验证方法用以满足软件体系结构动态性的需求。并通过“电力企业生产工程管理系统”应用案例进行实践验证,取得良好效果。具体内容主要包含以下几点：
(1)基于软件体系结构的理论基础,阐述了如何选取适应当前系统环境的动态软件体系结构的建模方法及模型验证方法,并通过实践表明在动态软件体系结构研究领域中,正确选取建模方法和模型验证方法的重要意义。
(2)本文提出了一种需求目标驱动的动态软件体系结构建模方法。该方法在Le Metayer的体系结构建模的理论和原则指导下,基于概念属性的需求目标模型和图元符号描述体系的SAAM方法而提出的一种需求目标驱动的动态软件体系结构的建模方法。
(3)本文基于谓词μ演算和空间逻辑,提出了一种基于谓词μ演算的空间逻辑的动态软件体系结构属性表示逻辑方法。该方法在谓词μ演算的基础上,增加了空间算子.的表示逻辑,统一地对结构和行为属性进行逻辑表示,解决了属性逻辑分别表示的问题。而在属性逻辑表示的过程中,本文提出了属性目标的部分满意度模型,并基于此模型评估属性满意度,从而解决属性目标常常是部分满足的问题。
(4)本文在动态软件体系结构模型验证中,分别提出了需求目标驱动的基于等价理论的缩减状态空间方法和基于LMC的动态软件体系结构模型验证算法。利用等价理论验证体系结构操作前后的等价关系,对动态体系结构模型提出一种新的缩减状态空间方法,从而实现了对初始体系结构的验证并简化了状态空间的搜索,一定程度缓解状态空间爆炸问题；初始体系结构的状态空间可作为模型验证算法的输入,而模型验证算法是模型验证的核心。另外本文基于LMC算法,还提出一种扩展LMC的动态软件体系结构模型验证算法,扩展了对空间算子的验证,解决了结构和行为属性同时验证的问题。
(5)根据本文所提出的动态软件体系结构建模和模型验证方法,对“电力企业生产工程管理系统”案例进行了应用研究。
The environment which located by the software system is changing according to the technique development, so the traditional static software architecture does not satisfy the present user's demands.In the contrast, the dynamic software architecture can not only strengthen the user's definition and extensibility but also lower the development fee and decrease the system's risk, meanwhile it can provide the service to update the system's property to users.In this way the development and study of dynamic software architecture is becoming hotspot of software engineering.
In the recent years,the primary coverage of dynamic software architecture studying concentrates on Modeling and Model Checking. The modeling of dynamic software architecture is the basis of successful software design, and the Model Checking of dynamic software architecture is the key factor to guarantee the quality of dynamic software architecture.Both of them are indispensable.
At present days the studying of Modeling and Model Checking of dynamic software architecture is not consummate because of its particularity, and it lacks the uniform methods of Modeling and Checking.
This Dissertation concentrates the author's research findings in software development, based on practice it proposed the methods of Modeling and Model Checking of dynamic software architecture to satisfy the demands of software architecture dynamics.The real application of "The production and project management system of power enterprises" has achieved perfect effects.The concrete contents are as following:
1.Based on the theoretical basis of software architecture the dissertation elaborates how to choose the methods of Modeling and Model Checking of dynamic software architecture which will best suit the present system environment, meanwhile,importance of valid choosing Modeling and Model Checking has been proven through the practice.
2.This dissertation proposes a demand driven modeling method of dynamic software architecture.Under Le Metayer's theory of system architecture modeling and principles,this method proposes a demand driven modeling method of dynamic software architecture based on the concept property demand and goal modeling, the SAAM method of graphic primitive symbolic describing system.
3.This dissertation proposes a property expressing logic method of dynamic software architecture based on predicateμcalcus arid space logics.It adds the expression logics to space algorithm operators, and unifying logic expresses the structure and behavior property to solve the problem of separately expressing the property and logics.In the expression of property logics, it proposes property goal partial satisfying model to solve the partial satisfy problem of property goal.
4. In the Model Checking of dynamic software architecture, this dissertation separately proposes a demand goal driven decreasing state space method which is based on equivalent theory, and a Model Checking method of dynamic software architecture which is based on LMC.Using the equivalent theory to verify the equivalent relationship before and after the operation of system architecture, it proposes a new decreasing state space method upon dynamic system architecture, and it in some extent relieves the state space explosion problem. The state space of initial system architecture is the enter data of Model Checking algorithm, and the method of Model Checking is the core of Model Checking. Moreover, it still proposes an extended LMC Model Checking of dynamic software architecture, based on the LMC algorithm, it extendes the verifying of space operators and solved the problem of simultaneously verifying the structure and the behavior property.
5.According to the Modeling and Model Checking methods in this dissertation, it carried out the application study in the real case of "The production and project management system of power enterprises"
近年来,动态软件体系结构研究的主要内容集中在建模和模型验证等两方面。动态软件体系结构建模是成功设计软件系统的基础；而动态软件体系结构模型验证是保证动态软件体系结构质量的关键因素。两者缺一不可。
动态软件体系结构建模和模型验证具有一定的特殊性,目前对此研究还很不完善,缺少统一的建模和验证方法。由此可知,针对动态软件体系结构建模和模型验证方法的研究具有重要意义,未来此领域将拥有更广阔的发展空间。
本文凝聚了作者多年来在软件系统开发领域中的研究成果,结合实践提出对动态软件体系结构建模和模型验证方法用以满足软件体系结构动态性的需求。并通过“电力企业生产工程管理系统”应用案例进行实践验证,取得良好效果。具体内容主要包含以下几点：
(1)基于软件体系结构的理论基础,阐述了如何选取适应当前系统环境的动态软件体系结构的建模方法及模型验证方法,并通过实践表明在动态软件体系结构研究领域中,正确选取建模方法和模型验证方法的重要意义。
(2)本文提出了一种需求目标驱动的动态软件体系结构建模方法。该方法在Le Metayer的体系结构建模的理论和原则指导下,基于概念属性的需求目标模型和图元符号描述体系的SAAM方法而提出的一种需求目标驱动的动态软件体系结构的建模方法。
(3)本文基于谓词μ演算和空间逻辑,提出了一种基于谓词μ演算的空间逻辑的动态软件体系结构属性表示逻辑方法。该方法在谓词μ演算的基础上,增加了空间算子.的表示逻辑,统一地对结构和行为属性进行逻辑表示,解决了属性逻辑分别表示的问题。而在属性逻辑表示的过程中,本文提出了属性目标的部分满意度模型,并基于此模型评估属性满意度,从而解决属性目标常常是部分满足的问题。
(4)本文在动态软件体系结构模型验证中,分别提出了需求目标驱动的基于等价理论的缩减状态空间方法和基于LMC的动态软件体系结构模型验证算法。利用等价理论验证体系结构操作前后的等价关系,对动态体系结构模型提出一种新的缩减状态空间方法,从而实现了对初始体系结构的验证并简化了状态空间的搜索,一定程度缓解状态空间爆炸问题；初始体系结构的状态空间可作为模型验证算法的输入,而模型验证算法是模型验证的核心。另外本文基于LMC算法,还提出一种扩展LMC的动态软件体系结构模型验证算法,扩展了对空间算子的验证,解决了结构和行为属性同时验证的问题。
(5)根据本文所提出的动态软件体系结构建模和模型验证方法,对“电力企业生产工程管理系统”案例进行了应用研究。
The environment which located by the software system is changing according to the technique development, so the traditional static software architecture does not satisfy the present user's demands.In the contrast, the dynamic software architecture can not only strengthen the user's definition and extensibility but also lower the development fee and decrease the system's risk, meanwhile it can provide the service to update the system's property to users.In this way the development and study of dynamic software architecture is becoming hotspot of software engineering.
In the recent years,the primary coverage of dynamic software architecture studying concentrates on Modeling and Model Checking. The modeling of dynamic software architecture is the basis of successful software design, and the Model Checking of dynamic software architecture is the key factor to guarantee the quality of dynamic software architecture.Both of them are indispensable.
At present days the studying of Modeling and Model Checking of dynamic software architecture is not consummate because of its particularity, and it lacks the uniform methods of Modeling and Checking.
This Dissertation concentrates the author's research findings in software development, based on practice it proposed the methods of Modeling and Model Checking of dynamic software architecture to satisfy the demands of software architecture dynamics.The real application of "The production and project management system of power enterprises" has achieved perfect effects.The concrete contents are as following:
1.Based on the theoretical basis of software architecture the dissertation elaborates how to choose the methods of Modeling and Model Checking of dynamic software architecture which will best suit the present system environment, meanwhile,importance of valid choosing Modeling and Model Checking has been proven through the practice.
2.This dissertation proposes a demand driven modeling method of dynamic software architecture.Under Le Metayer's theory of system architecture modeling and principles,this method proposes a demand driven modeling method of dynamic software architecture based on the concept property demand and goal modeling, the SAAM method of graphic primitive symbolic describing system.
3.This dissertation proposes a property expressing logic method of dynamic software architecture based on predicateμcalcus arid space logics.It adds the expression logics to space algorithm operators, and unifying logic expresses the structure and behavior property to solve the problem of separately expressing the property and logics.In the expression of property logics, it proposes property goal partial satisfying model to solve the partial satisfy problem of property goal.
4. In the Model Checking of dynamic software architecture, this dissertation separately proposes a demand goal driven decreasing state space method which is based on equivalent theory, and a Model Checking method of dynamic software architecture which is based on LMC.Using the equivalent theory to verify the equivalent relationship before and after the operation of system architecture, it proposes a new decreasing state space method upon dynamic system architecture, and it in some extent relieves the state space explosion problem. The state space of initial system architecture is the enter data of Model Checking algorithm, and the method of Model Checking is the core of Model Checking. Moreover, it still proposes an extended LMC Model Checking of dynamic software architecture, based on the LMC algorithm, it extendes the verifying of space operators and solved the problem of simultaneously verifying the structure and the behavior property.
5.According to the Modeling and Model Checking methods in this dissertation, it carried out the application study in the real case of "The production and project management system of power enterprises"
引文
[1]Shaw M, Garlan D. Software architecture:perspectives on an emerging discipline. Prentice Hall,1996.
[2]Clark E, Grumberg 0, Peled D. Model checking. MIT Press,2000.
[3]Bradbury J S.Organizing definitions and formalisms for dynamic software architectures. Technical Report 2004-477,School of Computing, Queen's University,2004.
[4]孙昌爱,金茂忠,刘超.软件体系结构研究综述.软件学报,2002,13(7)：1228-1237
[5]张鹏程,李必信,周宇.模型校验软件体系结构研究与进展.计算机科学,2007,34(4)：7-12
[6]Tsai J J P, Sistla A P, et al.Incremental verificaiton of architecture specification language for real-time system. In:Proc.of 3th International Workshop on object-oriented real-time Dependable System,1997.215-222.
[7]Magee J,Krammer J,Giannakopoulou D. Behaviour analysis of software architecture.The first Working IFIP Conf.on Software Architecture(WICSA).Kluwer Academic Publishers,1999:355-50.
[8]Giannakopoulou D.Model checking for concurent software architectures. PhD Thesis,University of London,1999.
[9]Ciancarini P, Mascolo C. Model checking a software architecture.In:Proc.of OSATEA International Workshop on t he Role of Software Architecture in Analysis and Testing. Software Engineering Notes,1999,24(4).
[10]Barber K S, Graser T, Holt J. Providing early feedback in the development cycle through automated application of model checking to software architectures.In:Proc.of 16th IEEE International Conference on Automated Software Engineering,2001.341-345.
[11]Jerad C,Barkaoui K. On the use of rewriting logic for verification of distributed software architecture description based LfP.In:Proc.of 16th IEEE International Workshop on Rapid System Prototyping,2005.202-208.
[12]Bose P. Automated translation of UML models of architectures for verification and simulation using SPIN. In:Proc.of 14th IEEE International Conference on Automated Software Engineering,1999.102-109.
[13]Inverardi P,Muccini H.Pelliccione P Automated check of architectural models consistency using SPIN. In:Proc.of 16th IEEE International Conference on Automated Software Engineering,2001.346-349
[14]Muccini H. Software architecture for testing, coordination and views model checking:[PhD dissertation].Roma:Universit'a degli Studi di Roma La Sapienza Dottorato di Ricerca in Informatica,2002
[15]McMillan K L.Symbolic model checking:an approach to the state explosion problem. Technical report,Deparment of Computer Science,Carnegie-Mellon University,1992.11.
[16]Holzmann G,Peled D. An improvement in formal verification. In FORTE1994,197-211,1995.11.
[17]Parrow R J, Steffen B. The concurrency workbench:a semantic-based verification tool for the verification of concurrent systems. ACM Transitions on Programming Languages and Systems,5(1):36-72,1993.11.
[18]Mateescu R, Model checking for software architecture.In:Proc.of the 1st Europe Workshop on Software Architecture Springer Verlag,2004.219-224
[19]Garlan D. Software architecture:a roadmap. In Proceedings of the Conference of the future of Software Engineering, New York:ACM Press,2000:93-101.
[20]Garlan D. Research directions in software architecture. ACM Computing Surveys,1995,27(2):257-261.
[21]Garlan D, Shaw M. An introduction to software architecture.Advances in Software Engineering and Knowledge Engineering, Pittsburgh:World Scientific,1993.
[22]Allen R,Garlan D.A formal basis for architectural connection.ACM Transaction on Software Engineering Notes,1992,6(3):214-249.
[23]Perry D E.Wolf A L. Foundations for the study of software architecture. ACM SIGSOFT Software Engineer Notes,1992,17(4):40-50.
[24]Kruchten.The 4+1 View Model of Architecture.IEEE Software,1995,12(6):42-50.
[25]Dilip Soni,Robert L. Nord, Christine Hofmeister.Software architecture in industrial applications. In:Proceedings of the 17th International Conference on Software Engineering. New York:ACM Press,1995.196-207.
[26]Medvidovic N, Taylor R N. A classification and comparison framework for software architecture description languages.IEEE Transactions on Software Engineering, 2000,26(1):70-93.
[27]李长云.基于体系结构的软件动态演化研究：(博士学位论文).杭州：浙江大学,2005.
[28]Perry D E, Wolf A L.Foundation for the research of software architecture. SIGSOFT Software Engineering Notes,1992,17(2):40-52.
[29]Magee J,Kramer J,Dynamic structure in software architecture. The Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering,1996:3-13.
[30]Oquendo F, Warboys B, Morrison R, et al.ARCHWare:Architecting evolvable software.EWSA 2004,2004,LNCS 3047:257-271.
[31]马晓星,余萍,陶先平等.一种面向服务的动态协同架构及其支撑平台.计算机学报,2005,28(4)：467-477.
[32]李长云,邬惠峰,应晶等.软件体系结构驱动的运行环境.小型微型计算机系统.2005,26(8)：1358-1363.
[33]Le Metayer D. Software architecture styles as graph grammars.In:Proceedings of the 4th ACM SIGSOFT Symposium on Foundations of Software Engineering. New York:ACM Press,1996.15-23
[34]Hirsch D. Graph Transformation Models for Software Architecture Styles. PhD thesis,Universidad de Buenos Aires,2003
[35]Taentzer G, Goedicke M, Meyer T. Dynamic accommodation of change:Automated architecture configuration of distributed systems. In:Proceedings of the 14th IEEE International Conference on Automated Software Engineering. Washington:IEEE Computer Society,1999.287
[36]Wermelinger M, Fiadeiro J L.A graph transformation approach to software architecture reconfiguration.Science of Computer Programming,2002,Vol44(2):133-155
[37]Berry G,Boudol G. The chemical abstract machine. Theorical Computer Science,96:217-248,1992.
[38]Inverardi P, Wolf A. Formal specification an analysis of software architectures using the Chemical Abstract Machine Model.IEEE Transactions on Software Engineering,1995,21(4).
[39]Allen R.A Formal approach to software architecture.PhD thesis,Carnegie Mellon Univ.,CMU Technical Report CMU-CS-97-114,May 1997.
[40]ALLen R,Douence R,Garlan D. Specifying and analyzing dynamic software architectures.LNCS 1382,1998.21-37.
[41]Hoarse C A R. Communicating sequential process.Prentice Hall,1985.
[42]Magee J, Dulay N, Eisenbach S,et al.Specifying Distributed Software Architectures. Proceedings of the 5th European Software Engineering Conference,Sitges,Spain, September 1995.
[43]Milner R,Parrow J,Walker D.A calcus of mobile processes.Journal of Information and Compution,1992,100:1-77.
[44]Canal C,Pimentel E,Troya J M. Specification and refinement of dynamic software architecture.In Software Architecture,pages 107-126.Kluwer Academic Publishing, Februrary 1999.
[45]Victor B,Moller F. The Mobility Workbench-a tool for π-calcus.In Computer Aided Verification(CAV'94),Springer-Verlag,1994,818:428-440.
[46]Cuesta C E, Fuente P, Solorzano M B. Dynamic cooperation architecture through the use of reflection. Symposium on Applied Computing Proceedings of the 2001 ACM symposium on Applied computing,2001:34-140.
[47]Oquendo F.π-ADL:an Architecture Description Language based on the higher-order typed π-calculus for specifying dynamic and mobile software architectures.ACM Software Engineering Notes,2004,29(4):1-14.
[48]李长云,李赣生,何频捷.一种形式化的动态体系结构描述语言.软件学报,2006,17(6)：1349-1359.
[49]Endler M.A language for implementing generic dynamic reconfiguration of distributed programs. In Proceedings of 12th Brazilian Symposium on Computer Networks,175-187,1994.
[50]Aguirre N,Maibaum T.A logical basis to the specification of reconfigurable component-based systems.In Proceedings of the 17th IEEE International Conference on Automated Software Engineering(ASE2002),271-274, Sept.2002.
[51]Virginia C. ZCL:a formal framework for specifying dynamic software architecture.PHD thesis,Federal University of Pernambuco,1999.
[52]Taylor R N, Medvidovic N, Anderson K M, et al.A component-and message based architecture style for GUI software. IEEE Transaction on software Engineering,1996,22(6):390-406.
[53]Luckham D C, Kenney J J, Augustin L M, Vera J, Bryan D, Mann W. Specification and analysis of system architecture using RAPIDE. IEEE Transactions on Software Engineering,1995,21(4).
[54]王晓光,冯耀东,梅宏.ABC/ADL:一种基于XML的软件体系结构描述语言.计算机研究与发展,2004,41(9)：1522-1531.
[55]冯铁,张家晨,陈伟.基于框架和角色模型的软件体系结构规约.软件学报,2001,11(8)：1078-1086.
[56]张家晨,冯铁,陈伟,等.基于主动连接的软件体系结构及其描述方法.软件学报,2000,11(8)：1047-1052.
[57]马俊涛,傅韶勇,刘积仁.A-Adl:一种多智能体系统体系结构描述语言.软件学报,2000,11(10)：1382-1389.
[58]于振华,蔡远利,徐海平.动态软件体系结构建模研究[J].西安交通大学学报,2007,41(2)：167-171.
[59]张世琨,王立福,常欣,等.基于层次消息总线的软件体系结构描述语言.电子学报,2001(5)：581-584.
[60]Zheng Zhi,Yang De-li,Lin Zheng-kui.Overview and Prospect on Goal-oriented Approach in RE. In:Proceedings of the 6th World Congress on Intelligent Control and Automation(WCICA2006),2006,2:7059-7063.
[61]Dardenne A, Lamsweerde A V,Fickas S.Goal-directed Requirements Acquisition. Science of Computer Programming,1993,20(1-2):3-50.
[62]Mylopoulos J, Chung L, Nixon B. Representing and Using Nonfunctional Requirements:A Process-Oriented Approach. IEEE Transactions on Software Engineering,1998,18(6):483-497.
[63]Rolland C, Souveyet C, Achour C B. Guiding goal modeling using scenarios.IEEE Transaction on Software Engineering,1998,24(12):1055-1071.
[64]Kiczales G, Lamping J, Mendhekar A. Aspect-oriented programming. In LNCS 1241(Proc.of ECOOP'97),1997.220-242.
[65]Kiczales G, Lamping J, Mendhekar A. Aspect-oriented programming. In LNCS 1241(Proc.of ECOOP'97),1997.220-242.
[66]郑志,杨德礼,林正奎.质量功能目标驱动的大型复杂信息系统开发方法的研究.计算机应用研究,2006年,12：59-68.
[67]Kazman R, Bass L, Abowd G,et al.SAAM:a method for analyzing the properties of software architectures. In:Proceedings of the 16th International Conference on Software Engineering.IEEE Computer Society,1994.
[68]Pnueli A. The Temporal Logic of Programms,18th annual IEEE-CS Symp.On Foundations of Computer Science,pp.46-57,1977.
[69]Clark E M, Emerson E A. Design and synthesis of Synchronization Skeletons using Branching Time Temporal,Logics of Programs Workshop, IBM Yorktown Heights,New York,Springer 131(52-71),may 1981.
[70]Pnueli A. A temporal logic of concurrent programs. Theoretical Computer Science,13:45-60,1981.
[71]Emerson E A. Automatic verification of finite-state concurrent systems using temporal logic specification. ACM Transition on Programming Languages and Systems,8(2):244-263,April 1986.7.
[72]Kozen D.Results on the Propositional Mu-Calculus. Theoretical Computer Science,27:333-354,1983.
[73]Bakten J C M. Mathematical Theory of Program Correctness.Prentice-Hall,1-465,1980.
[74]Park D.Fixpoint Induction and proof of program semantics. In Machine Intelligence, eds. B.Meltzer and D.Michie,5:59:78, Edinburgh Univ. Press, Edinburgh,1970.
[75]Hennessy M,Milner R. On observing nondeterminism and concurrency.Porcs ICALP'80 LNCS85:295-309,1980.
[76]刘剑.传值进程与移动进程模型检测方法：博士学位论文.北京：中国科学院,2005.
[77]Caires L, Cardelli L. A spatial logic for concurrency(Part Ⅰ).10th Symposium on Theoretical Aspects of Computer Science,Springer-Verlag,2001,2215:1-30.
[78]Caires L, Cardelli L. A spatial logic for concurrency(Part Ⅱ).In CONCUR 2002,LNCS2421.Springer-Verlag,2002.
[79]Caires L, Gordon A D. Anytime,Anywhere.Modal Logics for Mobile Ambients.In 27th ACM Symp.on Principles of Programming Languages,2000,365-377.
[80]Caires L, Gordon A D.I ogical Properties of Name Restriction. In:Proc. of TCLA'01,LNCS2044,Springer,2001.
[81]Alloui I,Garavel H, Mateescu R, Oquendo F. The ArchWare Architecture Analysis Language: Syntax and Semantics.Deliverable D3.1b,ArchWare European RTD Project,IST-2001-32360, 2003.
[82]Han T T,Chen T L,Lu Jian.Structure Analysis for Dynamic Software Architecture based on Spatial Logic.Proceedings of the 29th Annual International Computer Software and Application Conference(COMPSAC'05),2005.
[83]E. Letier, Reasoning about Agents in Goal-Oriented Requirements Engineering. Ph. D. Thesis, University of Louvain, May 2001.
[84]何书元.概率论.北京大学出版社,2006.
[85]郑志,杨德礼,林正奎.基于目标部分满意度的需求设计方案评估.计算机工程,2008年,34(2)：57-59..
[86]Antti Valmari.The State Explosion Problem. Lecture Notes in Computer Science:Lectures on Petri Nets I:Basic Models,1998,Vol(1491):429-528.
[87]Burch J R, Clark E M, McMillan K L, et al.Symbolic model checking:1020 states and beyond[A].5th IEEE Symposium on Logic in Computer Sciecce(LICS90).Los Alamitos:IEEE Computer Society,1990.428-439.
[88]Brant R E. Graph-based algorithms for booleam function manipulation. IEEE Transaction on Computers,1986,35(8):677-691.
[89]Holzmann G J. Design and Validation of Computer Protocols. New Jersey:Prentice Hall,1991.
[90]Katz S,Peled.Verification of distributed programms using representative interleaving sequence.Distributed Computing,1992,6:107-120.
[91]Holzmann G J, Peled D. An improvement in formal verification.7th IFIP WG6.1 International Conference on Formal Description Techniques VII(FORTE'1994).London:Chapman and Hall,1995.197-211.
[92]Emerson E A,Sistla P. Symmetry and model checking.Lecture Notes in Computer Science 697-5th International Conference on Computer Aided Verficaiton(CAV93).Berlin:Spring-Verlag,1993.463-478.
[93]Sistla P A, Gyuris V,Allen E. SMC:a symmetry-based model checker for verification of satey and liveness properties. ACM Transactions on Software Engineering and Methodology,2000,9(2):133-166.
[94]Cousot P, Radhia Cousot. Systematic design of program analysis frameworks.6th Annual ACM Symposium on Principles of Programming Languages(POPL79).New York:ACM Press,1979.269-282.
[95]Clark E M,Grumberg O, Long D E.Model checking and abstraction. ACM Transaction on Programming Language and Systems,1994,16(5):1512-1542.
[96]Loiseaux C, Graf S,Sifakis J, et al.Propery preserving abstractions for the verificaiton of concurrent system.Joural of Formal methods in System Design,1995,6:1-35.
[97]Weiser Mark.Progarm slicing. IEEE Transaction on Software Engineering,1984,10(4):352-357.
[98]Cheng J. Slicing concurrent programs-a graph-theoretical approach.LNCS749-lst Internatioanl Workshop on Automated and Algorithmic Debugging(AADEBUG93).Berlin:Spring-Verlag,1993.223-240.
[99]Millett L I,Teitelbaum T. Issues in slicing PROMELA and its applications to model checking, protocol understanding, and simulation. Intematioanl Journal on Software Tools for Technology Transfer,2000,2(4):343-349.
[100]Stark E W. A proof techniques for rely/guarantee properties. LNCS206-5th Conference on Foundation of Software Techniques and Theoretical Computer Science(FSTTCS85).Berlin:Spring-Verlag,1985.369-391.
[101]Clark E M, Long D E,McMillan K L.Compositional model checking.4th IEEE Symposium on Logic in Computer Science(LICS89).Los Alamitos:IEEE Computer Society,1989,353-362.
[102]Stahl K, Baukus K,Lakhnech Y, et al. Divide, abstract, and model-check. LNCS1680-Theoretical and Practical Aspects of SPIN Model Checking(Spin 99a,99b).Berlin:Springer-Verlag,1999.57-76.
[103]Laroussinie F, Schnoebelen P. The State Explosion Problem from Trace to Bisimulation Equivalence. Lecture Notes In Computer Science,2000,1784:192-207.
[104]Emerson E A, Lei C L. Efficient model checking in fragments of the propositional mu-calculus. In Proc.1st IEEE LICS,267-278,1986.23.
[105]Clarke S E, Long D J, Browne A, et al.An improved algorithm for the evaluation of fixpoint expressions. In Proc.of CAV'94, LNCS818, Springer,1994.23.
[106]Stirling C, Walker D. Local model checking in the modal mu-calculus. Theoretical Computer Science,89:161-177,1991.
[107]Stirling C.Modal and Temporal Logics.Springer,2001.23,46.
[108]Winskel G.A note on model checking the modal mu-calculus. In ICALP,LNCS372,1989.
[109]Lin H. Symbolic transition graphs with assignment. In Proc.of CONCUR'96,LNCS1119,1996.3,27,98,50-65.
[110]郑志,杨德礼,杨红.agent系统软件体系结构形式化建模方法.计算机工程,2008年,34(10)：35-37.
[111]Zheng Zhi,Yang De-li.Goal-oriented Reasoning Techniques Study for Evaluating Alternatives in Requirment Engineering. In:The 6th Wuhan International Conference on E-Business(WICEB2007),2007,1-4:1711-1716.
[2]Clark E, Grumberg 0, Peled D. Model checking. MIT Press,2000.
[3]Bradbury J S.Organizing definitions and formalisms for dynamic software architectures. Technical Report 2004-477,School of Computing, Queen's University,2004.
[4]孙昌爱,金茂忠,刘超.软件体系结构研究综述.软件学报,2002,13(7)：1228-1237
[5]张鹏程,李必信,周宇.模型校验软件体系结构研究与进展.计算机科学,2007,34(4)：7-12
[6]Tsai J J P, Sistla A P, et al.Incremental verificaiton of architecture specification language for real-time system. In:Proc.of 3th International Workshop on object-oriented real-time Dependable System,1997.215-222.
[7]Magee J,Krammer J,Giannakopoulou D. Behaviour analysis of software architecture.The first Working IFIP Conf.on Software Architecture(WICSA).Kluwer Academic Publishers,1999:355-50.
[8]Giannakopoulou D.Model checking for concurent software architectures. PhD Thesis,University of London,1999.
[9]Ciancarini P, Mascolo C. Model checking a software architecture.In:Proc.of OSATEA International Workshop on t he Role of Software Architecture in Analysis and Testing. Software Engineering Notes,1999,24(4).
[10]Barber K S, Graser T, Holt J. Providing early feedback in the development cycle through automated application of model checking to software architectures.In:Proc.of 16th IEEE International Conference on Automated Software Engineering,2001.341-345.
[11]Jerad C,Barkaoui K. On the use of rewriting logic for verification of distributed software architecture description based LfP.In:Proc.of 16th IEEE International Workshop on Rapid System Prototyping,2005.202-208.
[12]Bose P. Automated translation of UML models of architectures for verification and simulation using SPIN. In:Proc.of 14th IEEE International Conference on Automated Software Engineering,1999.102-109.
[13]Inverardi P,Muccini H.Pelliccione P Automated check of architectural models consistency using SPIN. In:Proc.of 16th IEEE International Conference on Automated Software Engineering,2001.346-349
[14]Muccini H. Software architecture for testing, coordination and views model checking:[PhD dissertation].Roma:Universit'a degli Studi di Roma La Sapienza Dottorato di Ricerca in Informatica,2002
[15]McMillan K L.Symbolic model checking:an approach to the state explosion problem. Technical report,Deparment of Computer Science,Carnegie-Mellon University,1992.11.
[16]Holzmann G,Peled D. An improvement in formal verification. In FORTE1994,197-211,1995.11.
[17]Parrow R J, Steffen B. The concurrency workbench:a semantic-based verification tool for the verification of concurrent systems. ACM Transitions on Programming Languages and Systems,5(1):36-72,1993.11.
[18]Mateescu R, Model checking for software architecture.In:Proc.of the 1st Europe Workshop on Software Architecture Springer Verlag,2004.219-224
[19]Garlan D. Software architecture:a roadmap. In Proceedings of the Conference of the future of Software Engineering, New York:ACM Press,2000:93-101.
[20]Garlan D. Research directions in software architecture. ACM Computing Surveys,1995,27(2):257-261.
[21]Garlan D, Shaw M. An introduction to software architecture.Advances in Software Engineering and Knowledge Engineering, Pittsburgh:World Scientific,1993.
[22]Allen R,Garlan D.A formal basis for architectural connection.ACM Transaction on Software Engineering Notes,1992,6(3):214-249.
[23]Perry D E.Wolf A L. Foundations for the study of software architecture. ACM SIGSOFT Software Engineer Notes,1992,17(4):40-50.
[24]Kruchten.The 4+1 View Model of Architecture.IEEE Software,1995,12(6):42-50.
[25]Dilip Soni,Robert L. Nord, Christine Hofmeister.Software architecture in industrial applications. In:Proceedings of the 17th International Conference on Software Engineering. New York:ACM Press,1995.196-207.
[26]Medvidovic N, Taylor R N. A classification and comparison framework for software architecture description languages.IEEE Transactions on Software Engineering, 2000,26(1):70-93.
[27]李长云.基于体系结构的软件动态演化研究：(博士学位论文).杭州：浙江大学,2005.
[28]Perry D E, Wolf A L.Foundation for the research of software architecture. SIGSOFT Software Engineering Notes,1992,17(2):40-52.
[29]Magee J,Kramer J,Dynamic structure in software architecture. The Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering,1996:3-13.
[30]Oquendo F, Warboys B, Morrison R, et al.ARCHWare:Architecting evolvable software.EWSA 2004,2004,LNCS 3047:257-271.
[31]马晓星,余萍,陶先平等.一种面向服务的动态协同架构及其支撑平台.计算机学报,2005,28(4)：467-477.
[32]李长云,邬惠峰,应晶等.软件体系结构驱动的运行环境.小型微型计算机系统.2005,26(8)：1358-1363.
[33]Le Metayer D. Software architecture styles as graph grammars.In:Proceedings of the 4th ACM SIGSOFT Symposium on Foundations of Software Engineering. New York:ACM Press,1996.15-23
[34]Hirsch D. Graph Transformation Models for Software Architecture Styles. PhD thesis,Universidad de Buenos Aires,2003
[35]Taentzer G, Goedicke M, Meyer T. Dynamic accommodation of change:Automated architecture configuration of distributed systems. In:Proceedings of the 14th IEEE International Conference on Automated Software Engineering. Washington:IEEE Computer Society,1999.287
[36]Wermelinger M, Fiadeiro J L.A graph transformation approach to software architecture reconfiguration.Science of Computer Programming,2002,Vol44(2):133-155
[37]Berry G,Boudol G. The chemical abstract machine. Theorical Computer Science,96:217-248,1992.
[38]Inverardi P, Wolf A. Formal specification an analysis of software architectures using the Chemical Abstract Machine Model.IEEE Transactions on Software Engineering,1995,21(4).
[39]Allen R.A Formal approach to software architecture.PhD thesis,Carnegie Mellon Univ.,CMU Technical Report CMU-CS-97-114,May 1997.
[40]ALLen R,Douence R,Garlan D. Specifying and analyzing dynamic software architectures.LNCS 1382,1998.21-37.
[41]Hoarse C A R. Communicating sequential process.Prentice Hall,1985.
[42]Magee J, Dulay N, Eisenbach S,et al.Specifying Distributed Software Architectures. Proceedings of the 5th European Software Engineering Conference,Sitges,Spain, September 1995.
[43]Milner R,Parrow J,Walker D.A calcus of mobile processes.Journal of Information and Compution,1992,100:1-77.
[44]Canal C,Pimentel E,Troya J M. Specification and refinement of dynamic software architecture.In Software Architecture,pages 107-126.Kluwer Academic Publishing, Februrary 1999.
[45]Victor B,Moller F. The Mobility Workbench-a tool for π-calcus.In Computer Aided Verification(CAV'94),Springer-Verlag,1994,818:428-440.
[46]Cuesta C E, Fuente P, Solorzano M B. Dynamic cooperation architecture through the use of reflection. Symposium on Applied Computing Proceedings of the 2001 ACM symposium on Applied computing,2001:34-140.
[47]Oquendo F.π-ADL:an Architecture Description Language based on the higher-order typed π-calculus for specifying dynamic and mobile software architectures.ACM Software Engineering Notes,2004,29(4):1-14.
[48]李长云,李赣生,何频捷.一种形式化的动态体系结构描述语言.软件学报,2006,17(6)：1349-1359.
[49]Endler M.A language for implementing generic dynamic reconfiguration of distributed programs. In Proceedings of 12th Brazilian Symposium on Computer Networks,175-187,1994.
[50]Aguirre N,Maibaum T.A logical basis to the specification of reconfigurable component-based systems.In Proceedings of the 17th IEEE International Conference on Automated Software Engineering(ASE2002),271-274, Sept.2002.
[51]Virginia C. ZCL:a formal framework for specifying dynamic software architecture.PHD thesis,Federal University of Pernambuco,1999.
[52]Taylor R N, Medvidovic N, Anderson K M, et al.A component-and message based architecture style for GUI software. IEEE Transaction on software Engineering,1996,22(6):390-406.
[53]Luckham D C, Kenney J J, Augustin L M, Vera J, Bryan D, Mann W. Specification and analysis of system architecture using RAPIDE. IEEE Transactions on Software Engineering,1995,21(4).
[54]王晓光,冯耀东,梅宏.ABC/ADL:一种基于XML的软件体系结构描述语言.计算机研究与发展,2004,41(9)：1522-1531.
[55]冯铁,张家晨,陈伟.基于框架和角色模型的软件体系结构规约.软件学报,2001,11(8)：1078-1086.
[56]张家晨,冯铁,陈伟,等.基于主动连接的软件体系结构及其描述方法.软件学报,2000,11(8)：1047-1052.
[57]马俊涛,傅韶勇,刘积仁.A-Adl:一种多智能体系统体系结构描述语言.软件学报,2000,11(10)：1382-1389.
[58]于振华,蔡远利,徐海平.动态软件体系结构建模研究[J].西安交通大学学报,2007,41(2)：167-171.
[59]张世琨,王立福,常欣,等.基于层次消息总线的软件体系结构描述语言.电子学报,2001(5)：581-584.
[60]Zheng Zhi,Yang De-li,Lin Zheng-kui.Overview and Prospect on Goal-oriented Approach in RE. In:Proceedings of the 6th World Congress on Intelligent Control and Automation(WCICA2006),2006,2:7059-7063.
[61]Dardenne A, Lamsweerde A V,Fickas S.Goal-directed Requirements Acquisition. Science of Computer Programming,1993,20(1-2):3-50.
[62]Mylopoulos J, Chung L, Nixon B. Representing and Using Nonfunctional Requirements:A Process-Oriented Approach. IEEE Transactions on Software Engineering,1998,18(6):483-497.
[63]Rolland C, Souveyet C, Achour C B. Guiding goal modeling using scenarios.IEEE Transaction on Software Engineering,1998,24(12):1055-1071.
[64]Kiczales G, Lamping J, Mendhekar A. Aspect-oriented programming. In LNCS 1241(Proc.of ECOOP'97),1997.220-242.
[65]Kiczales G, Lamping J, Mendhekar A. Aspect-oriented programming. In LNCS 1241(Proc.of ECOOP'97),1997.220-242.
[66]郑志,杨德礼,林正奎.质量功能目标驱动的大型复杂信息系统开发方法的研究.计算机应用研究,2006年,12：59-68.
[67]Kazman R, Bass L, Abowd G,et al.SAAM:a method for analyzing the properties of software architectures. In:Proceedings of the 16th International Conference on Software Engineering.IEEE Computer Society,1994.
[68]Pnueli A. The Temporal Logic of Programms,18th annual IEEE-CS Symp.On Foundations of Computer Science,pp.46-57,1977.
[69]Clark E M, Emerson E A. Design and synthesis of Synchronization Skeletons using Branching Time Temporal,Logics of Programs Workshop, IBM Yorktown Heights,New York,Springer 131(52-71),may 1981.
[70]Pnueli A. A temporal logic of concurrent programs. Theoretical Computer Science,13:45-60,1981.
[71]Emerson E A. Automatic verification of finite-state concurrent systems using temporal logic specification. ACM Transition on Programming Languages and Systems,8(2):244-263,April 1986.7.
[72]Kozen D.Results on the Propositional Mu-Calculus. Theoretical Computer Science,27:333-354,1983.
[73]Bakten J C M. Mathematical Theory of Program Correctness.Prentice-Hall,1-465,1980.
[74]Park D.Fixpoint Induction and proof of program semantics. In Machine Intelligence, eds. B.Meltzer and D.Michie,5:59:78, Edinburgh Univ. Press, Edinburgh,1970.
[75]Hennessy M,Milner R. On observing nondeterminism and concurrency.Porcs ICALP'80 LNCS85:295-309,1980.
[76]刘剑.传值进程与移动进程模型检测方法：博士学位论文.北京：中国科学院,2005.
[77]Caires L, Cardelli L. A spatial logic for concurrency(Part Ⅰ).10th Symposium on Theoretical Aspects of Computer Science,Springer-Verlag,2001,2215:1-30.
[78]Caires L, Cardelli L. A spatial logic for concurrency(Part Ⅱ).In CONCUR 2002,LNCS2421.Springer-Verlag,2002.
[79]Caires L, Gordon A D. Anytime,Anywhere.Modal Logics for Mobile Ambients.In 27th ACM Symp.on Principles of Programming Languages,2000,365-377.
[80]Caires L, Gordon A D.I ogical Properties of Name Restriction. In:Proc. of TCLA'01,LNCS2044,Springer,2001.
[81]Alloui I,Garavel H, Mateescu R, Oquendo F. The ArchWare Architecture Analysis Language: Syntax and Semantics.Deliverable D3.1b,ArchWare European RTD Project,IST-2001-32360, 2003.
[82]Han T T,Chen T L,Lu Jian.Structure Analysis for Dynamic Software Architecture based on Spatial Logic.Proceedings of the 29th Annual International Computer Software and Application Conference(COMPSAC'05),2005.
[83]E. Letier, Reasoning about Agents in Goal-Oriented Requirements Engineering. Ph. D. Thesis, University of Louvain, May 2001.
[84]何书元.概率论.北京大学出版社,2006.
[85]郑志,杨德礼,林正奎.基于目标部分满意度的需求设计方案评估.计算机工程,2008年,34(2)：57-59..
[86]Antti Valmari.The State Explosion Problem. Lecture Notes in Computer Science:Lectures on Petri Nets I:Basic Models,1998,Vol(1491):429-528.
[87]Burch J R, Clark E M, McMillan K L, et al.Symbolic model checking:1020 states and beyond[A].5th IEEE Symposium on Logic in Computer Sciecce(LICS90).Los Alamitos:IEEE Computer Society,1990.428-439.
[88]Brant R E. Graph-based algorithms for booleam function manipulation. IEEE Transaction on Computers,1986,35(8):677-691.
[89]Holzmann G J. Design and Validation of Computer Protocols. New Jersey:Prentice Hall,1991.
[90]Katz S,Peled.Verification of distributed programms using representative interleaving sequence.Distributed Computing,1992,6:107-120.
[91]Holzmann G J, Peled D. An improvement in formal verification.7th IFIP WG6.1 International Conference on Formal Description Techniques VII(FORTE'1994).London:Chapman and Hall,1995.197-211.
[92]Emerson E A,Sistla P. Symmetry and model checking.Lecture Notes in Computer Science 697-5th International Conference on Computer Aided Verficaiton(CAV93).Berlin:Spring-Verlag,1993.463-478.
[93]Sistla P A, Gyuris V,Allen E. SMC:a symmetry-based model checker for verification of satey and liveness properties. ACM Transactions on Software Engineering and Methodology,2000,9(2):133-166.
[94]Cousot P, Radhia Cousot. Systematic design of program analysis frameworks.6th Annual ACM Symposium on Principles of Programming Languages(POPL79).New York:ACM Press,1979.269-282.
[95]Clark E M,Grumberg O, Long D E.Model checking and abstraction. ACM Transaction on Programming Language and Systems,1994,16(5):1512-1542.
[96]Loiseaux C, Graf S,Sifakis J, et al.Propery preserving abstractions for the verificaiton of concurrent system.Joural of Formal methods in System Design,1995,6:1-35.
[97]Weiser Mark.Progarm slicing. IEEE Transaction on Software Engineering,1984,10(4):352-357.
[98]Cheng J. Slicing concurrent programs-a graph-theoretical approach.LNCS749-lst Internatioanl Workshop on Automated and Algorithmic Debugging(AADEBUG93).Berlin:Spring-Verlag,1993.223-240.
[99]Millett L I,Teitelbaum T. Issues in slicing PROMELA and its applications to model checking, protocol understanding, and simulation. Intematioanl Journal on Software Tools for Technology Transfer,2000,2(4):343-349.
[100]Stark E W. A proof techniques for rely/guarantee properties. LNCS206-5th Conference on Foundation of Software Techniques and Theoretical Computer Science(FSTTCS85).Berlin:Spring-Verlag,1985.369-391.
[101]Clark E M, Long D E,McMillan K L.Compositional model checking.4th IEEE Symposium on Logic in Computer Science(LICS89).Los Alamitos:IEEE Computer Society,1989,353-362.
[102]Stahl K, Baukus K,Lakhnech Y, et al. Divide, abstract, and model-check. LNCS1680-Theoretical and Practical Aspects of SPIN Model Checking(Spin 99a,99b).Berlin:Springer-Verlag,1999.57-76.
[103]Laroussinie F, Schnoebelen P. The State Explosion Problem from Trace to Bisimulation Equivalence. Lecture Notes In Computer Science,2000,1784:192-207.
[104]Emerson E A, Lei C L. Efficient model checking in fragments of the propositional mu-calculus. In Proc.1st IEEE LICS,267-278,1986.23.
[105]Clarke S E, Long D J, Browne A, et al.An improved algorithm for the evaluation of fixpoint expressions. In Proc.of CAV'94, LNCS818, Springer,1994.23.
[106]Stirling C, Walker D. Local model checking in the modal mu-calculus. Theoretical Computer Science,89:161-177,1991.
[107]Stirling C.Modal and Temporal Logics.Springer,2001.23,46.
[108]Winskel G.A note on model checking the modal mu-calculus. In ICALP,LNCS372,1989.
[109]Lin H. Symbolic transition graphs with assignment. In Proc.of CONCUR'96,LNCS1119,1996.3,27,98,50-65.
[110]郑志,杨德礼,杨红.agent系统软件体系结构形式化建模方法.计算机工程,2008年,34(10)：35-37.
[111]Zheng Zhi,Yang De-li.Goal-oriented Reasoning Techniques Study for Evaluating Alternatives in Requirment Engineering. In:The 6th Wuhan International Conference on E-Business(WICEB2007),2007,1-4:1711-1716.