形式化方法在构件组装实时系统中的应用研究
|
摘要
基于构件的软件开发方法(Component-Based Software Development,简称CBSD)将外部开发的构件集成到具体应用环境中来构建面向特定应用的软件系统,不仅能提高生产效率,降低开发费用,还能显著提高软件的可靠性,已经成为当前软件领域的主流技术。在实时系统领域中,随着系统中软件规模和复杂度的迅速增加,整个系统的质量和可靠性极大地依赖于软件系统的实时行为。如何描述构件的动态行为,如何根据系统的功能、实时性和可信属性组装已有的构件以满足实时系统的应用需求,成为当前此领域的一个研究热点。形式化方法因其精确性和严格性,能较好的满足上述要求,CBSD与形式化开发方法的融合对于构造可信实时系统具有重要的理论价值和实际意义。
形式化验证、充分的测试和有效的度量是主要的软件可信保证技术。本文将形式化方法和相应的模型检测工具、方法,以及可信质量模型相关理论应用于构件组装实时系统的构件建模、组装行为相容性验证、测试用例产生及构件选择,旨在构造一个可信的构件组装实时系统。本文的研究成果及核心内容归纳为如下四个方面：
(1)提出一种基于时间自动机的实时构件模型RCM,并给出了RCM积的构造方法。采用形式化方法对实时构件的交互行为进行描述,对提高系统可靠性有重要意义。通过引入动作的定义对构件的交互行为建模,用时钟约束表示构件交互行为的时间约束信息,RCM可以利用时钟约束和复位的时钟集合限制实时构件交互行为；通过构件组合信息RCM可以体现体系结构的层次关系。RCM的优点是既提供对实时构件所特有的时间约束特征的语义描述机制,又提供对构件交互行为的形式化描述和体系结构信息描述。
(2)提出一种对实时系统构件行为相容性分析验证的方法。基于构件的实时系统行为的不相容一般是由于时间约束不一致引起的,用RCM描述基于构件的实时系统,构件行为相容性问题就等价于在系统的实时模型上互补动作是否可以在共有通道上同步的问题,构件行为相容性检验可以转化为可被模型检测方法分析的可达性,最后用UPPAAL的验证功能给出结果。一个简单的铁路道岔系统的组装实例展示了这个方法及其效果。该方法的显著特点是建模精确,另外UPPAAL用动态验证技术和符号技术减少验证问题的规模,从而使该方法可以用于相当规模的系统组装。
(3)提出了三个针对实时系统的测试用例覆盖标准,自动生成长度优化的测试用例并给出了实例分析。根据实时系统的特点,在满足组装行为相容性的前提下,针对实时系统的安全属性和时间属性这两个重要的可信属性定义了两个新的测试覆盖标准,针对重要组装行为定义了相容性覆盖标准,然后将这三个覆盖标准转化为模型检测工具UPPAAL中对性质进行描述的断言形式,最后利用UPPAAL工具的生成最短诊断路径的功能自动生成长度优化的测试用例。面向性质测试比非面向性质测试进行得更深入,因此,该方法产生的测试用例比传统的测试用例更高效、覆盖率更高。
(4)提出了一种利用软件体系结构信息和可信等级化度量来选择构件并估计系统可靠性的方法。首先,根据构件软件及基于构件软件开发的层次性特征,用层次自动机对构件及整个软件系统进行形式化描述,用构件关系矩阵描述构件模块之间交互的频度,计算构件模块重要度因子,然后,根据重要程度不同,用重要度因子分级函数和等级质量映射函数来指导选择不同可信特性的构件组装系统并以此为基础对构件组装软件进行可靠性分析。最后,结合一个实例展示了这种方法的具体使用。构件组装相容性验证方法从行为层面指导构件选择,该方法更进一步,从属性量的指标层面来指导构件选择。该方法的显著特点是模型简单易理解,有效降低了系统复杂度。另外,引入不同的可信属性做为质量参数,使得构件的选择更加有效,为组装可信系统奠定了基础。
With the growth of software scale and complexity, the quality and reliability of the whole real-time system greatly depend on the efficient software development technique. These are strong motivations to apply new software engineering technique—Component-Based Software Development(CBSD).
Component-Based Software Development represents a pattern of "reuse instead of reinvention". It shifts the emphasis on software development from scratches to reusing and assembling of ready-made components and has become mainstream in software technique domain due to its lower cost, shorter time and higher reliability. Nowadays, how to describe the dynamic behavior and how to composite ready-made components for application according to the system's function, real-time property and trustworthy attributes have become hot-topics in research domain, and formal method can satisfy the above demands well for its accuracy. Thus, a novel concept to combine CBSD and formal method for constructing trustworthy real-time system is introduce in this paper.
Formal verification, adequate test and effective measurement are main trustworthy guarantee technique. So, formal methods, their corresponding model checking techniques and the theories of quality model of trusted component is applied to component modeling, verification of behavioral compatibility, test generation and component selection in thie thesis, aiming to construct a trustworthy component-based real-time system. The main contributions of this thesis are as follows:
(1) This thesis gives a formal model of real-time component based on timed automata(TA) named RCM, and also how to construct the product of the RCM is introduced. The behavior of components is modeled by introducing the definition of "Action" and the time property is shown by clock constraint in the RCM. So the model can limit the behavior of real-time components by clock constraint and the set of clock to be reset. RCM can also indicate the composition relation of components. The advantage of the RCM is that it provides description of real-time property, dynamic behavior between components and the architecture information.
(2) This thesis proposes a technique for behavioral compatibility analysis of component-based real-time system. The behavioral incompatibility of real-time system is often due to the inconsistency of clock constraints. So, how to describe and verify such behavioral incompatibility in an effective way should be taken more into consideration in real-time system component composition. First, the RCM based on timed automata is used to formally describe the component. In this way, the problem of component behavioral compatibility is equivalent to whether the complementary actions can really synchronize over common channels on the system's models. Then, the formulation of the behavioral compatibility verification is enabled as reachability properties that can be checked by reachability analysis of the model, and the verification function of the UPPAAL tool is used to generate the result. Finally, the method is applied to the composition of the railway level crossing control system, the results demonstrate the effectiveness and performance of the proposal. The obvious advantage of this method is the model of the component is explicit and the method is useful in sizeable component-composition systems, because model checking is often hampered by various state explosion problems, and in UPPAAL these problems are dealt with by a combination of on-the-fly verification together with a new and coarser symbolic technique reducing the verification problem to that of solving simple linear constraint systems.
(3) This thesis introduces new coverage criteria and the method to automatically generate length optimal tests for real-time system. On the basis of behavioral compatibility, new coverage criteria concerning safety, time property and key behavioral compatibility for the abstract formal of real-time system are presented and enabled as reachability properties. The method makes use of the RCM to formally describe the real-time system and uses the length optimal reachability feature of UPPAAL to automatically generate length optimal test sequences for the new coverage criteria. Experiment demonstrates how the technique works and performs. In general, testing focusing on particular properties is effective, so tests generated in this method have higher coverage and efficiency than traditional ones.
(4) This thesis provides a method for component selection and system reliability calculation. First, according to the hierarchy character of component-based software development, it makes use of the Hierarchical Automata(HA) to describe the component modules and the whole service system. Based on the interaction frequency among component modules, the relation matrix is introduced to calculate the importance factors contributing to the whole system. Wherein, to meet the system design requirement, a many-to-one mapping function is used to rank the importance into difference levels, each level corresponds to different quality criteria, which in return is used to select the appropriate components. Then, it proposes an algorithm to calculate the resulting system reliability. Finally, it studies a case to demonstrate the selection of components and the estimation of resulting reliability. Behavioral compatibility analysis of component-based system instructs component selection from behavior level, further more, this method from quality metrics. The obvious advantage of this method is that the model is easy to understand. Meanwhile, different trustworthy attributes are used as quality parameters, making the component selection and composition of the trustworthy software more effective.
形式化验证、充分的测试和有效的度量是主要的软件可信保证技术。本文将形式化方法和相应的模型检测工具、方法,以及可信质量模型相关理论应用于构件组装实时系统的构件建模、组装行为相容性验证、测试用例产生及构件选择,旨在构造一个可信的构件组装实时系统。本文的研究成果及核心内容归纳为如下四个方面：
(1)提出一种基于时间自动机的实时构件模型RCM,并给出了RCM积的构造方法。采用形式化方法对实时构件的交互行为进行描述,对提高系统可靠性有重要意义。通过引入动作的定义对构件的交互行为建模,用时钟约束表示构件交互行为的时间约束信息,RCM可以利用时钟约束和复位的时钟集合限制实时构件交互行为；通过构件组合信息RCM可以体现体系结构的层次关系。RCM的优点是既提供对实时构件所特有的时间约束特征的语义描述机制,又提供对构件交互行为的形式化描述和体系结构信息描述。
(2)提出一种对实时系统构件行为相容性分析验证的方法。基于构件的实时系统行为的不相容一般是由于时间约束不一致引起的,用RCM描述基于构件的实时系统,构件行为相容性问题就等价于在系统的实时模型上互补动作是否可以在共有通道上同步的问题,构件行为相容性检验可以转化为可被模型检测方法分析的可达性,最后用UPPAAL的验证功能给出结果。一个简单的铁路道岔系统的组装实例展示了这个方法及其效果。该方法的显著特点是建模精确,另外UPPAAL用动态验证技术和符号技术减少验证问题的规模,从而使该方法可以用于相当规模的系统组装。
(3)提出了三个针对实时系统的测试用例覆盖标准,自动生成长度优化的测试用例并给出了实例分析。根据实时系统的特点,在满足组装行为相容性的前提下,针对实时系统的安全属性和时间属性这两个重要的可信属性定义了两个新的测试覆盖标准,针对重要组装行为定义了相容性覆盖标准,然后将这三个覆盖标准转化为模型检测工具UPPAAL中对性质进行描述的断言形式,最后利用UPPAAL工具的生成最短诊断路径的功能自动生成长度优化的测试用例。面向性质测试比非面向性质测试进行得更深入,因此,该方法产生的测试用例比传统的测试用例更高效、覆盖率更高。
(4)提出了一种利用软件体系结构信息和可信等级化度量来选择构件并估计系统可靠性的方法。首先,根据构件软件及基于构件软件开发的层次性特征,用层次自动机对构件及整个软件系统进行形式化描述,用构件关系矩阵描述构件模块之间交互的频度,计算构件模块重要度因子,然后,根据重要程度不同,用重要度因子分级函数和等级质量映射函数来指导选择不同可信特性的构件组装系统并以此为基础对构件组装软件进行可靠性分析。最后,结合一个实例展示了这种方法的具体使用。构件组装相容性验证方法从行为层面指导构件选择,该方法更进一步,从属性量的指标层面来指导构件选择。该方法的显著特点是模型简单易理解,有效降低了系统复杂度。另外,引入不同的可信属性做为质量参数,使得构件的选择更加有效,为组装可信系统奠定了基础。
With the growth of software scale and complexity, the quality and reliability of the whole real-time system greatly depend on the efficient software development technique. These are strong motivations to apply new software engineering technique—Component-Based Software Development(CBSD).
Component-Based Software Development represents a pattern of "reuse instead of reinvention". It shifts the emphasis on software development from scratches to reusing and assembling of ready-made components and has become mainstream in software technique domain due to its lower cost, shorter time and higher reliability. Nowadays, how to describe the dynamic behavior and how to composite ready-made components for application according to the system's function, real-time property and trustworthy attributes have become hot-topics in research domain, and formal method can satisfy the above demands well for its accuracy. Thus, a novel concept to combine CBSD and formal method for constructing trustworthy real-time system is introduce in this paper.
Formal verification, adequate test and effective measurement are main trustworthy guarantee technique. So, formal methods, their corresponding model checking techniques and the theories of quality model of trusted component is applied to component modeling, verification of behavioral compatibility, test generation and component selection in thie thesis, aiming to construct a trustworthy component-based real-time system. The main contributions of this thesis are as follows:
(1) This thesis gives a formal model of real-time component based on timed automata(TA) named RCM, and also how to construct the product of the RCM is introduced. The behavior of components is modeled by introducing the definition of "Action" and the time property is shown by clock constraint in the RCM. So the model can limit the behavior of real-time components by clock constraint and the set of clock to be reset. RCM can also indicate the composition relation of components. The advantage of the RCM is that it provides description of real-time property, dynamic behavior between components and the architecture information.
(2) This thesis proposes a technique for behavioral compatibility analysis of component-based real-time system. The behavioral incompatibility of real-time system is often due to the inconsistency of clock constraints. So, how to describe and verify such behavioral incompatibility in an effective way should be taken more into consideration in real-time system component composition. First, the RCM based on timed automata is used to formally describe the component. In this way, the problem of component behavioral compatibility is equivalent to whether the complementary actions can really synchronize over common channels on the system's models. Then, the formulation of the behavioral compatibility verification is enabled as reachability properties that can be checked by reachability analysis of the model, and the verification function of the UPPAAL tool is used to generate the result. Finally, the method is applied to the composition of the railway level crossing control system, the results demonstrate the effectiveness and performance of the proposal. The obvious advantage of this method is the model of the component is explicit and the method is useful in sizeable component-composition systems, because model checking is often hampered by various state explosion problems, and in UPPAAL these problems are dealt with by a combination of on-the-fly verification together with a new and coarser symbolic technique reducing the verification problem to that of solving simple linear constraint systems.
(3) This thesis introduces new coverage criteria and the method to automatically generate length optimal tests for real-time system. On the basis of behavioral compatibility, new coverage criteria concerning safety, time property and key behavioral compatibility for the abstract formal of real-time system are presented and enabled as reachability properties. The method makes use of the RCM to formally describe the real-time system and uses the length optimal reachability feature of UPPAAL to automatically generate length optimal test sequences for the new coverage criteria. Experiment demonstrates how the technique works and performs. In general, testing focusing on particular properties is effective, so tests generated in this method have higher coverage and efficiency than traditional ones.
(4) This thesis provides a method for component selection and system reliability calculation. First, according to the hierarchy character of component-based software development, it makes use of the Hierarchical Automata(HA) to describe the component modules and the whole service system. Based on the interaction frequency among component modules, the relation matrix is introduced to calculate the importance factors contributing to the whole system. Wherein, to meet the system design requirement, a many-to-one mapping function is used to rank the importance into difference levels, each level corresponds to different quality criteria, which in return is used to select the appropriate components. Then, it proposes an algorithm to calculate the resulting system reliability. Finally, it studies a case to demonstrate the selection of components and the estimation of resulting reliability. Behavioral compatibility analysis of component-based system instructs component selection from behavior level, further more, this method from quality metrics. The obvious advantage of this method is that the model is easy to understand. Meanwhile, different trustworthy attributes are used as quality parameters, making the component selection and composition of the trustworthy software more effective.
引文
[1]Clements P C. From subroutines to subsystems:component-based software development[C]. In:Brown AW,eds. Component-Based Software Engineering:Selected Papers from the Software Engineering Institute. Los Alamitos, CA:IEEE Computer Society Press,1996.3-6.
[2]Meyer B, Mingins C. Component-Based development:From buzz to spark[J]. IEEE Computer,1999,32(7):35-37.
[3]Z. Manna, A. Pnueli. Models for reactivity[J]. Acta Informatica,1993,30(7):609-678.
[4]Councill B, Flynt J S, Mehta A, et al.. Component-based software engineering and the issue of trust[C]. In:Proceedings of the 22nd international conference on Software engineering. USA:ACM Press,2000.661-664.
[5]Meyer B.The Significance of Components in Software Development[EB].2003.http://www. sdmagazine. com/documents/s= 207/sdm9911k/.
[6]Microsoft Corporation, Microsoft COM Technologies-DCOM.2000.
[7]Microsystems. Enterprise JavaBeans Technology[EB].2001. http://java.sun.com/products/ ejb/.
[8]Chung L, Cesar J.On Nonfunctional Requirements in Software Engineering [J]. Lecture Notes in Computer Science,2009.5600(2009):363-379.
[9]Cysneiros L M, Leite J C S P, Neto J M S. A Framework for Integrating Non-functional Requirements into Conceptual Models[J]. Requiremants Engineering,2001,6(2),97-115.
[10]Cysneiros L M, Leite J C S P. Nonfunctional Requirements:From Elicitation to Conceptual Models[J]. IEEE Transactions on Software Engineering,2004,30(5):328-350.
[11]Gross D, Yu E. From Non-Functional Requirements to Design Through Patterns[J]. Requirements Engineering,2001,6(1):18-36.
[12]Chao Pingyi, Chen Tsungte. Analysis of assembly through product configuration[J]. Computers in Industry,2001,44:189-203.
[13]Bondavalli A, Mura I, Chiaradonna S, et al. DEEM:a tool for the dependability modeling and evaluation of multiple phased systems[C]. In:Proceedings of the International Conference on Dependable Systems and Networks. USA,2000.231-236.
[14]Ries G, Kalbarczyk Z, Kraljevic T, et al. DEPEND:a simulation environment for system dependability modeling and evaluation[C]. In:Proceedings of IEEE International Conference on Computer Performance and Dependability Symposium.USA,1996.54.
[15]Andrea B, Diego L, Mario D C,et al.High-level Integrated Design Environment for Dependability (HIDE) [C].In:Fifth International Workshop on Object-Oriented Real-Time Dependables Systems.Monterey,California,1999,87.
[16]Walter M,Trinitis C, Karl W. OpenSESAME:an intuitive dependability modeling environ-ment supporting inter-component dependencies[C].In:Proceedings of 2001 Pacific Rim International Symposium on Dependable Computing.Seoul,South Korea,2001.76-83.
[17]Meyer B. The next Software Breakthrough[J]. IEEE Computer, July 1997,30(7):113-114.
[18]江建慧.可信性指标体系[EB].同济大学http://www. plinux. org/teach/jhj/dep/.
[19]Johan Bengtsson, Fredrik Larson, Wang Yi,et al. UPPAAL-a Tool for Automatic Verification of Real-time Systems[C]. In:Proceedings of the DIMACS/SYCON workshop on Verification and control of Hybrid systems Ⅲ. Springer-Verlag New York, October 1995.232-243.
[20]Steffen Helke, Florian Kammuller. Representing Hierarchical Automata in Interactive Theorem Provers [C].In:Richard J Boulton, eds. Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics. London:Springer-Verlag,2001, 233-248.
[21]杨涛,肖田元,张林鍹.基于层次自动机的应用软件行为建模[J].系统仿真学报,2005,17(4)：778-781.
[22]Mcllroy M D, et al. Mass produced software components [C]. In:Proceedings of the 1968 NATO Conference on Software Engineering. Petrocelli/Charter, New York,1969.138-155.
[23]Cox B J. Object oriented programming:an evolutionary approach [M]. Boston, MA, USA: Addison-Wesley Longman Publishing,1986.
[24]Group O. M. CORBA Components Model.1999.
[25]C.Szypersky.Component software beyond object-oriented programming[M]. New York: Addison-Wesley Publishing,1998.
[26]D. Souza and A. Wills. Objects, components and frameworks with UML-the catalysis approach[M]. Addison-Wesley Publishing,1997.
[27]杨芙清.构件技术引领软件开发新潮流[J].中国计算机用户,2005,2(6)：42-43.
[28]金仙力.实时服务构件的语义特征和行为组装形式化技术研究[D].[博士学位论文].北京：北京邮电大学,2007.
[29]Z.Gu, K. Shin. Synthesis of real-time implementations from component-based software models[C].In:Proceedings Of the 26th IEEE International Real-Time Systems Symposium. Miami,FL,2005.167-176.
[30]Algirdas A, Jean-Claude L, Brian R, et al. Basic concepts and taxonomy of dependable and secure computing[J]. IEEE Trans on Dependable and Secure Computing,2004,1(1):11-33.
[31]Michael R Lyu. Handbook of software reliability engineering [M]. IEEE Computer Society Press,1996.
[32]Musa J D, Okumoto K. Software reliability:measurement prediction, and application[M]. New York:McGraw-Hill,1987.
[33]Alcatel and FPX. MicoCCM. http://www.fpx. De/MicoCCM/.
[34]Consortium.O. OpenCCM. http://openccm.objectweb.org/index.html.
[35]国防科技大学StarCCM. httP://starccm.sourceforge.net/.
[36]杨芙清.软件复用及相关技术[J].计算机科学,1999,26(5)：1-4.
[37]Meyer B. The grand challenge of trusted components[C]. In:Proceedings of the 25th International Conferenc on Software Engineering.Portland. Oregon, May 2003.660-667.
[38]Lindqvist U, Olovsson T, Jonsson E. An analysis of a secure system based on trusted components[C]. In:Proceedings of the Eleventh Annual Conference on Computer Assurance, Systems Integrity, Software Safety and Process Security. USA, June 1996.213-223.
[39]Howden W E, Huang Yudong. Software trustability[C]. In:Proceedings of the 5th International Symposium on Softwar Reliability Engineering. Monterey, CA, USA, Nov, 1994.143-151.
[40]GB/T 16260.1-ISO/IEC 9126-1：2003《软件工程-产品质量》第一部分《质量模刑》
[41]GB/T 16260.2-ISO/IEC 9126-2:2003《软件工程-产品质量》第二部分《外部度量》
[42]GB/T 16260.3-ISO/IEC 9126-3:2003《软件工程-产品质量》第三部分《内部度量》
[43]GB/T 16260.4-ISO/IEC 9126-4:2004《软件工程-产品质量》第四部分《使用质量度量》.
[44]信息产业部软件构件标准工作组.软件构件质量模型,VO.9,2004.12.
[45]Nicola G. Understanding, building and using ontologies:A commentary to "using explicit ontologies in KBS development"[J]. International Journal of Human Computer Studies,1997, 46(2-3):293-310.
[46]Fluit C, Sabou M, Harmelen F. Ontology-based information visualization[C]. In:Proceedings of Visualising the Semantic Web (VSW 2002). Springer-Verlag,2002.546-554.
[47]REN Hong-Min, QIAN Le-Qiu Research on Component Composition and Its Formal Reasoning[J]. Journal of Software,2003,14 (6):1066-1074.
[48]张世琨,张文娟,常欣等.基于软件体系结构的可复用构件制作和组装[J].软件学报,2001,12(9)：1351-1359.
[49]W3C (the World Wide Web Consortium). W3C Working Group Note 11-2004.2, Web Services Architecture. www.w3.org/TR/2004/NOTE-ws-arch-20040211/,www.w3.org.2004. 2.
[50]Business Process Execution Language for Web Services Versionl.l. http://xml.coverpages.org/ BPELv11-May052003 Final. Pdf.
[51]Web Services Business Process Execution Language Version2.0 Committee Draft,2007. http://docs.oasis-open.org/wsbpel/2.0/wsbpel-specification-draft.pdf.
[52]李景霞,侯紫峰.Web服务组合综述[J].计算机应用研究,2005,12(1)：4-7.
[53]Business Process Modeling Language,1.0, June 2002. http://www.ebpml.org/bpml_1_0_june_02.html.
[54]W. M. P. vander, Aalst. Pattern Based Analysis of BPML and WSCI. http://xml. coverpages. Org/Aalst-BPML.Pdf.
[55]Milanovic Nikola, Malek Miroslaw. Current solutions for Webservice composition[J]. IEEE Internet Computing,2004,8 (6):51-59.
[56]Grigoris Antoniou.Frank van Harmelen. Web Ontology Language:OWL.
[57]W3C. OWL Web Ontology Language Overview. Recommendation,2004.
[58]J.M. Wing. A specifier's introduction to formal methods[J]. IEEE Computer,1990,23(9):8-26.
[59]Marc Frappier, Henri Habrias. Software Specification Methods:An overview using a case study[M]. London:Springer-Verlag,1999.
[60]Johann M. Schumann. Automated theorem proving in software engineering[M]. Berlin Heidelerg:Springer-Verlag,2001.
[61]Emil Sekerinski, Kaisa Sere. Program Development by Refinement:Case Studies Using the B Method[M]. London:Springer-Verlag,2001.
[62]Manfred Broy, Oscar Slotosch. Enriching the Software Development Process by Formal Methods[J]. Lecture Notes in Computer Science,1999,1641(1999):44-61.
[63]Nenad Medvidovic, Peyman Orcizy, Jason E. Robbins, et al. Using object-oriented typing to support architectural design in the C2 style[J]. ACM SIGSOFT Software Engineering Notes, 1996,21 (6):24-32.
[64]David Garlan, Robert Monroe, David Wile. Acme:an architecture description interchang language[C].In:J.Howard Johnson, eds.Proceedings of the 1997 conference of the Centre for Advanced Studies on Collaborative research (CASCON'97).IBM Press,1997.169-183.
[65]David Garlan, Robert Allen, John Ockerbloom. Exploiting style in architectural design environments[C]. In:Proceeding of the 2nd ACM SIGSOFT Symposium on Foundations of Software Engineering. ACM Press,1994.179-185.
[66]Jeff Magee, Jeff Kramer. Dynamic structure in software architectures[J]. In:ACM SIGSOFT Software Engineering Notes,Nov 1996,21(6):3-14.
[67]David C, Luckham, L M.Aufustin, et al. Specification and analysis of system architecture using Rapid[J]. IEEE Transactions on Software Engineering,1995,21(4):336-355.
[68]M. Shaw, R. Deline, D V.Klein, et al. Abstractions for software architecture and tools to support them[J]. IEEE Transactions on Software Engineering-Special Issue on software Aichitecture,1995,21(4):314-335.
[69]Robert Allen, David Garlan. A formal basis for architectural connection[J]. ACM Transactions on Software Engineering and Methodology,1997,6(3):213-249,.
[70]M. Moriconi, X. Qian, R.A. Riemenschneider. Correct architecture refinement[J]. IEEE Transactions on Software Engineering,1995,21(4):356-372.
[71]Robin Milner. Communicating and mobile systems:the Pi-calculus[M]. Cambridge University Press,1999.
[72]Robert J. Allen. A formal approach to software architecture. Technical Report TR#CMU-CS-97-144, Carnegie Mellon University,1997.
[73]C.A.R. Hoare. Communicating sequential Processes[J]. Communications of the ACM-Special 25th Anniversary Issue,1983,26(1):100-106.
[74]冯铁,张家晨,陈伟,金淳兆.基于框架和角色模型的软件体系结构规约[J].软件学报,2000,11(8)：1078-1086.
[75]骆华俊,唐稚松,郑建丹.可视化体系结构描述语言XYZ/ADL[J]软件学报,2000,11(8)：1024-1029.
[76]朱雪阳,唐稚松.基于时序逻辑的软件体系结构描述语言XYZ/ADL[J]软件学报,2003,14(4)：713-720.
[77]梅宏,陈锋,冯耀东,杨杰.ABC：基于体系结构、面向构件的软件开发方法[J].软件学报,2003,14(4)：721-732.
[78]王晓光,冯耀东,梅宏ABC/ADL：一种基于XML的软件体系结构描述语言[J].计算机研究与发展,2004,41(9)：1521-1531.
[79]M.J.C. Gordon, T.F. Melham. Introduction to HOL:A theorem proving environment for higher-order logic[M]. Cambridge University Press,1993.
[80]S. Owre, J.M. Rushby, N. Shankar, et al. PVS:an experience report[M]. In:D.Huter, W. Stephan, P. Traverso, and M.Ullman, eds. APPlied Formal Methods Trends 98. Springer-Verlag,1998:338-345..
[81]W.H. Zhang. Verification of XYZ/SE Programs[J]. Chinese Journal of Advanced Software Research, April 1995,2(4):364-373.
[82]E.M. Clarke, E.A. Emerson, and A. P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications:A Practical approach[C]. In:Proceedings of the 10th ACM SIGACT-SIGPLAN Symposium on principles of Programming Languages. Austin, TX,Jan.24-26 1983,117-126.
[83]林惠民,张文辉.模型检测：理论、方法与应用[J].电子学报,2002,30(12A)：1907-1912.
[84]董威,王戟,齐治昌.并发和实时系统的模型检验技术[J].计算机研究与发展,2001,38(6)：698-705.
[85]Cindy Eisner, Doron Peled. Comparing symbolic and explicit model checking of a software system[C]. In:Proceedings of the 9th international SPIN Workshop on Model Checking of Software. Springer-Verlag,2002.230-239.
[86]Madanlal Musuvathi, Dawson R.Engler. Model checking large network protocol implementations[C].In:Proceedings of the 1st conference on Symposium on Networked Systems Design and Implementation. USENIX Association,2004.155-168.
[87]C. Courcoubetis, M.Vardi, P. VolPer, et al. Memory-efficient algorithms for the verification of temporal Properties[J]. Formal Methods in System Design,1992,1(2/3):275-288.
[88]G.J. Holzmann. Design and validation of computer protocols[M]. Englewood CliffS, New Jersey:Prentice-Hall,1991.
[89]G. Holzmann, D. Peled. An improvement in formal verification[C]. In Proceedings of FORTE 1994 Conference. Bern, Switzerland,1994.197-211.
[90]Shmuel Katz and Doron Peled. Verification of distributed programs using representative interleaving sequences[J]. Distributed Computing,1992,6:107-120.
[91]E.Allen Emerson, A.Prasad Sistla. Symmetry and model checking[J]. Formal Methods in System Design,1996,9(1-2):105-131.
[92]A.P. Sistla, V. Gyuris, E. Allen. Smc:a symmetry-based model checker for verification of safety and liveness properties[J]. ACM Transactions on Software Engineering Methodology, 2000,9(2):133-166.
[93]Edmund M. Clarke, Orna Grumberg, David E. Long. Model checking and abstraction[J]. ACM Transactions on Programming Languages and Systems,1994,16(5):1512-1542.
[94]Karsten Stahl, Kail Baukus, Yassine Lakhnech, et al. Divide, abstract, and model-check[J]. THEORETICAL AND PRACTICAL ASPECTS OF SPIN MODEL CHECKING,1999, LNCS 1680:57-76.
[95]K.L. McMillan. Symbolic model checking:An approach to the state explosion problem. Technical Report CMU-CS-92-131, Carnegie Mellon University,1992
[96]G.J. Holzmann. The model checker SPIN[J]. IEEE Transactions on Software Engineering, 1997,23(5):279-295.
[97]G. Holzmann.The SPIN model checker:Primer and reference manual[M]. Addison Wesley, 2004.
[98]Patrice Godefroid. Verisoft:A tool for the automatic analysis of concurrent reactive software[C]. In:Proceedings of the 9th Conference on Computer Aided Verification (CAV), Haifa, June 1997, LNCS 1254:476-479.
[99]Patrice Godefroid. Software model checking:The verisoft approach[J]. Formal Methods in System Design,2005,26(2):77-101.
[100]Henzinger T A, Jhala R, Majumdar R, et al. Lazy Abstraction[C]. In:Proceedings of the 29th Annual Symposium on Principles of Programming Languages (POPL). ACM Press,2002. 58-70.
[101]BLAST. http://www-cad.eecs.berkeley.edu/～rupak/blast.
[102]Klaus Havelund, Thomas Pressburger. Model checking java programs using java pathfinder [J]. International Journal on Software Tools for Technology Transfer (STTT),2000, 2(4):366-381.
[103]C. Daws, A. Olivero, S. TriPakis, et al. The tool KRONOS. In Hybrid Systems,1996.
[104]S. Yovine. KRONOS:A verification tool for real-time systems[J]. Springer-International Journal of Software Tools for Technology Transfer,1997,1(2):123-133.
[105]R. Alur, T. A. Henzinger and P.Ho. Automatic symbolic verification of embedded systems[J]. IEEE Transactions on Software Engineering,1996,22:181-201.
[106]T. Henzinger, P. Ho, and H. Wong-Toi. HyTech:A model checker for hybrid systems[J]. Software Tools for Technology Transfer,1997,1:110-122.
[107]R. Alur, R. P. Kurshan. Timing analysis in COSPAN[J]. In Hybrid Systems Ⅲ:Control and verification.Springer-Verlag,1996. LNCS 1066:220-231.
[108]R. Hardin, Z. Harei, and R. P. Kurshan. COSPAN[J]. In:Proceedings of the Eighth International Conference on Computer Aided Verification. Springer-Verlag,1996. LNCS 1102:423-427.
[109]R. Alur, A. Itai, R. P. Kurshan, et al. Timing verification by successive approximation[J]. Information and Computation,1995,118(1):142-157.
[110]Szyperski C, Gruntz D, Murer S. Component-Software:Beyond Object-oriented Programming (Second Edition) [M]. New York:ACM Press, Addison-Wesley,2002:12-18.
[111]Alagar V, Mohammad M. A component model for trustworthy real-time reactive systems development[C]. Formal Aspects of Component Software (FACS'07). Sophia-Antipolis, France:ENTCS, Elsevier, Sep.2007:1-15.
[112]Moller A, Akerholm M, Fredriksson J, et al. Evaluation of component technologies with respect to industrial requirements [C]. In:Proceedings of the 30th EUROMICRO Conference (EUROMICRO'04). Los Alamitos, CA, USA:IEEE Computer Society,2004:56-63.
[113]Antonio Vallecillo, Juan Hemandez, and Jose M. Troya.New issues in object interoperability [C].In:Proceedings Of the ECOOP 2000 Workshop on Object Interoperability. France,2000, LNCS 1964:256-269.
[114]W. Aalst, K. Hee, R. Toom. Component-Based software architectures:A framework based on inheritance of behavior[J]. Science of Computer Programming,2002,42(2-3):129-171.
[115]Marco Bemardo, Paolo Ciancarini, Lorenzo Donatiello. Architecting families of software systems with process algebras[J]. ACM Transactions on Software Engineering and Methodology(TOSEM),2002,11(4):386-426.
[116]P. Inverardi, A.L. Wolf. Formal specification and analysis of software architectures using the chemical abstract machine model[J]. IEEE Transactions on Software Engineering,1995, 21(4):373-386.
[117]Alessandro Aldini, Marco Bernardo. On the usability of Process algebra:An architectural view[J]. Theoretical Computer Science,2005,335(2-3):281-329.
[118]Fei Xie, James C. Browne. Verified systems by composition from verified components [J]. ACM SIGSOFT Software Engineering Notes,2003,28(5):277-286.
[119]Jezek P, Kofron J, Plasil F. Model Checking of Component Behavior Specification:A Real Life Experience [J]. Electronic Notes in Theoretical Computer Science,2006,160:197-210.
[120]Kofron J. Checking Software Component Behavior Using Behavior Protocols and Spin [C]. In:Proceedings of the 2007 ACM Symposium on Applied Computing. New York:ACM Press,2007:1513-1517.
[121]潘颖,赵俊峰,谢冰.构件库技术的研究与发展[J].计算机科学,2003,30(5)：90-93.
[122]谢冰,杨芙清.青鸟工程及其Case工具[J].计算机工程,2000,26(11)：76-78.
[123]Reed G M, Roscoe A W. A timed model for communicating sequential processes [J]. Theoretical Computer Science,1988,58(13):249-261.
[124]Rajeev Alur,David L. Dill. A theory of timed automata [J]. Theoretical Computer Science, 1994,126(2):183-235.
[125]Henzinger T A, Manna Z, Pnueli A. Temporal proof methodologies for timed transition systems [J]. Information and Computation,1994,112(2):273-337.
[126]郭亮,唐稚松.基于XYZ/E描述和验证容错系统[J].软件学报,2002,13(5)：913-920.
[127]R. Alur. Timed Automata[J].In Proceedings of the 11th International Conference on ComPuter-Aided Verification. Trento, Italy. Springer-Verlag Berlin Heidelberg, LNCS 1633:8-22.
[128]G. Behrmann, K. G. Larsen, J. Pearson, et al. Efficient timed reachability analysis using clock difference diagrams[J]. Trento, Italy, Springer-Verlag, July 1999. Computer Aided Verification LNCS 1633,682.
[129]D. Dill.Timing assumptions and verification of finite-state concurrent systems[J]. CAV'89, Springer-Verlag,1989. Automatic Verification Methods for Finite State Systems LNCS, 407(1990):97-212.
[130]Wang Yi, Paul Pettersson, and Mats Daniels. Automatic Verification of Real-Time Communicating Systems by Constraint-Solving[C]. In Proceedings of the 7th International conference on Formal Description Techniques,Citeseer,1994.
[131]Kim G. Larsen, Paul Pettersson, and Wang Yi. Composition and Symbolic Model Checking of Real-time Systems[C]. In Proceedings of the 16th IEEE Real-time Systems Symposiun. Pisa,ITALY,1995:76-87.
[132]贾仰理,张振领,李舟军.构件行为协议实时性扩展及相容性验证[J].计算机科学,2010,37(10)：143-147.
[133]Ammann P.E, Black P.E, Majurski W. Using model checking to generate tests from specifications [C]. In Proceedings of the 2nd IEEE International Conference on Formal Engineering Methods. Brisbane, Queensland, Australia,1998:46-54.
[134]Gargantini A, H eitmeyer C. Using model checking to generate tests from requirements specifications [C]. In Proceedings of the 7th European Engineering Conference Held Jointly with the 7th ACM'SIGSOFT International Symposium on Foundations of Software Engineering. Toulouse, FR,1999:146-162.
[135]梁陈良,聂长海,徐宝文等.一种基于模型检验的类测试用例生成方法[J].东南大学学报,2007,37(5)：776-781.
[136]Hyoung Seok Hong, Insup Lee,Oleg Sokolsky, et al. A temporal logic based theory of test coverage and generation [C].In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Grenoble, FR,2002:327-341.
[137]H. S. Hong, S. D. Cha, I. Lee, et al. Data flow testing as model cheeking[C]. In: Proceedings of the 25th International Conference on Software Engineering. Washington, DC, USA:IEEE Computer Society,2003,232-242.
[138]Rachel Cardell-Oliver. Conformance Testing of Real-Time Systems with Timed Automata[J]. Formal Aspects of Computing,2000,12(5):350-371.
[139]Abdeslam En-Nouaary, Rachida Dssouli, Ferhat Khendek,et al. Timed Test Cases Generation Based on State Characterization Technique[C]. In:Proceedings of the 19th IEEE Real-Time Systems Symposium (RTSS'98). Madrid,Spain, December 2-4 1998:220-229.
[140]J. Springintveld, F. Vaandrager, and P. R. D'Argenio. Testing Timed Automata[J]. Theoretical Computer Science, March 2001,254(1-2):225-257.
[141]陈小峰.可信平台模块的形式化分析和测试[J].计算机学报,2009,32(4)：646-653.
[142]李书浩,王戟,齐治昌,董威.一种面向性质的实时系统测试方法[J].电子学报,2005,33 (5).
[143]马良荔.基于元数据的构件集成测试技术研究[D].[博士学位论文].武汉：华中科技大学,2006.
[144]Francesca Basanieri,Antonia Bertolino. The Cow_Suite approach to planning and deriving test suites in UML projects[C]. In:Proceedings of the International Conference on the Unified Modeling Language.Dresden, Germany, Septmber 2002,383-397.
[145]Robert M. Hierons. Testing from a Z specification[J]. Software Testing,Verification and Reliablity,1997,7(1):19-33.
[146]Jan Tretmans. Conformance Testing with Labeled Transition Systems:Implementation relations and test generation[J]. Computer Networks and ISDN Systems,1996,29(1):49-79.
[147]Michael A. Friedman, Jeffrey M. Voas. Software Assessment:reliability, safety, testability [M].New York:John Wiley&sons,1995:21-34.
[148]J.L. Dalley. The Art of Software Testing[C]. In:proceedings of the IEEE 1991 National Conference on Aerospace and Electronics.Dayton,OH,USA,1991,757-760.
[149]C. Ghezzi. D. Mandrioli, A. Morzenti. TRIO:A logic language for executable specifications of real-time systems[J]. Journal of Systems and Software,1990,12(2):107-123.
[150]V Braberman, M Felder, M Marre. Testing Timing Behavior of Real-Time Software[A]. Int'l Software Quality Week.1997.
[151]S Morasca, MPezze. Using High-Level Petri Nets for Testing Concurrent and Real-Time Systems[A]. Real-Time Systems:Theory and Applications.Elsevier Science Publishers, 1990.119-132.
[152]A En-Nouaary, R Dssouli, F Khendek. Timed Wp-Method:Testing RealTime Systems[J]. IEEE Trans on Software Engineering,2002,28(11):1023-1038.
[153]E Petitjean,H Fochal. A Realistic Architecture for Timed Testing[A]. In:Proceedings of the 5th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'99). Las Vegas,NEVADA,1999.109-118.
[154]T Higashino, A Nakata, K Taniguchi,et al.Generating Test Cases for a Timed I/O Automata Model[A]. In:Proceedings of the 12th International Workshop on Testing Communicating Systems (IWTCS'99)[C].1999.197-214.
[155]P Bellini, R Mattolini, P Nesi. Temporal Logics for Real-time System Specification [J]. ACM Computing Surveys,2000,32(1):12-43.
[156]Angelo Gargantini, Elvinia Riccobene, Salvatore Rinzivillo.Using Spin to Generate Tests from ASM Specifications[A].In:Proceedings of the 2003 International Conference on Abstract State Machines,2003,LNCS 2589:263-277.
[157]R.J.Adam, J.ChliPala,Thomas A.Henzinger,R.Majumdar.Generating tests from counter examples[A].In:Proceedings of the 26th International Conference on Software Engineering (ICSE'04).IEEE Computer Society,2004,326-335.
[158]Hyoung Seok Hong, Insup Lee, Oleg Sokolsky, et al. A Temporal Logic Based Theory of Test Coverage and Generation[A]. In J. P. Katoen and P. Stevens, editors, TACAS 2002, pages 327-341. Kluwer Academic Publishers, April 2002.
[159]J. Callahan, F. Schneider, and S. Easterbrook. Specification-based testing using model checking[A]. In:Proceedings of SPIN Workshop, Rutgers University, August 1996. Tech. Report NASA-IVV-96-022.
[160]A. Engels, L. M. G. Feijs, and S. Mauw. Test generation for intelligent networks using model checking[J]. In:E.Brinksma, eds. Proceedings of TACAS'97. Springer,1997, LNCS 1217:384-398.
[161]Hwan Wook Sohn; Kung D.C; Pei Hsia.CORBA components testing with perception-based state behavior[C]. In Proceedings of the Twenty-Third Annual International Conference on Computer Software and Applications(COMPSAC'99). Phoenix,AZ,USA;IEEE Computer Society Press,1999,116-121.
[162]Liu W, Dasiewicz P. Component interaction testing using model-checking[C].In Proceedings of Canadian Conference on Electrical and Computer Engineering. Toronto,Ont,Canada:IEEE Computer Society Press,2001.41-46(vol.l).
[163]Ye Wu, Dai Pan, Mei-Hwa Chen.Techniques for testing component-based software[C]. In Proceedings of the Seventh IEEE International Conference on Engineering of Complex Computer Systems(ICECCS'01). Skovde, Sweden:IEEE Computer Society Press,2001, 222-232.
[164]盛津芳.商业构件评估方法及关键技术研究[D].[博士学位论文].长沙：中南大学,2007.
[165]Brownsword L, Sledge C A,Oberndorf T. An activity framework for COTS-based systems [R]. Software Engineering Institute,Carnegie Mellon University,2000.
[166]石军霞.ERP软件供应商选择风险研究[D].[硕士学位论文].西安：西安理工大学,2007.
[167]王荣培.面向构件的供应商管理模型研究与实现[D].[硕士学位论文].南京：南京航空航天大学,2004.
[168]Brereton P.The software customer/supplier relationship[J].Communications of the ACM, 2004,47(2):77-81.
[169]Michael Geisterfer C J, Ghosh S.Software component specification:A study in perspective of component selection and reuse[C].In:Proceedings of the 5th International Conference on COTS-Based Software Systems (ICCBSS'06),2006, Orlando, USA:100-108.
[170]Kunda D, Brooks L.Identifying and classifying processes (traditional and soft factors) that support COTS component selection:a case study[J]. European Journal of Information Systems,2000,9(4):226-234.
[171]Fahmi S A, Ho-Jin C. A study on software component selection methods[C].In:Proceedings of the 11th International Conference on Advanced Communication Technology.Phoenix Park, 2009.288-292.
[172]Haghpanah N, et al.Approximation algorithms for software component selection problem [C].In:Proceedings of the 14th Asia-Pacific Software Engineering Conference.Aichi, 2007:159-166.
[173]刘克,单志广,王戟,何积丰,张兆田,秦玉文.“可信软件基础研究”重大研究计划综述[J].中国科学基金,2008,3：145-151.
[174]Laprie J C. Dependability-Its attributes, impairments and means[M]. In Randell B, Laprie J C, Kopetz H, and Littlewood B, eds. Predictably Dependable Computing Systems. Washington, Springer,1998.
[175]Laprie J C. Dependability of computer system:from concept to limits[A].In:Proceedings of the Sixth International Symposium on Software Reliability Engineering. Toulosue, France, 24-27 Oct 1995.2-11.
[176]陈火旺,王戟,董威.高可信软件工程技术[J].电子学报,2003,31(12A),1933-1938.
[177]詹涛,周兴社,符宁,杨刚.软件能力可信研究综述[J].小型微型计算机系统,2008,29(5)：785-792.
[178]Andesron T, Laprie J C, Kopetz H. Dependability:Basic concepts and terminology[M]. New York:Springer-Verlag,1992
[179]Luckham D,Vera J, Meldal S.Three concepts of system architecture. Technical Report, CSL-TR-95-674, Stanford University,1995.
[180]Zhang S K, Zhang W J, Chang X, et al. Building and assembling reusable components based on software architecture[J]. Journal of Software,2001,12(9):1351-1359 (in Chinese with English abstract).
[181]Neil A. Maiden, Cornelius Ncube. Acquiring COTS software selection requirements[J]. IEEE Software,1998,15(2):46-56.
[182]Ruhe G. Intelligent support for selection of COTS products[J]. Lecture Notes in Computer Scienee,2593(2003):34-45.
[183]Briand L C.COTS evaluation and selection[A].In:Proceedings of the International Conference on Software Maintenance,1998, Washington, DC, USA,222-223.
[184]Vantakavikran P, Prompoon N. Constructing a process model for decision analysis and resolution on COTS selection issue of capability maturity model integration [A]. In: Proceedings of the 6th IEEE/ACIS International Conference on Computer and Information Science. Melbourne,Qld,2007,182-187.
[185]Hsuan-Shih L, Pei-Di S, Wen-Li C. A fuzzy multiple criteria decision making model for software selection[A]. In:Proceedings of the IEEE International Conference on Fuzzy Systems.2004,1709-1713.
[186]Sung W J, Kim J H, Rhew S Y. A quality model for open source software selection[A]. In: Proceedings of the Sixth International Conference on Advanced Language Processing and Web Information Technology (ALPIT 2007). China,2007,515-519.
[187]Donzelli P, et al. Evaluating COTS component dependability in context[J]. IEEE Software, 2005,22(4):46-53.
[188]Ncube C, Maiden N A M. Guiding parallel requirements acquisition and COTS software selection[C]. In:Proceedings of IEEE International Symposium on Requirements Engineering. Limerick, Ireland,1999,133-140.
[189]牟立峰.基于构件的软件开发中的构件供应商任务指派及构件选择方法[D].[博士学位论文].沈阳：东北大学,2009.
[190]张晓梅,张为群.一种基于信任机制的网构软件的构件选择方法研究[J].计算机科学,2010,37(2)：161-164.
[191]Mohamed A, Ruhe G, Eberlein A. COTS selection:Past, Present, and future[C]. In: Proceedings of the 14th Annual IEEE International Conference and Workshops on the Engineering of Computer-Based Systems (ECBS'07).Tucson, Arizona,2007,103-114.
[192]Navarrete F, Botella P, Franch X. How agile COTS selection methods are (and can be)?[C]. In:Proceedings of the 31st EUROMICRO Conference on Software Engineering and Advanced Applications.2005,160-167.
[193]Kohl R J. Requirements engineering changes for COTS-intensive systems[J]. IEEE Software, 2005,22(4):63-64.
[194]Ayag Z, Ozdemir R G. An intelligent approach to ERP software selection through fuzzy ANP[J]. International Journal of Production Research,2007,45(10):2169-2194.
[195]Cechich A, Piattini M. Early detection of COTS component functional suitability[J], Information and SoftwareTechnology,2007,49(2):108-121.
[196]Leung K, Leung H K N. On the efficiency of domain-based COTS Product selection method[J]. Information and Software Technology,2002,44(12):703-715.
[197]Jyrki Kontio. A case study in applying a systematic method for COTS selection[C]. In: Proceedings of the 18th International Conference on Software Engineering (ICSE'96). Washing,DC,USA:IEEE Computer Society,1996,201-209.
[198]李军.软构件工程学习环境开发及应用[D].大连：大连理工大学,2001.
[199]W.M Watkins, H W Lin, K Mcclelland, et al. COTS software selection process[R]. Sandia National Laboratories,US,2006.
[200]Bin W, Jinfang S. Extending FCD process to support COTS selection[A]. In:Proceedings of the 2008 International Conference on Computer Science and Software Engineering.2008, 139-142.
[201]Wanyama T, Far B H. Towards providing decision support for COTS selection[A]. In: Proceedings of the Conference on Electrical and Computer Engineering. Canada,2005, 908-911.
[202]Navarrete F, Botella P, Franch X. Reconciling agility and discipline in COTS selection Processes[A].In:Proceedings of the Sixth International IEEE Conference on Commercial-off-the-Shelf (COTS)-Based Software Systems (ICCBSS'07).Banff,Alta,2007,103-113.
[203]李敏,胡金柱,费丽娟,王军.基于粗糙-模糊集理论的智能化构件选取[J].计算机工程,2004,30(18)：135-137.
[204]Andreou A S,Tziakouris M. A quality framework for developing and evaluating original software components[J]. Information and Software Technology.2007,49(2):122-141.
[205]Keil M, Tiwana A. Beyond cost:The drivers of COTS application value[J]. IEEE Software. 2005,22(3):64-69.
[206]Carvallo J P, Franch X, Quer C. Determining criteria for selecting software components: Lessons learned[J]. IEEE Software,2007,24(3):84-94.
[207]Inoue K, Yokomori R, Yamamoto T, et al.Ranking significance of software components based on use relations[J]. IEEE Transactions on Software Engineering.2005,31 (3):213-225.
[208]Laprie J C. Dependability evaluation of software systems in operation[J]. IEEE Trans on Software Engineering.1984,10(6):701-714.
[209]Gokhale S. An analytical approach to architecture-based software reliability prediction[C]. In.Proceedings of the Third International Computer Performance and Dependability Symposium. Durham, North Carolina,1998.13-22.
[210]Sherif M. Scenario-based reliability analysis of component-based software[C].In: Proceedings of the 10th International Symposium on Software Reliability, Boca Raton, Florida,1999.
[211]Wells L, Christensen S, Kristensen L M, et al. Simulation-based performance analysis of web servers[A]. In:Proceedings of the 9th International Workshop on Petri Nets and Performance Models [C]. Piscataway, USA:IEEE Computer Society,2001,59-68.
[212]毛晓光,邓勇进.基于构件软件的可靠性通用模型[J].软件学报,2004,15(1)：27-32.
[213]徐如志等.基于XML的软件构件查询匹配算法研究[J].软件学报,2003,14(07)：1195-1202.
[214]Mariani L, Pezze M. Dynamic detection of COTS component incompatibility[J]. IEEE Software.2007,24(5):76-85.
[215]Yang Y, Jesal B, Boehm B, et al. Value-based Processes for COTS-based applications[J]. IEEE Software.2005,22(4):54-62.
[216]Baegh J. Certifying software component attributes [J]. IEEE Software.2006,23(3):74-81.
[217]刘晓明等.基于模型的构件系统性能预测综述[J].系统仿真学报.2007,19(13)：2924-2931.
[218]Seker R, Tanik M A. An information-theoretical framework for modeling component-based systems[J]. IEEE Transactions on Systems Man and Cybernetics Part C-Applications and Reviews.2004,34(4):475-484.
[219]Parsons T, et al. Extracting Interactions in Component-Based Systems[J]. IEEE Transactions on Software Engineering.2008,34(6):783-799.
[220]Tom W, Behrouz H F. Repositories for Cots Selection[A].In:Proceedings of the Canada Conference on Electrical and Computer Engineering (CCECE'06). Ottawa,Ont,2006,2416-2419.
[221]Hlupic V, Mann A S. SimSelect:A system for simulation software selection[A]. In: Proceedings of the Simulation Conference. Arlington, VA.USA, Winter,1995,720-727.
[222]张晓梅,张为群.一种基于信任机制的网构软件的构件选择方法研究[J].计算机科学,37(2),2010,161-164.
[223]廖渊,唐磊,李明树.一种基于QoS的服务构件组合方法[J].计算机学报,28(4),2005,627-634.
[224]Cheung, R.C.A User-Oriented Software Reliability Model[J].IEEE Transactions on Software Engineering,1980,6(2):115-125.
[225]Jung-Hua Lo;Sy-Yen Kuo;Lyu M.R;Chin-Yu Huang.Optimal Resource Allocation and Reliability Analysis for Component-based Software Application[J]. In the Proceedings of the 26th Annual International Conference on Computer Software and Application,2002, 12(10):7-12.
[226]Sherif Yacoub. A Scenario-Based Reliability Analysis Approach for Component-Based Software[J]. IEEE Transctions on Reliability,2004,53(4):465-480.
[2]Meyer B, Mingins C. Component-Based development:From buzz to spark[J]. IEEE Computer,1999,32(7):35-37.
[3]Z. Manna, A. Pnueli. Models for reactivity[J]. Acta Informatica,1993,30(7):609-678.
[4]Councill B, Flynt J S, Mehta A, et al.. Component-based software engineering and the issue of trust[C]. In:Proceedings of the 22nd international conference on Software engineering. USA:ACM Press,2000.661-664.
[5]Meyer B.The Significance of Components in Software Development[EB].2003.http://www. sdmagazine. com/documents/s= 207/sdm9911k/.
[6]Microsoft Corporation, Microsoft COM Technologies-DCOM.2000.
[7]Microsystems. Enterprise JavaBeans Technology[EB].2001. http://java.sun.com/products/ ejb/.
[8]Chung L, Cesar J.On Nonfunctional Requirements in Software Engineering [J]. Lecture Notes in Computer Science,2009.5600(2009):363-379.
[9]Cysneiros L M, Leite J C S P, Neto J M S. A Framework for Integrating Non-functional Requirements into Conceptual Models[J]. Requiremants Engineering,2001,6(2),97-115.
[10]Cysneiros L M, Leite J C S P. Nonfunctional Requirements:From Elicitation to Conceptual Models[J]. IEEE Transactions on Software Engineering,2004,30(5):328-350.
[11]Gross D, Yu E. From Non-Functional Requirements to Design Through Patterns[J]. Requirements Engineering,2001,6(1):18-36.
[12]Chao Pingyi, Chen Tsungte. Analysis of assembly through product configuration[J]. Computers in Industry,2001,44:189-203.
[13]Bondavalli A, Mura I, Chiaradonna S, et al. DEEM:a tool for the dependability modeling and evaluation of multiple phased systems[C]. In:Proceedings of the International Conference on Dependable Systems and Networks. USA,2000.231-236.
[14]Ries G, Kalbarczyk Z, Kraljevic T, et al. DEPEND:a simulation environment for system dependability modeling and evaluation[C]. In:Proceedings of IEEE International Conference on Computer Performance and Dependability Symposium.USA,1996.54.
[15]Andrea B, Diego L, Mario D C,et al.High-level Integrated Design Environment for Dependability (HIDE) [C].In:Fifth International Workshop on Object-Oriented Real-Time Dependables Systems.Monterey,California,1999,87.
[16]Walter M,Trinitis C, Karl W. OpenSESAME:an intuitive dependability modeling environ-ment supporting inter-component dependencies[C].In:Proceedings of 2001 Pacific Rim International Symposium on Dependable Computing.Seoul,South Korea,2001.76-83.
[17]Meyer B. The next Software Breakthrough[J]. IEEE Computer, July 1997,30(7):113-114.
[18]江建慧.可信性指标体系[EB].同济大学http://www. plinux. org/teach/jhj/dep/.
[19]Johan Bengtsson, Fredrik Larson, Wang Yi,et al. UPPAAL-a Tool for Automatic Verification of Real-time Systems[C]. In:Proceedings of the DIMACS/SYCON workshop on Verification and control of Hybrid systems Ⅲ. Springer-Verlag New York, October 1995.232-243.
[20]Steffen Helke, Florian Kammuller. Representing Hierarchical Automata in Interactive Theorem Provers [C].In:Richard J Boulton, eds. Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics. London:Springer-Verlag,2001, 233-248.
[21]杨涛,肖田元,张林鍹.基于层次自动机的应用软件行为建模[J].系统仿真学报,2005,17(4)：778-781.
[22]Mcllroy M D, et al. Mass produced software components [C]. In:Proceedings of the 1968 NATO Conference on Software Engineering. Petrocelli/Charter, New York,1969.138-155.
[23]Cox B J. Object oriented programming:an evolutionary approach [M]. Boston, MA, USA: Addison-Wesley Longman Publishing,1986.
[24]Group O. M. CORBA Components Model.1999.
[25]C.Szypersky.Component software beyond object-oriented programming[M]. New York: Addison-Wesley Publishing,1998.
[26]D. Souza and A. Wills. Objects, components and frameworks with UML-the catalysis approach[M]. Addison-Wesley Publishing,1997.
[27]杨芙清.构件技术引领软件开发新潮流[J].中国计算机用户,2005,2(6)：42-43.
[28]金仙力.实时服务构件的语义特征和行为组装形式化技术研究[D].[博士学位论文].北京：北京邮电大学,2007.
[29]Z.Gu, K. Shin. Synthesis of real-time implementations from component-based software models[C].In:Proceedings Of the 26th IEEE International Real-Time Systems Symposium. Miami,FL,2005.167-176.
[30]Algirdas A, Jean-Claude L, Brian R, et al. Basic concepts and taxonomy of dependable and secure computing[J]. IEEE Trans on Dependable and Secure Computing,2004,1(1):11-33.
[31]Michael R Lyu. Handbook of software reliability engineering [M]. IEEE Computer Society Press,1996.
[32]Musa J D, Okumoto K. Software reliability:measurement prediction, and application[M]. New York:McGraw-Hill,1987.
[33]Alcatel and FPX. MicoCCM. http://www.fpx. De/MicoCCM/.
[34]Consortium.O. OpenCCM. http://openccm.objectweb.org/index.html.
[35]国防科技大学StarCCM. httP://starccm.sourceforge.net/.
[36]杨芙清.软件复用及相关技术[J].计算机科学,1999,26(5)：1-4.
[37]Meyer B. The grand challenge of trusted components[C]. In:Proceedings of the 25th International Conferenc on Software Engineering.Portland. Oregon, May 2003.660-667.
[38]Lindqvist U, Olovsson T, Jonsson E. An analysis of a secure system based on trusted components[C]. In:Proceedings of the Eleventh Annual Conference on Computer Assurance, Systems Integrity, Software Safety and Process Security. USA, June 1996.213-223.
[39]Howden W E, Huang Yudong. Software trustability[C]. In:Proceedings of the 5th International Symposium on Softwar Reliability Engineering. Monterey, CA, USA, Nov, 1994.143-151.
[40]GB/T 16260.1-ISO/IEC 9126-1：2003《软件工程-产品质量》第一部分《质量模刑》
[41]GB/T 16260.2-ISO/IEC 9126-2:2003《软件工程-产品质量》第二部分《外部度量》
[42]GB/T 16260.3-ISO/IEC 9126-3:2003《软件工程-产品质量》第三部分《内部度量》
[43]GB/T 16260.4-ISO/IEC 9126-4:2004《软件工程-产品质量》第四部分《使用质量度量》.
[44]信息产业部软件构件标准工作组.软件构件质量模型,VO.9,2004.12.
[45]Nicola G. Understanding, building and using ontologies:A commentary to "using explicit ontologies in KBS development"[J]. International Journal of Human Computer Studies,1997, 46(2-3):293-310.
[46]Fluit C, Sabou M, Harmelen F. Ontology-based information visualization[C]. In:Proceedings of Visualising the Semantic Web (VSW 2002). Springer-Verlag,2002.546-554.
[47]REN Hong-Min, QIAN Le-Qiu Research on Component Composition and Its Formal Reasoning[J]. Journal of Software,2003,14 (6):1066-1074.
[48]张世琨,张文娟,常欣等.基于软件体系结构的可复用构件制作和组装[J].软件学报,2001,12(9)：1351-1359.
[49]W3C (the World Wide Web Consortium). W3C Working Group Note 11-2004.2, Web Services Architecture. www.w3.org/TR/2004/NOTE-ws-arch-20040211/,www.w3.org.2004. 2.
[50]Business Process Execution Language for Web Services Versionl.l. http://xml.coverpages.org/ BPELv11-May052003 Final. Pdf.
[51]Web Services Business Process Execution Language Version2.0 Committee Draft,2007. http://docs.oasis-open.org/wsbpel/2.0/wsbpel-specification-draft.pdf.
[52]李景霞,侯紫峰.Web服务组合综述[J].计算机应用研究,2005,12(1)：4-7.
[53]Business Process Modeling Language,1.0, June 2002. http://www.ebpml.org/bpml_1_0_june_02.html.
[54]W. M. P. vander, Aalst. Pattern Based Analysis of BPML and WSCI. http://xml. coverpages. Org/Aalst-BPML.Pdf.
[55]Milanovic Nikola, Malek Miroslaw. Current solutions for Webservice composition[J]. IEEE Internet Computing,2004,8 (6):51-59.
[56]Grigoris Antoniou.Frank van Harmelen. Web Ontology Language:OWL.
[57]W3C. OWL Web Ontology Language Overview. Recommendation,2004.
[58]J.M. Wing. A specifier's introduction to formal methods[J]. IEEE Computer,1990,23(9):8-26.
[59]Marc Frappier, Henri Habrias. Software Specification Methods:An overview using a case study[M]. London:Springer-Verlag,1999.
[60]Johann M. Schumann. Automated theorem proving in software engineering[M]. Berlin Heidelerg:Springer-Verlag,2001.
[61]Emil Sekerinski, Kaisa Sere. Program Development by Refinement:Case Studies Using the B Method[M]. London:Springer-Verlag,2001.
[62]Manfred Broy, Oscar Slotosch. Enriching the Software Development Process by Formal Methods[J]. Lecture Notes in Computer Science,1999,1641(1999):44-61.
[63]Nenad Medvidovic, Peyman Orcizy, Jason E. Robbins, et al. Using object-oriented typing to support architectural design in the C2 style[J]. ACM SIGSOFT Software Engineering Notes, 1996,21 (6):24-32.
[64]David Garlan, Robert Monroe, David Wile. Acme:an architecture description interchang language[C].In:J.Howard Johnson, eds.Proceedings of the 1997 conference of the Centre for Advanced Studies on Collaborative research (CASCON'97).IBM Press,1997.169-183.
[65]David Garlan, Robert Allen, John Ockerbloom. Exploiting style in architectural design environments[C]. In:Proceeding of the 2nd ACM SIGSOFT Symposium on Foundations of Software Engineering. ACM Press,1994.179-185.
[66]Jeff Magee, Jeff Kramer. Dynamic structure in software architectures[J]. In:ACM SIGSOFT Software Engineering Notes,Nov 1996,21(6):3-14.
[67]David C, Luckham, L M.Aufustin, et al. Specification and analysis of system architecture using Rapid[J]. IEEE Transactions on Software Engineering,1995,21(4):336-355.
[68]M. Shaw, R. Deline, D V.Klein, et al. Abstractions for software architecture and tools to support them[J]. IEEE Transactions on Software Engineering-Special Issue on software Aichitecture,1995,21(4):314-335.
[69]Robert Allen, David Garlan. A formal basis for architectural connection[J]. ACM Transactions on Software Engineering and Methodology,1997,6(3):213-249,.
[70]M. Moriconi, X. Qian, R.A. Riemenschneider. Correct architecture refinement[J]. IEEE Transactions on Software Engineering,1995,21(4):356-372.
[71]Robin Milner. Communicating and mobile systems:the Pi-calculus[M]. Cambridge University Press,1999.
[72]Robert J. Allen. A formal approach to software architecture. Technical Report TR#CMU-CS-97-144, Carnegie Mellon University,1997.
[73]C.A.R. Hoare. Communicating sequential Processes[J]. Communications of the ACM-Special 25th Anniversary Issue,1983,26(1):100-106.
[74]冯铁,张家晨,陈伟,金淳兆.基于框架和角色模型的软件体系结构规约[J].软件学报,2000,11(8)：1078-1086.
[75]骆华俊,唐稚松,郑建丹.可视化体系结构描述语言XYZ/ADL[J]软件学报,2000,11(8)：1024-1029.
[76]朱雪阳,唐稚松.基于时序逻辑的软件体系结构描述语言XYZ/ADL[J]软件学报,2003,14(4)：713-720.
[77]梅宏,陈锋,冯耀东,杨杰.ABC：基于体系结构、面向构件的软件开发方法[J].软件学报,2003,14(4)：721-732.
[78]王晓光,冯耀东,梅宏ABC/ADL：一种基于XML的软件体系结构描述语言[J].计算机研究与发展,2004,41(9)：1521-1531.
[79]M.J.C. Gordon, T.F. Melham. Introduction to HOL:A theorem proving environment for higher-order logic[M]. Cambridge University Press,1993.
[80]S. Owre, J.M. Rushby, N. Shankar, et al. PVS:an experience report[M]. In:D.Huter, W. Stephan, P. Traverso, and M.Ullman, eds. APPlied Formal Methods Trends 98. Springer-Verlag,1998:338-345..
[81]W.H. Zhang. Verification of XYZ/SE Programs[J]. Chinese Journal of Advanced Software Research, April 1995,2(4):364-373.
[82]E.M. Clarke, E.A. Emerson, and A. P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications:A Practical approach[C]. In:Proceedings of the 10th ACM SIGACT-SIGPLAN Symposium on principles of Programming Languages. Austin, TX,Jan.24-26 1983,117-126.
[83]林惠民,张文辉.模型检测：理论、方法与应用[J].电子学报,2002,30(12A)：1907-1912.
[84]董威,王戟,齐治昌.并发和实时系统的模型检验技术[J].计算机研究与发展,2001,38(6)：698-705.
[85]Cindy Eisner, Doron Peled. Comparing symbolic and explicit model checking of a software system[C]. In:Proceedings of the 9th international SPIN Workshop on Model Checking of Software. Springer-Verlag,2002.230-239.
[86]Madanlal Musuvathi, Dawson R.Engler. Model checking large network protocol implementations[C].In:Proceedings of the 1st conference on Symposium on Networked Systems Design and Implementation. USENIX Association,2004.155-168.
[87]C. Courcoubetis, M.Vardi, P. VolPer, et al. Memory-efficient algorithms for the verification of temporal Properties[J]. Formal Methods in System Design,1992,1(2/3):275-288.
[88]G.J. Holzmann. Design and validation of computer protocols[M]. Englewood CliffS, New Jersey:Prentice-Hall,1991.
[89]G. Holzmann, D. Peled. An improvement in formal verification[C]. In Proceedings of FORTE 1994 Conference. Bern, Switzerland,1994.197-211.
[90]Shmuel Katz and Doron Peled. Verification of distributed programs using representative interleaving sequences[J]. Distributed Computing,1992,6:107-120.
[91]E.Allen Emerson, A.Prasad Sistla. Symmetry and model checking[J]. Formal Methods in System Design,1996,9(1-2):105-131.
[92]A.P. Sistla, V. Gyuris, E. Allen. Smc:a symmetry-based model checker for verification of safety and liveness properties[J]. ACM Transactions on Software Engineering Methodology, 2000,9(2):133-166.
[93]Edmund M. Clarke, Orna Grumberg, David E. Long. Model checking and abstraction[J]. ACM Transactions on Programming Languages and Systems,1994,16(5):1512-1542.
[94]Karsten Stahl, Kail Baukus, Yassine Lakhnech, et al. Divide, abstract, and model-check[J]. THEORETICAL AND PRACTICAL ASPECTS OF SPIN MODEL CHECKING,1999, LNCS 1680:57-76.
[95]K.L. McMillan. Symbolic model checking:An approach to the state explosion problem. Technical Report CMU-CS-92-131, Carnegie Mellon University,1992
[96]G.J. Holzmann. The model checker SPIN[J]. IEEE Transactions on Software Engineering, 1997,23(5):279-295.
[97]G. Holzmann.The SPIN model checker:Primer and reference manual[M]. Addison Wesley, 2004.
[98]Patrice Godefroid. Verisoft:A tool for the automatic analysis of concurrent reactive software[C]. In:Proceedings of the 9th Conference on Computer Aided Verification (CAV), Haifa, June 1997, LNCS 1254:476-479.
[99]Patrice Godefroid. Software model checking:The verisoft approach[J]. Formal Methods in System Design,2005,26(2):77-101.
[100]Henzinger T A, Jhala R, Majumdar R, et al. Lazy Abstraction[C]. In:Proceedings of the 29th Annual Symposium on Principles of Programming Languages (POPL). ACM Press,2002. 58-70.
[101]BLAST. http://www-cad.eecs.berkeley.edu/～rupak/blast.
[102]Klaus Havelund, Thomas Pressburger. Model checking java programs using java pathfinder [J]. International Journal on Software Tools for Technology Transfer (STTT),2000, 2(4):366-381.
[103]C. Daws, A. Olivero, S. TriPakis, et al. The tool KRONOS. In Hybrid Systems,1996.
[104]S. Yovine. KRONOS:A verification tool for real-time systems[J]. Springer-International Journal of Software Tools for Technology Transfer,1997,1(2):123-133.
[105]R. Alur, T. A. Henzinger and P.Ho. Automatic symbolic verification of embedded systems[J]. IEEE Transactions on Software Engineering,1996,22:181-201.
[106]T. Henzinger, P. Ho, and H. Wong-Toi. HyTech:A model checker for hybrid systems[J]. Software Tools for Technology Transfer,1997,1:110-122.
[107]R. Alur, R. P. Kurshan. Timing analysis in COSPAN[J]. In Hybrid Systems Ⅲ:Control and verification.Springer-Verlag,1996. LNCS 1066:220-231.
[108]R. Hardin, Z. Harei, and R. P. Kurshan. COSPAN[J]. In:Proceedings of the Eighth International Conference on Computer Aided Verification. Springer-Verlag,1996. LNCS 1102:423-427.
[109]R. Alur, A. Itai, R. P. Kurshan, et al. Timing verification by successive approximation[J]. Information and Computation,1995,118(1):142-157.
[110]Szyperski C, Gruntz D, Murer S. Component-Software:Beyond Object-oriented Programming (Second Edition) [M]. New York:ACM Press, Addison-Wesley,2002:12-18.
[111]Alagar V, Mohammad M. A component model for trustworthy real-time reactive systems development[C]. Formal Aspects of Component Software (FACS'07). Sophia-Antipolis, France:ENTCS, Elsevier, Sep.2007:1-15.
[112]Moller A, Akerholm M, Fredriksson J, et al. Evaluation of component technologies with respect to industrial requirements [C]. In:Proceedings of the 30th EUROMICRO Conference (EUROMICRO'04). Los Alamitos, CA, USA:IEEE Computer Society,2004:56-63.
[113]Antonio Vallecillo, Juan Hemandez, and Jose M. Troya.New issues in object interoperability [C].In:Proceedings Of the ECOOP 2000 Workshop on Object Interoperability. France,2000, LNCS 1964:256-269.
[114]W. Aalst, K. Hee, R. Toom. Component-Based software architectures:A framework based on inheritance of behavior[J]. Science of Computer Programming,2002,42(2-3):129-171.
[115]Marco Bemardo, Paolo Ciancarini, Lorenzo Donatiello. Architecting families of software systems with process algebras[J]. ACM Transactions on Software Engineering and Methodology(TOSEM),2002,11(4):386-426.
[116]P. Inverardi, A.L. Wolf. Formal specification and analysis of software architectures using the chemical abstract machine model[J]. IEEE Transactions on Software Engineering,1995, 21(4):373-386.
[117]Alessandro Aldini, Marco Bernardo. On the usability of Process algebra:An architectural view[J]. Theoretical Computer Science,2005,335(2-3):281-329.
[118]Fei Xie, James C. Browne. Verified systems by composition from verified components [J]. ACM SIGSOFT Software Engineering Notes,2003,28(5):277-286.
[119]Jezek P, Kofron J, Plasil F. Model Checking of Component Behavior Specification:A Real Life Experience [J]. Electronic Notes in Theoretical Computer Science,2006,160:197-210.
[120]Kofron J. Checking Software Component Behavior Using Behavior Protocols and Spin [C]. In:Proceedings of the 2007 ACM Symposium on Applied Computing. New York:ACM Press,2007:1513-1517.
[121]潘颖,赵俊峰,谢冰.构件库技术的研究与发展[J].计算机科学,2003,30(5)：90-93.
[122]谢冰,杨芙清.青鸟工程及其Case工具[J].计算机工程,2000,26(11)：76-78.
[123]Reed G M, Roscoe A W. A timed model for communicating sequential processes [J]. Theoretical Computer Science,1988,58(13):249-261.
[124]Rajeev Alur,David L. Dill. A theory of timed automata [J]. Theoretical Computer Science, 1994,126(2):183-235.
[125]Henzinger T A, Manna Z, Pnueli A. Temporal proof methodologies for timed transition systems [J]. Information and Computation,1994,112(2):273-337.
[126]郭亮,唐稚松.基于XYZ/E描述和验证容错系统[J].软件学报,2002,13(5)：913-920.
[127]R. Alur. Timed Automata[J].In Proceedings of the 11th International Conference on ComPuter-Aided Verification. Trento, Italy. Springer-Verlag Berlin Heidelberg, LNCS 1633:8-22.
[128]G. Behrmann, K. G. Larsen, J. Pearson, et al. Efficient timed reachability analysis using clock difference diagrams[J]. Trento, Italy, Springer-Verlag, July 1999. Computer Aided Verification LNCS 1633,682.
[129]D. Dill.Timing assumptions and verification of finite-state concurrent systems[J]. CAV'89, Springer-Verlag,1989. Automatic Verification Methods for Finite State Systems LNCS, 407(1990):97-212.
[130]Wang Yi, Paul Pettersson, and Mats Daniels. Automatic Verification of Real-Time Communicating Systems by Constraint-Solving[C]. In Proceedings of the 7th International conference on Formal Description Techniques,Citeseer,1994.
[131]Kim G. Larsen, Paul Pettersson, and Wang Yi. Composition and Symbolic Model Checking of Real-time Systems[C]. In Proceedings of the 16th IEEE Real-time Systems Symposiun. Pisa,ITALY,1995:76-87.
[132]贾仰理,张振领,李舟军.构件行为协议实时性扩展及相容性验证[J].计算机科学,2010,37(10)：143-147.
[133]Ammann P.E, Black P.E, Majurski W. Using model checking to generate tests from specifications [C]. In Proceedings of the 2nd IEEE International Conference on Formal Engineering Methods. Brisbane, Queensland, Australia,1998:46-54.
[134]Gargantini A, H eitmeyer C. Using model checking to generate tests from requirements specifications [C]. In Proceedings of the 7th European Engineering Conference Held Jointly with the 7th ACM'SIGSOFT International Symposium on Foundations of Software Engineering. Toulouse, FR,1999:146-162.
[135]梁陈良,聂长海,徐宝文等.一种基于模型检验的类测试用例生成方法[J].东南大学学报,2007,37(5)：776-781.
[136]Hyoung Seok Hong, Insup Lee,Oleg Sokolsky, et al. A temporal logic based theory of test coverage and generation [C].In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Grenoble, FR,2002:327-341.
[137]H. S. Hong, S. D. Cha, I. Lee, et al. Data flow testing as model cheeking[C]. In: Proceedings of the 25th International Conference on Software Engineering. Washington, DC, USA:IEEE Computer Society,2003,232-242.
[138]Rachel Cardell-Oliver. Conformance Testing of Real-Time Systems with Timed Automata[J]. Formal Aspects of Computing,2000,12(5):350-371.
[139]Abdeslam En-Nouaary, Rachida Dssouli, Ferhat Khendek,et al. Timed Test Cases Generation Based on State Characterization Technique[C]. In:Proceedings of the 19th IEEE Real-Time Systems Symposium (RTSS'98). Madrid,Spain, December 2-4 1998:220-229.
[140]J. Springintveld, F. Vaandrager, and P. R. D'Argenio. Testing Timed Automata[J]. Theoretical Computer Science, March 2001,254(1-2):225-257.
[141]陈小峰.可信平台模块的形式化分析和测试[J].计算机学报,2009,32(4)：646-653.
[142]李书浩,王戟,齐治昌,董威.一种面向性质的实时系统测试方法[J].电子学报,2005,33 (5).
[143]马良荔.基于元数据的构件集成测试技术研究[D].[博士学位论文].武汉：华中科技大学,2006.
[144]Francesca Basanieri,Antonia Bertolino. The Cow_Suite approach to planning and deriving test suites in UML projects[C]. In:Proceedings of the International Conference on the Unified Modeling Language.Dresden, Germany, Septmber 2002,383-397.
[145]Robert M. Hierons. Testing from a Z specification[J]. Software Testing,Verification and Reliablity,1997,7(1):19-33.
[146]Jan Tretmans. Conformance Testing with Labeled Transition Systems:Implementation relations and test generation[J]. Computer Networks and ISDN Systems,1996,29(1):49-79.
[147]Michael A. Friedman, Jeffrey M. Voas. Software Assessment:reliability, safety, testability [M].New York:John Wiley&sons,1995:21-34.
[148]J.L. Dalley. The Art of Software Testing[C]. In:proceedings of the IEEE 1991 National Conference on Aerospace and Electronics.Dayton,OH,USA,1991,757-760.
[149]C. Ghezzi. D. Mandrioli, A. Morzenti. TRIO:A logic language for executable specifications of real-time systems[J]. Journal of Systems and Software,1990,12(2):107-123.
[150]V Braberman, M Felder, M Marre. Testing Timing Behavior of Real-Time Software[A]. Int'l Software Quality Week.1997.
[151]S Morasca, MPezze. Using High-Level Petri Nets for Testing Concurrent and Real-Time Systems[A]. Real-Time Systems:Theory and Applications.Elsevier Science Publishers, 1990.119-132.
[152]A En-Nouaary, R Dssouli, F Khendek. Timed Wp-Method:Testing RealTime Systems[J]. IEEE Trans on Software Engineering,2002,28(11):1023-1038.
[153]E Petitjean,H Fochal. A Realistic Architecture for Timed Testing[A]. In:Proceedings of the 5th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'99). Las Vegas,NEVADA,1999.109-118.
[154]T Higashino, A Nakata, K Taniguchi,et al.Generating Test Cases for a Timed I/O Automata Model[A]. In:Proceedings of the 12th International Workshop on Testing Communicating Systems (IWTCS'99)[C].1999.197-214.
[155]P Bellini, R Mattolini, P Nesi. Temporal Logics for Real-time System Specification [J]. ACM Computing Surveys,2000,32(1):12-43.
[156]Angelo Gargantini, Elvinia Riccobene, Salvatore Rinzivillo.Using Spin to Generate Tests from ASM Specifications[A].In:Proceedings of the 2003 International Conference on Abstract State Machines,2003,LNCS 2589:263-277.
[157]R.J.Adam, J.ChliPala,Thomas A.Henzinger,R.Majumdar.Generating tests from counter examples[A].In:Proceedings of the 26th International Conference on Software Engineering (ICSE'04).IEEE Computer Society,2004,326-335.
[158]Hyoung Seok Hong, Insup Lee, Oleg Sokolsky, et al. A Temporal Logic Based Theory of Test Coverage and Generation[A]. In J. P. Katoen and P. Stevens, editors, TACAS 2002, pages 327-341. Kluwer Academic Publishers, April 2002.
[159]J. Callahan, F. Schneider, and S. Easterbrook. Specification-based testing using model checking[A]. In:Proceedings of SPIN Workshop, Rutgers University, August 1996. Tech. Report NASA-IVV-96-022.
[160]A. Engels, L. M. G. Feijs, and S. Mauw. Test generation for intelligent networks using model checking[J]. In:E.Brinksma, eds. Proceedings of TACAS'97. Springer,1997, LNCS 1217:384-398.
[161]Hwan Wook Sohn; Kung D.C; Pei Hsia.CORBA components testing with perception-based state behavior[C]. In Proceedings of the Twenty-Third Annual International Conference on Computer Software and Applications(COMPSAC'99). Phoenix,AZ,USA;IEEE Computer Society Press,1999,116-121.
[162]Liu W, Dasiewicz P. Component interaction testing using model-checking[C].In Proceedings of Canadian Conference on Electrical and Computer Engineering. Toronto,Ont,Canada:IEEE Computer Society Press,2001.41-46(vol.l).
[163]Ye Wu, Dai Pan, Mei-Hwa Chen.Techniques for testing component-based software[C]. In Proceedings of the Seventh IEEE International Conference on Engineering of Complex Computer Systems(ICECCS'01). Skovde, Sweden:IEEE Computer Society Press,2001, 222-232.
[164]盛津芳.商业构件评估方法及关键技术研究[D].[博士学位论文].长沙：中南大学,2007.
[165]Brownsword L, Sledge C A,Oberndorf T. An activity framework for COTS-based systems [R]. Software Engineering Institute,Carnegie Mellon University,2000.
[166]石军霞.ERP软件供应商选择风险研究[D].[硕士学位论文].西安：西安理工大学,2007.
[167]王荣培.面向构件的供应商管理模型研究与实现[D].[硕士学位论文].南京：南京航空航天大学,2004.
[168]Brereton P.The software customer/supplier relationship[J].Communications of the ACM, 2004,47(2):77-81.
[169]Michael Geisterfer C J, Ghosh S.Software component specification:A study in perspective of component selection and reuse[C].In:Proceedings of the 5th International Conference on COTS-Based Software Systems (ICCBSS'06),2006, Orlando, USA:100-108.
[170]Kunda D, Brooks L.Identifying and classifying processes (traditional and soft factors) that support COTS component selection:a case study[J]. European Journal of Information Systems,2000,9(4):226-234.
[171]Fahmi S A, Ho-Jin C. A study on software component selection methods[C].In:Proceedings of the 11th International Conference on Advanced Communication Technology.Phoenix Park, 2009.288-292.
[172]Haghpanah N, et al.Approximation algorithms for software component selection problem [C].In:Proceedings of the 14th Asia-Pacific Software Engineering Conference.Aichi, 2007:159-166.
[173]刘克,单志广,王戟,何积丰,张兆田,秦玉文.“可信软件基础研究”重大研究计划综述[J].中国科学基金,2008,3：145-151.
[174]Laprie J C. Dependability-Its attributes, impairments and means[M]. In Randell B, Laprie J C, Kopetz H, and Littlewood B, eds. Predictably Dependable Computing Systems. Washington, Springer,1998.
[175]Laprie J C. Dependability of computer system:from concept to limits[A].In:Proceedings of the Sixth International Symposium on Software Reliability Engineering. Toulosue, France, 24-27 Oct 1995.2-11.
[176]陈火旺,王戟,董威.高可信软件工程技术[J].电子学报,2003,31(12A),1933-1938.
[177]詹涛,周兴社,符宁,杨刚.软件能力可信研究综述[J].小型微型计算机系统,2008,29(5)：785-792.
[178]Andesron T, Laprie J C, Kopetz H. Dependability:Basic concepts and terminology[M]. New York:Springer-Verlag,1992
[179]Luckham D,Vera J, Meldal S.Three concepts of system architecture. Technical Report, CSL-TR-95-674, Stanford University,1995.
[180]Zhang S K, Zhang W J, Chang X, et al. Building and assembling reusable components based on software architecture[J]. Journal of Software,2001,12(9):1351-1359 (in Chinese with English abstract).
[181]Neil A. Maiden, Cornelius Ncube. Acquiring COTS software selection requirements[J]. IEEE Software,1998,15(2):46-56.
[182]Ruhe G. Intelligent support for selection of COTS products[J]. Lecture Notes in Computer Scienee,2593(2003):34-45.
[183]Briand L C.COTS evaluation and selection[A].In:Proceedings of the International Conference on Software Maintenance,1998, Washington, DC, USA,222-223.
[184]Vantakavikran P, Prompoon N. Constructing a process model for decision analysis and resolution on COTS selection issue of capability maturity model integration [A]. In: Proceedings of the 6th IEEE/ACIS International Conference on Computer and Information Science. Melbourne,Qld,2007,182-187.
[185]Hsuan-Shih L, Pei-Di S, Wen-Li C. A fuzzy multiple criteria decision making model for software selection[A]. In:Proceedings of the IEEE International Conference on Fuzzy Systems.2004,1709-1713.
[186]Sung W J, Kim J H, Rhew S Y. A quality model for open source software selection[A]. In: Proceedings of the Sixth International Conference on Advanced Language Processing and Web Information Technology (ALPIT 2007). China,2007,515-519.
[187]Donzelli P, et al. Evaluating COTS component dependability in context[J]. IEEE Software, 2005,22(4):46-53.
[188]Ncube C, Maiden N A M. Guiding parallel requirements acquisition and COTS software selection[C]. In:Proceedings of IEEE International Symposium on Requirements Engineering. Limerick, Ireland,1999,133-140.
[189]牟立峰.基于构件的软件开发中的构件供应商任务指派及构件选择方法[D].[博士学位论文].沈阳：东北大学,2009.
[190]张晓梅,张为群.一种基于信任机制的网构软件的构件选择方法研究[J].计算机科学,2010,37(2)：161-164.
[191]Mohamed A, Ruhe G, Eberlein A. COTS selection:Past, Present, and future[C]. In: Proceedings of the 14th Annual IEEE International Conference and Workshops on the Engineering of Computer-Based Systems (ECBS'07).Tucson, Arizona,2007,103-114.
[192]Navarrete F, Botella P, Franch X. How agile COTS selection methods are (and can be)?[C]. In:Proceedings of the 31st EUROMICRO Conference on Software Engineering and Advanced Applications.2005,160-167.
[193]Kohl R J. Requirements engineering changes for COTS-intensive systems[J]. IEEE Software, 2005,22(4):63-64.
[194]Ayag Z, Ozdemir R G. An intelligent approach to ERP software selection through fuzzy ANP[J]. International Journal of Production Research,2007,45(10):2169-2194.
[195]Cechich A, Piattini M. Early detection of COTS component functional suitability[J], Information and SoftwareTechnology,2007,49(2):108-121.
[196]Leung K, Leung H K N. On the efficiency of domain-based COTS Product selection method[J]. Information and Software Technology,2002,44(12):703-715.
[197]Jyrki Kontio. A case study in applying a systematic method for COTS selection[C]. In: Proceedings of the 18th International Conference on Software Engineering (ICSE'96). Washing,DC,USA:IEEE Computer Society,1996,201-209.
[198]李军.软构件工程学习环境开发及应用[D].大连：大连理工大学,2001.
[199]W.M Watkins, H W Lin, K Mcclelland, et al. COTS software selection process[R]. Sandia National Laboratories,US,2006.
[200]Bin W, Jinfang S. Extending FCD process to support COTS selection[A]. In:Proceedings of the 2008 International Conference on Computer Science and Software Engineering.2008, 139-142.
[201]Wanyama T, Far B H. Towards providing decision support for COTS selection[A]. In: Proceedings of the Conference on Electrical and Computer Engineering. Canada,2005, 908-911.
[202]Navarrete F, Botella P, Franch X. Reconciling agility and discipline in COTS selection Processes[A].In:Proceedings of the Sixth International IEEE Conference on Commercial-off-the-Shelf (COTS)-Based Software Systems (ICCBSS'07).Banff,Alta,2007,103-113.
[203]李敏,胡金柱,费丽娟,王军.基于粗糙-模糊集理论的智能化构件选取[J].计算机工程,2004,30(18)：135-137.
[204]Andreou A S,Tziakouris M. A quality framework for developing and evaluating original software components[J]. Information and Software Technology.2007,49(2):122-141.
[205]Keil M, Tiwana A. Beyond cost:The drivers of COTS application value[J]. IEEE Software. 2005,22(3):64-69.
[206]Carvallo J P, Franch X, Quer C. Determining criteria for selecting software components: Lessons learned[J]. IEEE Software,2007,24(3):84-94.
[207]Inoue K, Yokomori R, Yamamoto T, et al.Ranking significance of software components based on use relations[J]. IEEE Transactions on Software Engineering.2005,31 (3):213-225.
[208]Laprie J C. Dependability evaluation of software systems in operation[J]. IEEE Trans on Software Engineering.1984,10(6):701-714.
[209]Gokhale S. An analytical approach to architecture-based software reliability prediction[C]. In.Proceedings of the Third International Computer Performance and Dependability Symposium. Durham, North Carolina,1998.13-22.
[210]Sherif M. Scenario-based reliability analysis of component-based software[C].In: Proceedings of the 10th International Symposium on Software Reliability, Boca Raton, Florida,1999.
[211]Wells L, Christensen S, Kristensen L M, et al. Simulation-based performance analysis of web servers[A]. In:Proceedings of the 9th International Workshop on Petri Nets and Performance Models [C]. Piscataway, USA:IEEE Computer Society,2001,59-68.
[212]毛晓光,邓勇进.基于构件软件的可靠性通用模型[J].软件学报,2004,15(1)：27-32.
[213]徐如志等.基于XML的软件构件查询匹配算法研究[J].软件学报,2003,14(07)：1195-1202.
[214]Mariani L, Pezze M. Dynamic detection of COTS component incompatibility[J]. IEEE Software.2007,24(5):76-85.
[215]Yang Y, Jesal B, Boehm B, et al. Value-based Processes for COTS-based applications[J]. IEEE Software.2005,22(4):54-62.
[216]Baegh J. Certifying software component attributes [J]. IEEE Software.2006,23(3):74-81.
[217]刘晓明等.基于模型的构件系统性能预测综述[J].系统仿真学报.2007,19(13)：2924-2931.
[218]Seker R, Tanik M A. An information-theoretical framework for modeling component-based systems[J]. IEEE Transactions on Systems Man and Cybernetics Part C-Applications and Reviews.2004,34(4):475-484.
[219]Parsons T, et al. Extracting Interactions in Component-Based Systems[J]. IEEE Transactions on Software Engineering.2008,34(6):783-799.
[220]Tom W, Behrouz H F. Repositories for Cots Selection[A].In:Proceedings of the Canada Conference on Electrical and Computer Engineering (CCECE'06). Ottawa,Ont,2006,2416-2419.
[221]Hlupic V, Mann A S. SimSelect:A system for simulation software selection[A]. In: Proceedings of the Simulation Conference. Arlington, VA.USA, Winter,1995,720-727.
[222]张晓梅,张为群.一种基于信任机制的网构软件的构件选择方法研究[J].计算机科学,37(2),2010,161-164.
[223]廖渊,唐磊,李明树.一种基于QoS的服务构件组合方法[J].计算机学报,28(4),2005,627-634.
[224]Cheung, R.C.A User-Oriented Software Reliability Model[J].IEEE Transactions on Software Engineering,1980,6(2):115-125.
[225]Jung-Hua Lo;Sy-Yen Kuo;Lyu M.R;Chin-Yu Huang.Optimal Resource Allocation and Reliability Analysis for Component-based Software Application[J]. In the Proceedings of the 26th Annual International Conference on Computer Software and Application,2002, 12(10):7-12.
[226]Sherif Yacoub. A Scenario-Based Reliability Analysis Approach for Component-Based Software[J]. IEEE Transctions on Reliability,2004,53(4):465-480.
© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号 地址：北京市海淀区学院路29号 邮编：100083 电话：办公室：(+86 10)66554848；文献借阅、咨询服务、科技查新：66554700 |