实时服务构件的语义特征和行为组装形式化技术研究
|
摘要
在面向服务的架构中,如何根据系统资源环境的变化以及构件的功能和实时性等QoS属性动态组合已有的功能构件以满足应用需求,成为当前此领域的一个研究热点。由于采用非形式化(自然语言)和半形式化(图表)方法描述实时服务系统均存在不精确、歧义的及不易验证等缺陷,而形式化方法能较好地克服上述不足,可充分表述系统的各种特性,并为系统的验证、实现等提供良好的基础。
本文提出了一种结合OCL与HTA的实时服务构件(Real-Time ServiceComponent)形式化描述方法:用OCL描述构件的静态语义特征,用HTA描述构件的动态抽象行为;前者为后者的正确性提供属性约束,后者提供前者所描述需求的具体实现,两者语义互补。主要内容及其贡献包括:
(1)提出一种基于特征的构件语义描述模型,首先分别给出特征、特征空间和构件特征空间表示模型的定义。接着将构件特征间的各种关联和依赖关系分成自身约束、父子关系约束、显性约束和隐性约束四类,并采用对象约束语言对这些关系进行形式化描述,从而为模型提供了精确的语义支持。面向电子商务的构件特征子树的实例研究及其模型验证和实验结果证明了该模型的正确性与有效性。
(2)采用HTA形式化描述实时服务构件的动态抽象行为。给出实时服务构件的HTA模型,系统阐述构件间的各种组装方式及其形式模型,分析构件组装的语法可组合性和语义可组合性问题。采用HTA可层次地构造实时系统集成框架,较高层次的实时服务构件的行为可通过由较低层次的构件组成的HTA来定义。该模型的显著特点是简单容易理解,能在一个统一的框架中表示构件的组装、行为和分析系统性能,适用于不同粒度的实时服务构件集成,有效降低了实时服务系统的复杂度,从而使模型验证工具能够处理更为复杂的服务系统。
(3)提出一种基于MLTS的实时服务构件HTA模型组装验证算法。给出(层次)自动机到标号迁移系统的转换过程,在标号迁移系统的扩展模型—多集标号迁移系统基础上,给出其组装算法,利用共享动作是否转换为内部动作来判定模型的组装兼容性。该算法能够有效降低状态空间爆炸给模型实例检测带来的难度,同时利用了MLTS能够描述系统同步、异步动作的特点,不仅可以跟踪构件组装前后的状态变化,而且能够刻画构件的接口行为动作变化,因此,它在基于HTA的实时服务构件模型组装兼容性验证方面具有较强的表达能力。
(4)描述一个较简单但又具有典型实时服务系统特征的小额支付视频点播实例应用系统。首先采用自顶向下的方法构建系统,接着采用本文的描述方法对系统级的构件及其组装进行建模、分析和验证,并简单分析了系统的时间属性。
How to composite a service from its components is a hot-topic in service-oriented architecture. Since non-formal methods, such as nature languages, and half-formal methods, such as graph, can not specify service-oriented systems exactly, formal methods can do it well and provide the bases for model checking and implementation.
This thesis proposes a formal description method of real-time service component which is combined with OCL and HTA. In detail, it describes the static characteristic of the component by using OCL and the dynamic behaviour of the component by using HTA. The OCL description provides the property constraints for the HTA description while the latter description provides the detailed implementation of the former description. The two descriptions are mutually beneficial to each other. The main contributions of this thesis are as follows:
(1) This thesis proposes a feature-based semantic description model for component. First, the presentation models of the feature, the feature space and the component feature space are defined respectively. Then, the association and dependency relations among the features of the components are classified into four types: self constraint, paternity constraint, dominant constraint and recessive constraint. The four kinds of constraints are formally described by the object constraint language, which provides an accurate semantic support for such model. Also, it presents a case study based on a component sub-tree of features for e-business. The results of the model checking and experiments in the object constraint language environment prove that this model is correct and valid.
(2) This thesis employs the HTA to formally describe the dynamic behaviour of the service component. It defines the HTA model of the real-time service component, systematically describes the various composition manners and formal models between different components, and analyzes the syntax compatibility and semantics compatibility of the component composition. By HTA, the integrated system framework can be constructed hierarchically and the behaviour of the high level real-time service component can be defined by the low level components. The obvious advantage of this model is that it can be easily to be understood and it can specify the component composition and its behaviour in a hierarchical and unified framework, which can be applied to the integration of service component with different granularities. As a result, it can efficiently decrease the complexity of the real-time service system, and make possible for applying the model validation tools for more complex service system.
(3) This thesis provides a validation algorithm for the MLTS based HTA model of the real-time service component. It provides conversion process from (hierarchical) automaton to LTS. Based on the extension model of the LTS - the MLTS, we provide the composition algorithm, which determines the composition compatibility according to whether the shared actions are transformed into the internal actions. The proposed algorithm can decrease the difficulties of model instance tests, which is caused by explosion of the state space. Meanwhile, it can not only trace the state variations before and after component composition, but also describe the behavior variations of the component interfaces. Therefore, it is more suitable for the compatibility validation of real-time component composition.
(4) This thesis also presents a case study based on a mobile micro-payment for video-on-demand application system. It first builds the system in a top-down manner, and then uses the methods mentioned above to model, analyze and verify the components and their composition in the system level. Also, the timing properties of the system are analysied.
本文提出了一种结合OCL与HTA的实时服务构件(Real-Time ServiceComponent)形式化描述方法:用OCL描述构件的静态语义特征,用HTA描述构件的动态抽象行为;前者为后者的正确性提供属性约束,后者提供前者所描述需求的具体实现,两者语义互补。主要内容及其贡献包括:
(1)提出一种基于特征的构件语义描述模型,首先分别给出特征、特征空间和构件特征空间表示模型的定义。接着将构件特征间的各种关联和依赖关系分成自身约束、父子关系约束、显性约束和隐性约束四类,并采用对象约束语言对这些关系进行形式化描述,从而为模型提供了精确的语义支持。面向电子商务的构件特征子树的实例研究及其模型验证和实验结果证明了该模型的正确性与有效性。
(2)采用HTA形式化描述实时服务构件的动态抽象行为。给出实时服务构件的HTA模型,系统阐述构件间的各种组装方式及其形式模型,分析构件组装的语法可组合性和语义可组合性问题。采用HTA可层次地构造实时系统集成框架,较高层次的实时服务构件的行为可通过由较低层次的构件组成的HTA来定义。该模型的显著特点是简单容易理解,能在一个统一的框架中表示构件的组装、行为和分析系统性能,适用于不同粒度的实时服务构件集成,有效降低了实时服务系统的复杂度,从而使模型验证工具能够处理更为复杂的服务系统。
(3)提出一种基于MLTS的实时服务构件HTA模型组装验证算法。给出(层次)自动机到标号迁移系统的转换过程,在标号迁移系统的扩展模型—多集标号迁移系统基础上,给出其组装算法,利用共享动作是否转换为内部动作来判定模型的组装兼容性。该算法能够有效降低状态空间爆炸给模型实例检测带来的难度,同时利用了MLTS能够描述系统同步、异步动作的特点,不仅可以跟踪构件组装前后的状态变化,而且能够刻画构件的接口行为动作变化,因此,它在基于HTA的实时服务构件模型组装兼容性验证方面具有较强的表达能力。
(4)描述一个较简单但又具有典型实时服务系统特征的小额支付视频点播实例应用系统。首先采用自顶向下的方法构建系统,接着采用本文的描述方法对系统级的构件及其组装进行建模、分析和验证,并简单分析了系统的时间属性。
How to composite a service from its components is a hot-topic in service-oriented architecture. Since non-formal methods, such as nature languages, and half-formal methods, such as graph, can not specify service-oriented systems exactly, formal methods can do it well and provide the bases for model checking and implementation.
This thesis proposes a formal description method of real-time service component which is combined with OCL and HTA. In detail, it describes the static characteristic of the component by using OCL and the dynamic behaviour of the component by using HTA. The OCL description provides the property constraints for the HTA description while the latter description provides the detailed implementation of the former description. The two descriptions are mutually beneficial to each other. The main contributions of this thesis are as follows:
(1) This thesis proposes a feature-based semantic description model for component. First, the presentation models of the feature, the feature space and the component feature space are defined respectively. Then, the association and dependency relations among the features of the components are classified into four types: self constraint, paternity constraint, dominant constraint and recessive constraint. The four kinds of constraints are formally described by the object constraint language, which provides an accurate semantic support for such model. Also, it presents a case study based on a component sub-tree of features for e-business. The results of the model checking and experiments in the object constraint language environment prove that this model is correct and valid.
(2) This thesis employs the HTA to formally describe the dynamic behaviour of the service component. It defines the HTA model of the real-time service component, systematically describes the various composition manners and formal models between different components, and analyzes the syntax compatibility and semantics compatibility of the component composition. By HTA, the integrated system framework can be constructed hierarchically and the behaviour of the high level real-time service component can be defined by the low level components. The obvious advantage of this model is that it can be easily to be understood and it can specify the component composition and its behaviour in a hierarchical and unified framework, which can be applied to the integration of service component with different granularities. As a result, it can efficiently decrease the complexity of the real-time service system, and make possible for applying the model validation tools for more complex service system.
(3) This thesis provides a validation algorithm for the MLTS based HTA model of the real-time service component. It provides conversion process from (hierarchical) automaton to LTS. Based on the extension model of the LTS - the MLTS, we provide the composition algorithm, which determines the composition compatibility according to whether the shared actions are transformed into the internal actions. The proposed algorithm can decrease the difficulties of model instance tests, which is caused by explosion of the state space. Meanwhile, it can not only trace the state variations before and after component composition, but also describe the behavior variations of the component interfaces. Therefore, it is more suitable for the compatibility validation of real-time component composition.
(4) This thesis also presents a case study based on a mobile micro-payment for video-on-demand application system. It first builds the system in a top-down manner, and then uses the methods mentioned above to model, analyze and verify the components and their composition in the system level. Also, the timing properties of the system are analysied.
引文
[Aalst02] W. Aalst, K. Hee, R. Toorn. Component-Based software architectures: A framework based on inheritance of behavior. Science of Computer Programming, 42:129-171,2002.
[Aho91] A. Aho, A. Dahbura, D. Lee, M. Uyar. An optimization technique for protocol conformance test sequence generation based on UIO sequence and rural Chinese postman tour. IEEE Transactions on Communications, 39(11): 1604-1615,1991.
[Aldini05] A. Aldini, M. Bernardo. On the usability of process algebra: An architectural view. Theoretical Computer Science, 335:281-329, 2005.
[Alfaro01] L. de Alfaro and T. A. Henzinger. Interface automata. In Proceedings of the Foundation of Software Engeneering, Software Engineering Notes, (26): 109-122. ACM Press, 2001.
[Allen97a] R. Allen, D. Garlan. A formal basis for architectural connection. ACM Transactions on Software Engineering and Methodology, 6(3):213-249, July 1997.
[Allen97b] R.J. Allen. A formal approach to software architecture. Technical Report. TR#CMU-CS-97-144, Carnegie Mellon University, 1997.
[AlurR92] R. Alur, C. Courcoubetis, Dill DL, Halbwachs N, Wong-Toi H. Minimization of timed transition systems. In: Cleaveland R, ed. Proc, of the 3rd Conf, on Concurrency Theory. LNCS630:340-354, Berlin: Springer-Verlag, 1992.
[AlurR93] R. Alur, C. Courcoubetis, and D. Dill, Model-checking in dense real-time, Information and Computation, (104):2-34,1993.
[AlurR94] R. Alur et al. A theory of timed automata [J]. Theor. Comp. Sci., 126: 183-235, 1994.
[AlurR96] R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering 22:181-201, 1996.
[AlurR99] R. Alur. Timed automata. In: Halbwachs N, Peled D, eds. Proc, of the 11th Int'l Conf. on Computer-Aided Verification. LNCS1633:8-22, London: Springer-Verlag, 1999.
[Behrmann99] G. Behrmann, K.G. Larsen, J. Pearson, C. Weise, Wang Yi. Efficient timed reachability analysis using clock diffirence diagrams. CAV'99, LNCS 1633, Springer-Verlag, Trento, Italy, July 1999.
[Bengtsson03] J. Bengtsson, Y. Wang. Timed automata: Semantics, algorithms and tools. In: Desel J, Reisig W, Rozenberg G, eds. Lectures on Concurrency and Petri Nets 2003. LNCS3098:87-124, Berlin: Springer-Verlag, 2004.
[Bernardo02] M. Bernardo, P. Ciancarini P, L. Donatiello. Architecting families of software systems with process algebras. ACM Transactions on Software Engineering and Methodology, 11(4):386-426, 2002.
[Beyer03]D.Beyer,C.Lewerentz,A.Noack.Rabbit:A tool for BDD-based verification of real-time systems.Computer-Aided Verification 2003(CAV 2003),Boulder,Colorado,USA,July 8-12,2003.
[Bjomer00]N.Bjomer,A.Browne,M.Colon,B.Finkbeiner,Z.Manna,H.Sipma,T.Uribe.Verifying temporal properties of reactive systems:A Step tutorial.In Formal Methods in System Design,(16):227-270.2000.
[Bouajjani02]A.Bouajjani,J.Fernandez,N.Halbwachs,P.Raymond,C.Ratel.Minimal state graph generation.Science of Computer Programming,18(3):247-269,1992.
[Bormans03]J.Bormans,J.Gelissen,A.Perkis.MPEG-21:The 21st century multimedia framework.Signal Processing Magazine,IEEE,20(2):53-62,March 2003.
[Brinksma01]E.Brinksma and J.Tretmans.Testing transition systems:An annotated bibliography.In MOVEP2000,LNCS2067,Springer,2001.
[Broy99]M.Broy,O.Slotosch:Enriching the Software Engineering Process by Formal Methods.LNCS 1641:1-43,Springer Verlag.1999.
[Burch90]J.R.Burch,Edmund M.Clarke,K.L.McMillan,D.L.Dill,and L.J.Hwang.Symbolic model checking:10~(20)states and beyond.In Proceedings of the 5~(th)Annual IEEE Symposium Logic in Computer Science:428-439,1990.
[Cardell98]R.Cardell-Oliver,T.Glover.A practical and complete algorithm for testing real-time systems.In:Ravn AP,Rischel H,eds.Proc.of the 5th Int'l Syrup.on Formal Techniques in Real-Time and Fault-Tolerant Systems.LNCS1486:251-261,Berlin:Springer-Verlag,1998.
[Chan89]W.Chan,C.Vuong,M.Otp.An improved protocol test generation procedure based on UIOS.In:Landweber LH,ed.Symp.Proc.on Communications Architectures & Protocols:283-294,ACM Press,New York,1989.
[ChangJC00]常继传,李克勤,郭立峰,等.青鸟系统中可复用软件构件的表示与查询.电子学报,28(8):20-24,2000.
[ChangJY02]J.Chang and H.Ma.Modeling the architecture for component-based e-commerce system.(ICFEM2002)LNCS2495:98-102,Springer,Germany,Oct.2002.
[ChenW07]陈伟,薛云志,赵琛,李明树.一种基于时间自动机的实时系统测试方法.软件学报,18(1):62-73,Jan.2007.
[Chow78]T.Chow.Testing software design modeled by finite-state machines.IEEE Transactions on Software Engineering,4(3):178-187,1978.
[Clarke83]M.Edmund,E.Clarke,A.Emerson,and A.P.Sistla.Automatic verification of finite state concurrent systems using temporal logic specifications:A practical approach.In Proc.of the 10~(th)ACM Symposium on Principles of Programming Languages:117-126,Austin,TX,Jan.24-26 1983.
[Clarke94]E.Clarke,O.Grumberg,and E.David.Long.Model checking and abstraction.ACM Transactions on Programming Languages and Systems,16(5):1512-1542,1994.
[Clarke96]E.Clarke,J.Wing.Formal methods:State of the art and future directions.ACM Computing Surveys,28(4):626-843,1996.
[Cleaveland93]J.Parrow,R.Cleaveland and B.Steffen.The concurrency workbench:A semantic-based verification tool for the verification of concurrent systems.ACM Transactions on Programming Languages and Systems,5(1):36-72,1993.
[Courcoubetis92]C.Courcoubetis,M.Vardi,P.Volper,and M.Yannakakis.Memory-efficient algorithms for the verification of temporal properties.Formal Methods in System Design,1(2/3):275-288,1992.
[David98]A.David,W.Yi.Hierarchical timed automata for UPPAAL.10th Nordic Workshop on Programming Theory(NWPT'98).Turku Centre for Computer Science(TUCS),Finland,1998.
[David01]A.David and M.Oliver Moller.From HUppaal to Uppaal:A translation from hierarchical timed automata to fiat timed automata.Research Series RS-01-11,BRICS,Department of Computer Science,University of Aarhus,Mar.2001.
[Daws96]C.Daws,A.Olivero,S.Tripakis,and s.Yovine.The tool KRONOS.In Hybrid Systems,1996.
[Dembinski]P.Dembinski,etc..Verics:A tool for verifying timed automata and Estelle specifications,http://citeseer.ist.psu.edu/dembinski03verics.html.
[Desmond98]F.Desmond,C.Alan.UML,objects,components,and frameworks with UML:The catalysis approach,reading:Addison-Wesley Longman,Inc.,1998.
[Dill89]D.Dill.Timing assumptions and verification of finite-state concurrent systems.CAV'89,LNCS407,Springer-Verlag,1989.
[DongW01]董威,王戟齐,治昌.并发和实时系统的模型检验技术.计算机研究与发展,38(6),June 2001.
[Eisner02]C.Eisner and D.Peled.Comparing symbolic and explicit model checking of a software system.In Proc.of the 9th International SPIN Workshop on Model Checking of Software:230-239,Springger-Verlag,2002.
[Emerson96]E.Emerson and A.Sistla.Symmetry and model checking.Formal Methods in System Design,9(1-2):105-131,1996.
[FanJ05]J.Fan,S.Kambhampati.A snapshot of public Web services.SIGMOD Record,34(1):24-32,2005.
[FarrellJ07]J.Farrell,H.Lausen.Semantic annotations for WSDL and XML schema.2007.HTTP://www.w3.org/TR/sawsdl/.
[FengT00]冯铁,张家晨,陈伟,金淳兆.基于框架和角色模型的软件体系结构规约.软件学报,11(8):1078-1086,2000.
[Frappier99]M.Frappier,H.Habrias(eds).Software Specification Methods—An overview using a case study.Springer-Verlag,1999.
[Fujiwara91]Fujiwara S,Bochmann GV.Test selection based on finite state models.IEEE Transactions on Software Engineering,17(6):591-603,1991.
[Garlan94]D.Garlan,R.Allen,J.Ockerbloom.Exploiting style in architectural design environments.In Proc.of SIGSOFT '94 Symposium on the Foundations of Software Engineering:179-185,ACM Press,Dec.1994.
[Garlan97]D.Garlan,R.Monroe,D.Wile.Acme:an architecture description interchange language.In:Johnson JH,ed.Proceedings of the CASCON' 97:169-183.1997.
[Godefroid97] P. Godefroid. Verisoft: A tool for the automatic analysis of concurrent reactive software. In Proc, of the 9th Conference on Computer Aided Verification (CAV), LNCS1254: 476-479, Haifa, June 1997.
[Godefroid05] P. Godefroid. Software model checking: The verisoft approach. Formal Methods in System Design, 26(2), 2005.
[Gordon93] M. Gordon, T. Melham. Introduction to HOL: A theorem proving environment for higher-order logic. Cambridge University Press, 1993.
[Gossler05] G. Gossler and J. Sifakis: Composition for component-based modeling. Sci. Comput. Program, 55(1-3):161-183, 2005.
[GuZH05] Z. Gu, K. Shin. Synthesis of real-time implementations from component-based software models. Proc, of IEEE Real-Time Systems Symposium, 2005.
[Havelund00] K. Havelund and T. Pressburger. Model checking java programs using java pathfinder. International Journal on Software Tools for Technology Transfer (STTT), 2(4), 2000.
[Heineman01] G.Heineman, W. Councill. Component-based software engineering. Boston: Addison-Wesley, 2001.
[Henzinger92] T. Henzinger, Z. Manna, A. Pnueli. Timed transition system. In: Bakker JWD, Huizing C, Roever WPD, Rozenberg G, eds. Proc, of the Real-Time: Theory in Practice, REX Workshop. LNCS600:226-251, Berlin: Springer-Verlag 1992.
[Henzinger94] T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193-244 1994.
[Henzinger97] T. Henzinger, P. Ho, and H. Wong-Toi. HyTech: A model checker for hybrid systems. Software Tools for Technology Transfer, 1:110-122, 1997.
[Henzinger06] T. Henzinger and S. Matic. An interface algebra for real-time components.In IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS): 253-266, 2006.
[Hessel03] A. Hessel, K. Larsen, B. Nielsen, P. Pettersson, and A. Skou. Time-optimal test cases for real-time systems. In: Larsen KG, Niebert P, eds. Proc, of the 1st Int'l Workshop, FORMATS 2003, LNCS2791:234-245, Berlin: Springer-Verlag, 2003.
[Hoare85] C. Hoare. Communicating sequential processes. Prentice-Hall, 1985.
[Holzmann91] G.Holzmann. Design and validation of computer protocols. Prentice-Hall, Englewood Cliffs, New Jersey, 1991.
[Holzmann95] G.Holzmann and D. Peled. An improvement in formal verification. In FORTE 1994: 197-211, 1995.
[Holzmann97] G.Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279-295, 1997.
[Holzmann04] G.Holzmann. The SPIN model checker: Primer and reference manual. HOL g 03:11.Ex., Addison Wesley, 2004.
[HuJ05] J. Hu, X. Yu, Y. Zhang, T. Zhang, X. Li, and G. Zheng. Checking component-based embedded software designs for scenario-based timing specifications. EUC 2005: 395-404, 2005.
[Inverardi95] P. Inverardi, A. Wolf. Formal specification and analysis of software architectures using the chemical abstract machine model. IEEE Transactions on Software Engineering, 21(4):373-386,1995.
[Jeffrey03] J. Jeffrey. E. Tsai, Y. Juan, and S. Avinash. Model and algorithm for efficient verification of high-assurance properties of real-Time systems. IEEE transactions on Knowledge and Data Engineering, 15(2), March/April 2003.
[JiaoWP06] W. Jiao, H. Mei. Automating integration of heterogeneous COTS components. ICSR 2006: 29-42,2006.
[JinXL05a] X. Jin, H. Ma. An approach to formally modeling the component-based e-commerce system. IEEE International Workshop on Service-Oriented System Engineering, Beijing, China, October 20-21, 2005.
[JinXL05b] X. Jin, H. Ma. Hierarchically modeling the component-based real-time system with duration calculus. The Fifth International Conference on Information, Communications and Signal Processing, Bangkok, Thailand, December 6-9, 2005.
[JinXL05c] X. Jin, H. Ma, and Z. Gu. Real-Time Component Composition using Hierarchical Timed Automata. Proc. International Conference on Quality Software (QSIC 2007), October 10-12,2007.
[JY02] 贾育,顾毓清．基于领域特征空间的构件语义表示方法．软件学报,13(2)：311-316,2002．
[Kang90] K. Kang, S. Cohen, J. Hess, W. Novak, A. Peterson. Feature-Oriented domain analysis (FODA) feasibility study. Technical Report, CMU/SEI-90-TR-21. Pittsburgh: Carnegie Mellon University, Software Engineering Institute: 1-52, 1990.
[Katz92] S. Katz and D. Peled. Verification of distributed programs using representative interleaving sequences. Distributed Computing, 6:107-120,1992.
[Kaynar03] D. Kaynar, N. Lynch, R. Segala, F. Vaandrager. Timed I/O automata: A mathematical framework for modeling and analyzing real-time systems. In: Kaynar DK, Lynch N, Segala R, Vaandrager F, eds. Proc, of the 24th IEEE Int'l Real-Time Systems Symp. Washington: 166-177, IEEE Computer Society, 2003.
[Krichen05] M. Krichen, S. Tripakis. State identification problems for timed automata. In: Khendek F, Dssouli R, eds. Proc, of the 17th IFIP Int'l Conf, on Testing of Communicating Systems (TestCom 2005). LNCS3502:175-191, Berlin: Springer-Verlag, 2005.
[Lamport94] L. Lamport. The temporal logic of actions. ACM Transactions on Programming Language and Systems, 16(3):872-923, 1994.
[Laroussinie98] F. Laroussinie and K. G. Larsen, CMC: A tool for compositional modelchecking of real-time systems. In Proc. IFIP Joint Int. Conf. Formal Description Techniques & Protocol Specification, Testing, and Verification (FORTE-PSTV'98): 439-456, Kluwer Academic Publishers, 1998.
[Larsen93] K. Larsen, Y. Wang. Time abstracted bisimiulation: Implicit specifications and decidability. In: Brookes SD, Main MG, Melton A, Mislove MW, Schmidt DA, eds. Proc, of the 9th Int'l Conf, on Mathematical Foundation of Programming Semantics. LNCS802:160-176, Berlin: Springer-Verlag, 1993.
[Larsen97]K.Larsen,P.Pettersson,and Y.Wang.Uppaal in a nutshell.Int.Journal on Software Tools for Technology Transfer,1(1-2):134-152,Oct.1997.
[Larsen05]K.Larsen,M.Mikucionis,and B.Nielsen.Online testing of real-time systems using uppaal.In:Grabowski J,Nielsen B,eds.Formal Approaches to Software Testing:4th Int'l Workshop.LNCS3395:79-94,Linz:Springer-Verlag,2005.
[LiCY06]李长云,李赣生,何频捷.一种形式化的动态体系结构描述语言.软件学报,17(6):1349-1359,2006.
[LinHM02]林惠民,张文辉.模型检测:理论、方法与应用.电子学报,30(12A):1907-1912.Dec.2002.
[LiuWM01]W.Liu,H.Ma.Modeling video-on-demand system in temporal logic.IEEE Pacific Rim Conference on Multimedia,2001.
[Luckham95]D.Luckham,J.Vera.An Event-Based Architecture Definition Language.IEEE Transactions on Software Engineering,21(9):717-734,1995.
[LuoHJ00]骆华俊,唐稚松.可视化体系结构描述语言XYZ/ADL.软件学报,11(8):1024-1029,2000.
[LvJ00]吕建,张鸣,廖宇,陶先平.基于移动Agent技术的构件软件框架研究.软件学报,11(8):1018-1023,2000.
[Magee95]J.Magee,N.Dulay,S.Eisenbach,and J.Kramer,Specifying distributed software architectures.In:Proc of the 5th European Software Engineering Conference(ESEC '95),LNCS989:137-153,Springer-Verlag,Sep.1995.
[MaH06]H.Ma,I.Yen,J.Zhou,and K.Coope.QoS analysis for component-based embedded software:Model and methodology.Journal of Systems and Software,79(6):859-870,2006.
[MaHD02]马华东,多媒体计算机技术原理(第2版).清华大学出版社,2002.
[Malte01]K.Malte.The future of m-payments-business option and policy issues.Background Paper No.2,Electronic payment Systems Observatory(ePSO),Aug.2001.
[Mandrioli95]D.Mandrioli,S.Morasca,and A.Morzenti.Generating test cases for real-time systems from logic specifications.ACM Transactions on Computer Systems,13(4):365-398,1995.
[McMillan92]K.McMillan.Symbolic model checking:An approach to the state explosion problem.Technical Report CMU-CS-92-131,Carnegie Mellon University,1992.
[Medvidovic96]N.Medvidovic,P.Orcizy,J.Robbins,and R.Taylor.Using object-oriented typing to support architectural design in the C2 style.In:D.Garlan,ed.Proceedings of the ACM SIGSOF7' 96:the 4th Symposium on the Foundations of Software Engineering:24-32,ACM Press,1996.
[Medvidovic00]N.Medvidovic,R.Taylor.A classification and comparison framework for software architecture description language.IEEE Transactions on Software Engineering,26(1):70-93,2000.
[MeiH02]H.Mei,L.Zhang,F.Yang.A component-based software configuration management model and its supporting system.Journal of Computer Science and Technology.17(4),July,2002.
[MeiH03]梅宏,陈锋,冯耀东,杨杰.ABC:基于体系结构、面向构件的软件开发方法.软件学报,14(4):721-732,2003.
[Milner98]R.Milner.Communication and concurrency.Prentice-Hall,1998.
[Milner99]R.Milner.Communicating and mobile systems:the Pi-calculus.Cambridge University Press,1999.
[Neema03]S.Neema,J.Sztipanovits,G.Karsai,and K.Butts.Constraint-based design-space exploration and model synthesis.In EMSOFT:290-305,2003.
[Moriconi95]M.Moriconi,X.Qian,and R.Riemenschneider.Correct architecture refinement.IEEE Transactions on Software Engineering,21(4):356-372,1995.
[Musuvathi04]M.Musuvathi and D.Engler.Model checking large network protocol implementations.In Proceedings of the 1st Symposium on networked Systems Design and Implementation:155-168.USENIX Association,2004.
[Narayanan02]S.Narayanan,S.Mcllraith.Simulation,verification and automated composition of web services.In:Proc.of the 11th Int'l Conf.on World Wide Web.New York:ACM Press,77-88.2002.
[Nouaary02]A.En-Nouaary,R.Dssouli,F.Khendek.Timed Wp-method:Testing real-time systems.IEEE Trans.on Software Engineering,28(11):1023-1038,2002.
[OCLE05]OCLE Tool,http://lci.cs.ubbcluj.ro/OCLE/index.htm.
[OMG03]Object Management Group:UML 2.00CL Specification.
[Owre98]S.Owre,J.Rushby,N.Shankar,and D.Stringer-Calvert.PVS:an experience report.In D,Huter,W.Stephan,P.Traverso,and M.Ullman,eds.,Applied Formal Methods-FM-Trends 98,LNCS 1641:338-345.Springer-Verlag,1998.
[PengX06]彭鑫,赵文耘,刘奕明.基于特征模型和构件语义的概念体系结构设计.软件学报,17(6):1307-1317,2006.
[Podgurski93]A.Podgurski,L.Pierce.Retrieving reusable software by sampling behavior.ACM Transactions on Software Engineering and Methodology,2(3):286-303,1993.
[QianZZ06]钱柱中,陆桑璐,谢立.基于Petri网的Web服务自动组合研究.计算机学报,29(7):1057-1066,2006.
[RenHM03]任洪敏,钱乐秋.构件组装及其形式化推导研究.软件学报,14(6):1066-1074,2003.
[RaoJ05]J.Rao,X.Su.A survey of automated Web service composition methods.In:Cardoso J,Sheth A,eds.Proc.of the SWSWPC 2004.LNCS3387:43-54,Berlin,Heidelberg:Springer-Verlag,2005.
[Schumann01]J.Schumann.Automated theorem proving in software engineering.Berlin Heidelerg:Springer-Verlag,2001.
[Sedigh05]S.Sedigh-Ali,A.Ghafoor.A graph-based model for component-based software development.In WORDS:254-262,2005.
[Sekerinski01]E.Sekerinski,K.Sere(eds).Program development by refinement(case studies using the B method).London:Springer-Verlag,2001.
[Shaw95] M. Shaw, R. DeLine, D. Klein, T. Ross, M. David and Y. Zelesnik. Abstractions for software architecture and tools to support them. IEEE Transactions on Software Engineering, Special Issue on software Architecture, 21(4): 314-335, 1995.
[Shaw96] M. Shaw, D. Garlan. Software Architecture: Perspectives on an Emerging Discipline. New Jersey: Prentice Hall, 1996.
[Sidhu89] D. Sidhu, T. Leung. Formal methods for protocol testing: A detailed study. IEEE Transactions on Software Engineering, 15(4): 413-426, 1989.
[SirinE04] E.Sirin, etc.. HTN planning for Web service composition using SHOP2. Journal of Web Semantics, l(4):377-396,2004.
[Sistla00] A. Sistla, V. Gyuris, and E. Allen. Smc: a symmetry-based model checker for verification of safety and liveness properties. ACM Transactions on Software Engineering Methodology, 9(2): 133-166,2000.
[Souza97] D. Souza and A. Wills.Objects, components and frameworks with UML - the catalysis approach. Addison-Wesley, 1997.
[Springintveld01] J. Springintveld, F. Vadranger, and P. Dargenio. Testing timed automata. Theoretical Computer Science, 254(1-2):225-257, 2001.
[Stahl99] K. Stahl, K. Baukus, Y. Lakhnech, and M. Steffen. Divide, abstract, and model-check. In SPIN: 57-76,1999.
[SunY03] Y. Sun, H. Ma. A component-based iterative software development model and the application. CNCC'2003, 2003.
[Szypersky98] C. Szypersky. Component software beyond object-oriented programming, Addison-Wesley, ACM Press, New York, 1998.
[Szypersky02] C. Szypersky, D. Gruntz, S. Murer. Component software: Beyond object-oriented programming. 2nd. Massachusetts: Addison-Wesley Professional, 2002.
[Tretmans02] J. Tretmans. Testing techniques. Lecture notes, University of Twente, The Netherlands, 2002.
[Tripakis96] S. Tripakis, C. Courcoubetis. Extending Promela and Spin for real time, Proceedings of TACAS '96, LNCS1055, 1996.
[Tripakis01] S. Tripakis, S. Yovine. Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design, 18(1):25-68, 2001.
[Vallecillo00] A. Vallecillo, J. Hernandez, and J. Troya. New issues in object interoperability. In Proc, of the ECOOP 2000 Workshop on Object Interoperability. LNCS 1964:256-269, France, 2000.
[Wandeler06] E. Wandeler and L. Thiele: Interface-based design of real-time systems with hierarchical scheduling. In IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS): 243-252, 2006.
[WangJZ00] J. Wang, Q. Xu, and H. Ma. Modeling and verification of a network player system with DCValid. First Asia-Pacific Conference on Quality Software, 30-31 Oct. 2000.
[Warmer03] J. Warmer, A. Kleppe. The object constraint language: Getting your models ready for MDA. Second Edition, Addison-Wesley, 2003.
[WangXG04]王晓光,冯耀东,梅宏.ABC/ADL:一种基于XML的软件体系结构描述语言.计算机研究与发展,第9期,2004.
[WangYF02]王渊峰,张涌,任洪敏等,基于刻面描述的构件检索.软件学报,13(8):1546-1551,2002.
[WangF00]F.Wang.Region encoding diagram for fully symbolic verification of real-time systems.In Proc.of 24th International Computer Software and Applications Conference:509-515,Berlin,Germany,March 2000.
[WangF05]F.Wang.Symbolic parametric safety analysis of linear hybrid systems with BDD-Like data-structures.IEEE Transactions on Software Engineering,31(1):38-51,Jan.2005.
[Wing90]J.Wing.A specifier's introduction to formal methods.IEEE Computer,23(9):8-24,1990.
[Wozna02]B.Wozna,W.Penczek,and A.Zbrzezny.Reachiability for timed systems based on SAT-solvers.In Proc.of the Int.Workshop on Concurrency,Specification and Programming(CS&P'02),Informatik-Berichte,161(2):380-395,Humboldt University,2002.
[Yovine97]S.Yovine.KRONOS:A verification tool for real-time systems.Springer International Journal of Software Tools for Technology Transfer,1(1/2):123-133,1997.
[Zaremski96]A.Zaremski.Signature and specification matching:[Ph.D,dissertation].School of Computer Science Carnegie Mellon University,1996.
[ZengL04]L.Zeng etc..QoS-Aware middleware for Web services composition.IEEE Transactions on Software Engineering,30(5):311-327,2004.
[ZhangJC00]张家晨,冯铁,陈伟,金淳兆.基于主动连接件的软件体系结构及其描述方法.软件学报,11(8):1047-1052,2000.
[ZhangSK02]张世琨,王立福,杨芙清.基于层次消息总线的软件体系结构风格.中国科学(E辑),32(3):393-400,2002.
[ZhangWH95]W.Zhang.Verification of XYZ/SE Programs.Chinese J.of Adv.Software Research,April 1995.
[ZhuXY03]朱雪阳,唐稚松.基于时序逻辑的软件体系结构描述语言XYZ/ADL.软件学报,14(4):731-720,2003.
[Aho91] A. Aho, A. Dahbura, D. Lee, M. Uyar. An optimization technique for protocol conformance test sequence generation based on UIO sequence and rural Chinese postman tour. IEEE Transactions on Communications, 39(11): 1604-1615,1991.
[Aldini05] A. Aldini, M. Bernardo. On the usability of process algebra: An architectural view. Theoretical Computer Science, 335:281-329, 2005.
[Alfaro01] L. de Alfaro and T. A. Henzinger. Interface automata. In Proceedings of the Foundation of Software Engeneering, Software Engineering Notes, (26): 109-122. ACM Press, 2001.
[Allen97a] R. Allen, D. Garlan. A formal basis for architectural connection. ACM Transactions on Software Engineering and Methodology, 6(3):213-249, July 1997.
[Allen97b] R.J. Allen. A formal approach to software architecture. Technical Report. TR#CMU-CS-97-144, Carnegie Mellon University, 1997.
[AlurR92] R. Alur, C. Courcoubetis, Dill DL, Halbwachs N, Wong-Toi H. Minimization of timed transition systems. In: Cleaveland R, ed. Proc, of the 3rd Conf, on Concurrency Theory. LNCS630:340-354, Berlin: Springer-Verlag, 1992.
[AlurR93] R. Alur, C. Courcoubetis, and D. Dill, Model-checking in dense real-time, Information and Computation, (104):2-34,1993.
[AlurR94] R. Alur et al. A theory of timed automata [J]. Theor. Comp. Sci., 126: 183-235, 1994.
[AlurR96] R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering 22:181-201, 1996.
[AlurR99] R. Alur. Timed automata. In: Halbwachs N, Peled D, eds. Proc, of the 11th Int'l Conf. on Computer-Aided Verification. LNCS1633:8-22, London: Springer-Verlag, 1999.
[Behrmann99] G. Behrmann, K.G. Larsen, J. Pearson, C. Weise, Wang Yi. Efficient timed reachability analysis using clock diffirence diagrams. CAV'99, LNCS 1633, Springer-Verlag, Trento, Italy, July 1999.
[Bengtsson03] J. Bengtsson, Y. Wang. Timed automata: Semantics, algorithms and tools. In: Desel J, Reisig W, Rozenberg G, eds. Lectures on Concurrency and Petri Nets 2003. LNCS3098:87-124, Berlin: Springer-Verlag, 2004.
[Bernardo02] M. Bernardo, P. Ciancarini P, L. Donatiello. Architecting families of software systems with process algebras. ACM Transactions on Software Engineering and Methodology, 11(4):386-426, 2002.
[Beyer03]D.Beyer,C.Lewerentz,A.Noack.Rabbit:A tool for BDD-based verification of real-time systems.Computer-Aided Verification 2003(CAV 2003),Boulder,Colorado,USA,July 8-12,2003.
[Bjomer00]N.Bjomer,A.Browne,M.Colon,B.Finkbeiner,Z.Manna,H.Sipma,T.Uribe.Verifying temporal properties of reactive systems:A Step tutorial.In Formal Methods in System Design,(16):227-270.2000.
[Bouajjani02]A.Bouajjani,J.Fernandez,N.Halbwachs,P.Raymond,C.Ratel.Minimal state graph generation.Science of Computer Programming,18(3):247-269,1992.
[Bormans03]J.Bormans,J.Gelissen,A.Perkis.MPEG-21:The 21st century multimedia framework.Signal Processing Magazine,IEEE,20(2):53-62,March 2003.
[Brinksma01]E.Brinksma and J.Tretmans.Testing transition systems:An annotated bibliography.In MOVEP2000,LNCS2067,Springer,2001.
[Broy99]M.Broy,O.Slotosch:Enriching the Software Engineering Process by Formal Methods.LNCS 1641:1-43,Springer Verlag.1999.
[Burch90]J.R.Burch,Edmund M.Clarke,K.L.McMillan,D.L.Dill,and L.J.Hwang.Symbolic model checking:10~(20)states and beyond.In Proceedings of the 5~(th)Annual IEEE Symposium Logic in Computer Science:428-439,1990.
[Cardell98]R.Cardell-Oliver,T.Glover.A practical and complete algorithm for testing real-time systems.In:Ravn AP,Rischel H,eds.Proc.of the 5th Int'l Syrup.on Formal Techniques in Real-Time and Fault-Tolerant Systems.LNCS1486:251-261,Berlin:Springer-Verlag,1998.
[Chan89]W.Chan,C.Vuong,M.Otp.An improved protocol test generation procedure based on UIOS.In:Landweber LH,ed.Symp.Proc.on Communications Architectures & Protocols:283-294,ACM Press,New York,1989.
[ChangJC00]常继传,李克勤,郭立峰,等.青鸟系统中可复用软件构件的表示与查询.电子学报,28(8):20-24,2000.
[ChangJY02]J.Chang and H.Ma.Modeling the architecture for component-based e-commerce system.(ICFEM2002)LNCS2495:98-102,Springer,Germany,Oct.2002.
[ChenW07]陈伟,薛云志,赵琛,李明树.一种基于时间自动机的实时系统测试方法.软件学报,18(1):62-73,Jan.2007.
[Chow78]T.Chow.Testing software design modeled by finite-state machines.IEEE Transactions on Software Engineering,4(3):178-187,1978.
[Clarke83]M.Edmund,E.Clarke,A.Emerson,and A.P.Sistla.Automatic verification of finite state concurrent systems using temporal logic specifications:A practical approach.In Proc.of the 10~(th)ACM Symposium on Principles of Programming Languages:117-126,Austin,TX,Jan.24-26 1983.
[Clarke94]E.Clarke,O.Grumberg,and E.David.Long.Model checking and abstraction.ACM Transactions on Programming Languages and Systems,16(5):1512-1542,1994.
[Clarke96]E.Clarke,J.Wing.Formal methods:State of the art and future directions.ACM Computing Surveys,28(4):626-843,1996.
[Cleaveland93]J.Parrow,R.Cleaveland and B.Steffen.The concurrency workbench:A semantic-based verification tool for the verification of concurrent systems.ACM Transactions on Programming Languages and Systems,5(1):36-72,1993.
[Courcoubetis92]C.Courcoubetis,M.Vardi,P.Volper,and M.Yannakakis.Memory-efficient algorithms for the verification of temporal properties.Formal Methods in System Design,1(2/3):275-288,1992.
[David98]A.David,W.Yi.Hierarchical timed automata for UPPAAL.10th Nordic Workshop on Programming Theory(NWPT'98).Turku Centre for Computer Science(TUCS),Finland,1998.
[David01]A.David and M.Oliver Moller.From HUppaal to Uppaal:A translation from hierarchical timed automata to fiat timed automata.Research Series RS-01-11,BRICS,Department of Computer Science,University of Aarhus,Mar.2001.
[Daws96]C.Daws,A.Olivero,S.Tripakis,and s.Yovine.The tool KRONOS.In Hybrid Systems,1996.
[Dembinski]P.Dembinski,etc..Verics:A tool for verifying timed automata and Estelle specifications,http://citeseer.ist.psu.edu/dembinski03verics.html.
[Desmond98]F.Desmond,C.Alan.UML,objects,components,and frameworks with UML:The catalysis approach,reading:Addison-Wesley Longman,Inc.,1998.
[Dill89]D.Dill.Timing assumptions and verification of finite-state concurrent systems.CAV'89,LNCS407,Springer-Verlag,1989.
[DongW01]董威,王戟齐,治昌.并发和实时系统的模型检验技术.计算机研究与发展,38(6),June 2001.
[Eisner02]C.Eisner and D.Peled.Comparing symbolic and explicit model checking of a software system.In Proc.of the 9th International SPIN Workshop on Model Checking of Software:230-239,Springger-Verlag,2002.
[Emerson96]E.Emerson and A.Sistla.Symmetry and model checking.Formal Methods in System Design,9(1-2):105-131,1996.
[FanJ05]J.Fan,S.Kambhampati.A snapshot of public Web services.SIGMOD Record,34(1):24-32,2005.
[FarrellJ07]J.Farrell,H.Lausen.Semantic annotations for WSDL and XML schema.2007.HTTP://www.w3.org/TR/sawsdl/.
[FengT00]冯铁,张家晨,陈伟,金淳兆.基于框架和角色模型的软件体系结构规约.软件学报,11(8):1078-1086,2000.
[Frappier99]M.Frappier,H.Habrias(eds).Software Specification Methods—An overview using a case study.Springer-Verlag,1999.
[Fujiwara91]Fujiwara S,Bochmann GV.Test selection based on finite state models.IEEE Transactions on Software Engineering,17(6):591-603,1991.
[Garlan94]D.Garlan,R.Allen,J.Ockerbloom.Exploiting style in architectural design environments.In Proc.of SIGSOFT '94 Symposium on the Foundations of Software Engineering:179-185,ACM Press,Dec.1994.
[Garlan97]D.Garlan,R.Monroe,D.Wile.Acme:an architecture description interchange language.In:Johnson JH,ed.Proceedings of the CASCON' 97:169-183.1997.
[Godefroid97] P. Godefroid. Verisoft: A tool for the automatic analysis of concurrent reactive software. In Proc, of the 9th Conference on Computer Aided Verification (CAV), LNCS1254: 476-479, Haifa, June 1997.
[Godefroid05] P. Godefroid. Software model checking: The verisoft approach. Formal Methods in System Design, 26(2), 2005.
[Gordon93] M. Gordon, T. Melham. Introduction to HOL: A theorem proving environment for higher-order logic. Cambridge University Press, 1993.
[Gossler05] G. Gossler and J. Sifakis: Composition for component-based modeling. Sci. Comput. Program, 55(1-3):161-183, 2005.
[GuZH05] Z. Gu, K. Shin. Synthesis of real-time implementations from component-based software models. Proc, of IEEE Real-Time Systems Symposium, 2005.
[Havelund00] K. Havelund and T. Pressburger. Model checking java programs using java pathfinder. International Journal on Software Tools for Technology Transfer (STTT), 2(4), 2000.
[Heineman01] G.Heineman, W. Councill. Component-based software engineering. Boston: Addison-Wesley, 2001.
[Henzinger92] T. Henzinger, Z. Manna, A. Pnueli. Timed transition system. In: Bakker JWD, Huizing C, Roever WPD, Rozenberg G, eds. Proc, of the Real-Time: Theory in Practice, REX Workshop. LNCS600:226-251, Berlin: Springer-Verlag 1992.
[Henzinger94] T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193-244 1994.
[Henzinger97] T. Henzinger, P. Ho, and H. Wong-Toi. HyTech: A model checker for hybrid systems. Software Tools for Technology Transfer, 1:110-122, 1997.
[Henzinger06] T. Henzinger and S. Matic. An interface algebra for real-time components.In IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS): 253-266, 2006.
[Hessel03] A. Hessel, K. Larsen, B. Nielsen, P. Pettersson, and A. Skou. Time-optimal test cases for real-time systems. In: Larsen KG, Niebert P, eds. Proc, of the 1st Int'l Workshop, FORMATS 2003, LNCS2791:234-245, Berlin: Springer-Verlag, 2003.
[Hoare85] C. Hoare. Communicating sequential processes. Prentice-Hall, 1985.
[Holzmann91] G.Holzmann. Design and validation of computer protocols. Prentice-Hall, Englewood Cliffs, New Jersey, 1991.
[Holzmann95] G.Holzmann and D. Peled. An improvement in formal verification. In FORTE 1994: 197-211, 1995.
[Holzmann97] G.Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279-295, 1997.
[Holzmann04] G.Holzmann. The SPIN model checker: Primer and reference manual. HOL g 03:11.Ex., Addison Wesley, 2004.
[HuJ05] J. Hu, X. Yu, Y. Zhang, T. Zhang, X. Li, and G. Zheng. Checking component-based embedded software designs for scenario-based timing specifications. EUC 2005: 395-404, 2005.
[Inverardi95] P. Inverardi, A. Wolf. Formal specification and analysis of software architectures using the chemical abstract machine model. IEEE Transactions on Software Engineering, 21(4):373-386,1995.
[Jeffrey03] J. Jeffrey. E. Tsai, Y. Juan, and S. Avinash. Model and algorithm for efficient verification of high-assurance properties of real-Time systems. IEEE transactions on Knowledge and Data Engineering, 15(2), March/April 2003.
[JiaoWP06] W. Jiao, H. Mei. Automating integration of heterogeneous COTS components. ICSR 2006: 29-42,2006.
[JinXL05a] X. Jin, H. Ma. An approach to formally modeling the component-based e-commerce system. IEEE International Workshop on Service-Oriented System Engineering, Beijing, China, October 20-21, 2005.
[JinXL05b] X. Jin, H. Ma. Hierarchically modeling the component-based real-time system with duration calculus. The Fifth International Conference on Information, Communications and Signal Processing, Bangkok, Thailand, December 6-9, 2005.
[JinXL05c] X. Jin, H. Ma, and Z. Gu. Real-Time Component Composition using Hierarchical Timed Automata. Proc. International Conference on Quality Software (QSIC 2007), October 10-12,2007.
[JY02] 贾育,顾毓清．基于领域特征空间的构件语义表示方法．软件学报,13(2)：311-316,2002．
[Kang90] K. Kang, S. Cohen, J. Hess, W. Novak, A. Peterson. Feature-Oriented domain analysis (FODA) feasibility study. Technical Report, CMU/SEI-90-TR-21. Pittsburgh: Carnegie Mellon University, Software Engineering Institute: 1-52, 1990.
[Katz92] S. Katz and D. Peled. Verification of distributed programs using representative interleaving sequences. Distributed Computing, 6:107-120,1992.
[Kaynar03] D. Kaynar, N. Lynch, R. Segala, F. Vaandrager. Timed I/O automata: A mathematical framework for modeling and analyzing real-time systems. In: Kaynar DK, Lynch N, Segala R, Vaandrager F, eds. Proc, of the 24th IEEE Int'l Real-Time Systems Symp. Washington: 166-177, IEEE Computer Society, 2003.
[Krichen05] M. Krichen, S. Tripakis. State identification problems for timed automata. In: Khendek F, Dssouli R, eds. Proc, of the 17th IFIP Int'l Conf, on Testing of Communicating Systems (TestCom 2005). LNCS3502:175-191, Berlin: Springer-Verlag, 2005.
[Lamport94] L. Lamport. The temporal logic of actions. ACM Transactions on Programming Language and Systems, 16(3):872-923, 1994.
[Laroussinie98] F. Laroussinie and K. G. Larsen, CMC: A tool for compositional modelchecking of real-time systems. In Proc. IFIP Joint Int. Conf. Formal Description Techniques & Protocol Specification, Testing, and Verification (FORTE-PSTV'98): 439-456, Kluwer Academic Publishers, 1998.
[Larsen93] K. Larsen, Y. Wang. Time abstracted bisimiulation: Implicit specifications and decidability. In: Brookes SD, Main MG, Melton A, Mislove MW, Schmidt DA, eds. Proc, of the 9th Int'l Conf, on Mathematical Foundation of Programming Semantics. LNCS802:160-176, Berlin: Springer-Verlag, 1993.
[Larsen97]K.Larsen,P.Pettersson,and Y.Wang.Uppaal in a nutshell.Int.Journal on Software Tools for Technology Transfer,1(1-2):134-152,Oct.1997.
[Larsen05]K.Larsen,M.Mikucionis,and B.Nielsen.Online testing of real-time systems using uppaal.In:Grabowski J,Nielsen B,eds.Formal Approaches to Software Testing:4th Int'l Workshop.LNCS3395:79-94,Linz:Springer-Verlag,2005.
[LiCY06]李长云,李赣生,何频捷.一种形式化的动态体系结构描述语言.软件学报,17(6):1349-1359,2006.
[LinHM02]林惠民,张文辉.模型检测:理论、方法与应用.电子学报,30(12A):1907-1912.Dec.2002.
[LiuWM01]W.Liu,H.Ma.Modeling video-on-demand system in temporal logic.IEEE Pacific Rim Conference on Multimedia,2001.
[Luckham95]D.Luckham,J.Vera.An Event-Based Architecture Definition Language.IEEE Transactions on Software Engineering,21(9):717-734,1995.
[LuoHJ00]骆华俊,唐稚松.可视化体系结构描述语言XYZ/ADL.软件学报,11(8):1024-1029,2000.
[LvJ00]吕建,张鸣,廖宇,陶先平.基于移动Agent技术的构件软件框架研究.软件学报,11(8):1018-1023,2000.
[Magee95]J.Magee,N.Dulay,S.Eisenbach,and J.Kramer,Specifying distributed software architectures.In:Proc of the 5th European Software Engineering Conference(ESEC '95),LNCS989:137-153,Springer-Verlag,Sep.1995.
[MaH06]H.Ma,I.Yen,J.Zhou,and K.Coope.QoS analysis for component-based embedded software:Model and methodology.Journal of Systems and Software,79(6):859-870,2006.
[MaHD02]马华东,多媒体计算机技术原理(第2版).清华大学出版社,2002.
[Malte01]K.Malte.The future of m-payments-business option and policy issues.Background Paper No.2,Electronic payment Systems Observatory(ePSO),Aug.2001.
[Mandrioli95]D.Mandrioli,S.Morasca,and A.Morzenti.Generating test cases for real-time systems from logic specifications.ACM Transactions on Computer Systems,13(4):365-398,1995.
[McMillan92]K.McMillan.Symbolic model checking:An approach to the state explosion problem.Technical Report CMU-CS-92-131,Carnegie Mellon University,1992.
[Medvidovic96]N.Medvidovic,P.Orcizy,J.Robbins,and R.Taylor.Using object-oriented typing to support architectural design in the C2 style.In:D.Garlan,ed.Proceedings of the ACM SIGSOF7' 96:the 4th Symposium on the Foundations of Software Engineering:24-32,ACM Press,1996.
[Medvidovic00]N.Medvidovic,R.Taylor.A classification and comparison framework for software architecture description language.IEEE Transactions on Software Engineering,26(1):70-93,2000.
[MeiH02]H.Mei,L.Zhang,F.Yang.A component-based software configuration management model and its supporting system.Journal of Computer Science and Technology.17(4),July,2002.
[MeiH03]梅宏,陈锋,冯耀东,杨杰.ABC:基于体系结构、面向构件的软件开发方法.软件学报,14(4):721-732,2003.
[Milner98]R.Milner.Communication and concurrency.Prentice-Hall,1998.
[Milner99]R.Milner.Communicating and mobile systems:the Pi-calculus.Cambridge University Press,1999.
[Neema03]S.Neema,J.Sztipanovits,G.Karsai,and K.Butts.Constraint-based design-space exploration and model synthesis.In EMSOFT:290-305,2003.
[Moriconi95]M.Moriconi,X.Qian,and R.Riemenschneider.Correct architecture refinement.IEEE Transactions on Software Engineering,21(4):356-372,1995.
[Musuvathi04]M.Musuvathi and D.Engler.Model checking large network protocol implementations.In Proceedings of the 1st Symposium on networked Systems Design and Implementation:155-168.USENIX Association,2004.
[Narayanan02]S.Narayanan,S.Mcllraith.Simulation,verification and automated composition of web services.In:Proc.of the 11th Int'l Conf.on World Wide Web.New York:ACM Press,77-88.2002.
[Nouaary02]A.En-Nouaary,R.Dssouli,F.Khendek.Timed Wp-method:Testing real-time systems.IEEE Trans.on Software Engineering,28(11):1023-1038,2002.
[OCLE05]OCLE Tool,http://lci.cs.ubbcluj.ro/OCLE/index.htm.
[OMG03]Object Management Group:UML 2.00CL Specification.
[Owre98]S.Owre,J.Rushby,N.Shankar,and D.Stringer-Calvert.PVS:an experience report.In D,Huter,W.Stephan,P.Traverso,and M.Ullman,eds.,Applied Formal Methods-FM-Trends 98,LNCS 1641:338-345.Springer-Verlag,1998.
[PengX06]彭鑫,赵文耘,刘奕明.基于特征模型和构件语义的概念体系结构设计.软件学报,17(6):1307-1317,2006.
[Podgurski93]A.Podgurski,L.Pierce.Retrieving reusable software by sampling behavior.ACM Transactions on Software Engineering and Methodology,2(3):286-303,1993.
[QianZZ06]钱柱中,陆桑璐,谢立.基于Petri网的Web服务自动组合研究.计算机学报,29(7):1057-1066,2006.
[RenHM03]任洪敏,钱乐秋.构件组装及其形式化推导研究.软件学报,14(6):1066-1074,2003.
[RaoJ05]J.Rao,X.Su.A survey of automated Web service composition methods.In:Cardoso J,Sheth A,eds.Proc.of the SWSWPC 2004.LNCS3387:43-54,Berlin,Heidelberg:Springer-Verlag,2005.
[Schumann01]J.Schumann.Automated theorem proving in software engineering.Berlin Heidelerg:Springer-Verlag,2001.
[Sedigh05]S.Sedigh-Ali,A.Ghafoor.A graph-based model for component-based software development.In WORDS:254-262,2005.
[Sekerinski01]E.Sekerinski,K.Sere(eds).Program development by refinement(case studies using the B method).London:Springer-Verlag,2001.
[Shaw95] M. Shaw, R. DeLine, D. Klein, T. Ross, M. David and Y. Zelesnik. Abstractions for software architecture and tools to support them. IEEE Transactions on Software Engineering, Special Issue on software Architecture, 21(4): 314-335, 1995.
[Shaw96] M. Shaw, D. Garlan. Software Architecture: Perspectives on an Emerging Discipline. New Jersey: Prentice Hall, 1996.
[Sidhu89] D. Sidhu, T. Leung. Formal methods for protocol testing: A detailed study. IEEE Transactions on Software Engineering, 15(4): 413-426, 1989.
[SirinE04] E.Sirin, etc.. HTN planning for Web service composition using SHOP2. Journal of Web Semantics, l(4):377-396,2004.
[Sistla00] A. Sistla, V. Gyuris, and E. Allen. Smc: a symmetry-based model checker for verification of safety and liveness properties. ACM Transactions on Software Engineering Methodology, 9(2): 133-166,2000.
[Souza97] D. Souza and A. Wills.Objects, components and frameworks with UML - the catalysis approach. Addison-Wesley, 1997.
[Springintveld01] J. Springintveld, F. Vadranger, and P. Dargenio. Testing timed automata. Theoretical Computer Science, 254(1-2):225-257, 2001.
[Stahl99] K. Stahl, K. Baukus, Y. Lakhnech, and M. Steffen. Divide, abstract, and model-check. In SPIN: 57-76,1999.
[SunY03] Y. Sun, H. Ma. A component-based iterative software development model and the application. CNCC'2003, 2003.
[Szypersky98] C. Szypersky. Component software beyond object-oriented programming, Addison-Wesley, ACM Press, New York, 1998.
[Szypersky02] C. Szypersky, D. Gruntz, S. Murer. Component software: Beyond object-oriented programming. 2nd. Massachusetts: Addison-Wesley Professional, 2002.
[Tretmans02] J. Tretmans. Testing techniques. Lecture notes, University of Twente, The Netherlands, 2002.
[Tripakis96] S. Tripakis, C. Courcoubetis. Extending Promela and Spin for real time, Proceedings of TACAS '96, LNCS1055, 1996.
[Tripakis01] S. Tripakis, S. Yovine. Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design, 18(1):25-68, 2001.
[Vallecillo00] A. Vallecillo, J. Hernandez, and J. Troya. New issues in object interoperability. In Proc, of the ECOOP 2000 Workshop on Object Interoperability. LNCS 1964:256-269, France, 2000.
[Wandeler06] E. Wandeler and L. Thiele: Interface-based design of real-time systems with hierarchical scheduling. In IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS): 243-252, 2006.
[WangJZ00] J. Wang, Q. Xu, and H. Ma. Modeling and verification of a network player system with DCValid. First Asia-Pacific Conference on Quality Software, 30-31 Oct. 2000.
[Warmer03] J. Warmer, A. Kleppe. The object constraint language: Getting your models ready for MDA. Second Edition, Addison-Wesley, 2003.
[WangXG04]王晓光,冯耀东,梅宏.ABC/ADL:一种基于XML的软件体系结构描述语言.计算机研究与发展,第9期,2004.
[WangYF02]王渊峰,张涌,任洪敏等,基于刻面描述的构件检索.软件学报,13(8):1546-1551,2002.
[WangF00]F.Wang.Region encoding diagram for fully symbolic verification of real-time systems.In Proc.of 24th International Computer Software and Applications Conference:509-515,Berlin,Germany,March 2000.
[WangF05]F.Wang.Symbolic parametric safety analysis of linear hybrid systems with BDD-Like data-structures.IEEE Transactions on Software Engineering,31(1):38-51,Jan.2005.
[Wing90]J.Wing.A specifier's introduction to formal methods.IEEE Computer,23(9):8-24,1990.
[Wozna02]B.Wozna,W.Penczek,and A.Zbrzezny.Reachiability for timed systems based on SAT-solvers.In Proc.of the Int.Workshop on Concurrency,Specification and Programming(CS&P'02),Informatik-Berichte,161(2):380-395,Humboldt University,2002.
[Yovine97]S.Yovine.KRONOS:A verification tool for real-time systems.Springer International Journal of Software Tools for Technology Transfer,1(1/2):123-133,1997.
[Zaremski96]A.Zaremski.Signature and specification matching:[Ph.D,dissertation].School of Computer Science Carnegie Mellon University,1996.
[ZengL04]L.Zeng etc..QoS-Aware middleware for Web services composition.IEEE Transactions on Software Engineering,30(5):311-327,2004.
[ZhangJC00]张家晨,冯铁,陈伟,金淳兆.基于主动连接件的软件体系结构及其描述方法.软件学报,11(8):1047-1052,2000.
[ZhangSK02]张世琨,王立福,杨芙清.基于层次消息总线的软件体系结构风格.中国科学(E辑),32(3):393-400,2002.
[ZhangWH95]W.Zhang.Verification of XYZ/SE Programs.Chinese J.of Adv.Software Research,April 1995.
[ZhuXY03]朱雪阳,唐稚松.基于时序逻辑的软件体系结构描述语言XYZ/ADL.软件学报,14(4):731-720,2003.