网络式软件的语义过程模型及其验证技术研究
|
摘要
随着互联网技术的发展和普及,社会对于软件的形态和开发过程提出了更高的要求,如各种业务应用的快速集成,业务系统的良好适应性及可复用性等。为了满足这种要求,一种面向服务(Service-Oriented)的软件形态正在来临。网络式软件作为一种为了顺应这种新要求而涌现的软件新形态,具有网络化和服务化的特点,集中体现了“软件即服务(Software as a service SaaS)"的核心思想。网络式软件的开发呈现了“用户主导,面向领域,柔性生产”的模式特点,其中,领域的可复用的共性资产是实现网络式软件敏捷开发和满足用户个性化和多元化目标的重要基础。
网络式软件的领域建模是构建应用领域可复用的共性资产的过程。O-RGPS元建模框架为网络式软件的领域建模提供了建模视角及其之间的元关系。在元建模框架的指导下,领域建模构建了应用领域中的本体(O)资产,角色(R)资产,目标(G)资产,过程(P)资产,及服务(S)资产。这些不同视角的资产并非完全正交和独立的,而是呈现多层次、多粒度、且在语义层面上相互耦合。为了有利于这些语义丰富且相互耦合的领域资产的复用、规约、分析与管理,提出一个合适的资产组织框架来有效地组织这些不同视角的资产是十分必要的。
作为O-RGPS元建模框架的深入性基础研究,本文主要关注于领域资产的组织结构、描述及资产间一致性问题的分析和验证。因此,本文拟解决的科学问题为“基于元建模框架O-RGPS,针对语义丰富且耦合的领域资产,如何有效地组织这些不同视角的领域资产,使其能够被正确的复用和管理”。围绕着该科学问题,本文的贡献主要体现在以下几个方面：
(1)基于O-RGPS元建模框架,提出了一个以过程模型为核心的形式化的资产组织框架RGPS-SPM(Semantic Process Model),称之为语义过程模型框架。以过程模型为核心的资产组织方式顺应了当前业务过程模型在面向服务计算和面向服务的软件开发中越来越重要的趋势。以过程模型为基点,组合与其语义上强耦合的角色模型、目标模型等资产,从而结构化和模块化的形成以过程模型为核心的语义上高内聚、低耦合的、更大粒度的可复用的组合模型(称之为语义过程模型)。基于多类型谓词逻辑(Many-sorted Predicate Logic)及并发事务逻辑(Concurrent TRansaction logic, CTR),给出了语义过程模型的形式定义,及其内部的角色模型、目标模型及过程模型的形式定义。
(2)给出了语义过程模型的模型语义(Model Semantics),基于该模型语义,定义了语义过程模型的一致性公理。语义过程模型作为以过程模型为核心,封装与过程模型在语义上强耦合的角色模型、目标模型的复合模型,其内部的一致性是实现领域资产正确复用的重要前提。给出了语义过程模型的模型语义。基于该模型语义,定义了语义过程模型关于模型间静态语义的一致性公理。
(3)基于语义过程模型的模型语义和形式定义,定义了语义过程模型的形式化规约语言SPML(Semantic Process Modeling Language)。O-RGPS元建模框架为领域资产的建模提供了建模视角和视角之间的元关系。然而当前并没有相应的具有足够描述能力的资产规约语言。基于语义过程模型框架,并借鉴语义Web建模语言WSML(Web Service Modeling Language)和OWL-S的特点,定义了语义过程模型的规约语言SPML,该语言可以对O-RGPS框架中各模型(不包括服务模型)进行规约。
(4)基于语义过程模型的模型语义,针对目标模型相对于过程模型的可实现性(Realizable)问题,定义了两类验证问题并提出了相应的验证方法。基于语义过程模型的模型语义,给出了目标模型相对于过程模型的可实现性定义。并给出了目标模型相对过程模型的可实现性判定定理。根据该定理,定义了两类关于目标模型相对于过程模型的可实现性的验证问题,即语义过程模型的约束验证和语义过程模型的能力一致性验证问题。一方面,约束验证是过程模型是否满足数据流和目标模型关于过程执行的时序约束；借助进程代数CSP(Communicating Sequence Processes)及其工具FDR2,提出了语义过程模型的约束验证方法。另一方面,能力一致性验证是过程模型的实际执行能力是否同过程模型的能力模型和目标模型对过程模型的能力期望是否相一致。借助谓词抽象技术(Prediate Abstraction)和可满足性求解工具SAT solver,提出了能力一致性的验证方法。
简言之,本文主要是在O-RGPS元建模框架下关于领域资产的组织结构、描述、和一致性分析与验证方面作了一定的贡献,为RGPS元建模框架的更深入应用奠定基础。
With the Internet technique development and prevalence, our society today requires higher level on the form as well as development process of software than ever before, e.g., agile and seamless integration of various businesses, high flexibility and reusability of business software system, etc. To battle for these requirements, service-oriented software as a new form appears recently. Networked software is one of such software, which is of service-oriented and networked, and embodies the principle of "Software as a Service(SaaS)". The development lifecycle of networked software is a kind of process which is user-centric, domain-oriented, and flexible. During the lifecycle of networked software development, the reusable and common domain assets play the important role for its agility and satisfying the client goals of personalized and diverse.
The domain modeling of networked software is a process of creating the reusable and common assets of application domain. The meta-modeling framework O-RGPS provides the dimensions of domain modeling as well as the meta-interrelations among them. Under the guide of the meta-modeling framework, domain modeling needs to create the domain ontology, role model assets, goal model assets, process model assets, and service assets in the application domain. These assets of different dimensions are not totally orthogonal and independent, but of multi-level, various granularity, and interconnected in the underlying semantics. As for facilitating reuse, specifying, analysis, and managing these domain assets, it is by no means trivial to propose a proper assets organization framework to efficiently organize these various dimension assets.
As a further study of the meta-modeling framework O-RGPS, this thesis focuses on the organization structure, the description, and the consistency analysis and verification of domain assets. Therefore, the scientific problem studied in the thesis is, based on the meta-modeling framework O-RGPS, how to efficiently organize the domain assets to facilitate them to be correctly reuse and managed..Considering the scientific problem, the main contributions of thesis are summarized as follows::
(1) Based on O-RGPS meta-modeling framework, a process-centric formal framework for organizing assets, named RGPS-SPM, is proposed. It is also called semantic process model framework. This process-centric feature is corresponded to the increasingly important role of process model in service-oriented computing and service-oriented software development. Starting from process model, by combing its strongly semantic-coupled role model and goal model assets, a more granular composite model, named semantic process model, is synthesized structurally and modularly, which is of high inner related and lower inter coupled. Based on many-sorted predicate logic and concurrent transaction logic CTR, the semantic process model and its inner models are defined formally.
(2) The model semantics of semantic process model is defined and, based on the model semantics, the consistency axioms of semantic process model is also presented. The semantic process model is process-centric and encapsulates the semantically related role model and goal model. The consistency of semantic process model is the prerequisite for correct reusing domain assets.
(3) Based on the formal definition and model semantics of semantic process model, a specification language for modeling semantic process model is proposed and named as SPML. Up to now, there are few languages with enough expressive power to specify domain assets under the meta-framework O-RGPS. Based on the model semantics of semantic process model, a formal specification language SPML is proposed by referring the good feature of web service modeling languages WSML and OWL-S. SPML can specify various assets except service assets under the O-RGPS framework.
(4) To address the realizable problem between goal model and process model, two sorts of verification problems and their solution are accordingly defined and proposed. Based on the model semantics of semantic process model, the realizability between goal model and process model is defined and the theorem to decide the realizability is also proposed accordingly. Based on the theorem, two sort of verification problem is defined, i.e., the constraints verification and capability compliance verification. On the one hand, the constraint verification problem concerns whether the process model satisfies the constraints about process execution temporal order imposed by dataflow and goal model. By making use of process algebra CSP(Communicating Sequence Processes) and the tool FDR2, the procedure for constraint verification is proposed; on the other hand, the capability compliance verification concern the consistency between the process actual capability and its capability model as well as capability expectation from goal model. Motivated by predicate abstraction technique and making use of SAT solver, the verification method to solve the capability compliance is proposed.
In summary, the thesis, under the O-RGPS meta-modeling framework, has made positive contributions to the organization structure, description, and consistency analysis and verification for domain assets, and paved the way for further applications of RGPS metamodeling frameowrk.
网络式软件的领域建模是构建应用领域可复用的共性资产的过程。O-RGPS元建模框架为网络式软件的领域建模提供了建模视角及其之间的元关系。在元建模框架的指导下,领域建模构建了应用领域中的本体(O)资产,角色(R)资产,目标(G)资产,过程(P)资产,及服务(S)资产。这些不同视角的资产并非完全正交和独立的,而是呈现多层次、多粒度、且在语义层面上相互耦合。为了有利于这些语义丰富且相互耦合的领域资产的复用、规约、分析与管理,提出一个合适的资产组织框架来有效地组织这些不同视角的资产是十分必要的。
作为O-RGPS元建模框架的深入性基础研究,本文主要关注于领域资产的组织结构、描述及资产间一致性问题的分析和验证。因此,本文拟解决的科学问题为“基于元建模框架O-RGPS,针对语义丰富且耦合的领域资产,如何有效地组织这些不同视角的领域资产,使其能够被正确的复用和管理”。围绕着该科学问题,本文的贡献主要体现在以下几个方面：
(1)基于O-RGPS元建模框架,提出了一个以过程模型为核心的形式化的资产组织框架RGPS-SPM(Semantic Process Model),称之为语义过程模型框架。以过程模型为核心的资产组织方式顺应了当前业务过程模型在面向服务计算和面向服务的软件开发中越来越重要的趋势。以过程模型为基点,组合与其语义上强耦合的角色模型、目标模型等资产,从而结构化和模块化的形成以过程模型为核心的语义上高内聚、低耦合的、更大粒度的可复用的组合模型(称之为语义过程模型)。基于多类型谓词逻辑(Many-sorted Predicate Logic)及并发事务逻辑(Concurrent TRansaction logic, CTR),给出了语义过程模型的形式定义,及其内部的角色模型、目标模型及过程模型的形式定义。
(2)给出了语义过程模型的模型语义(Model Semantics),基于该模型语义,定义了语义过程模型的一致性公理。语义过程模型作为以过程模型为核心,封装与过程模型在语义上强耦合的角色模型、目标模型的复合模型,其内部的一致性是实现领域资产正确复用的重要前提。给出了语义过程模型的模型语义。基于该模型语义,定义了语义过程模型关于模型间静态语义的一致性公理。
(3)基于语义过程模型的模型语义和形式定义,定义了语义过程模型的形式化规约语言SPML(Semantic Process Modeling Language)。O-RGPS元建模框架为领域资产的建模提供了建模视角和视角之间的元关系。然而当前并没有相应的具有足够描述能力的资产规约语言。基于语义过程模型框架,并借鉴语义Web建模语言WSML(Web Service Modeling Language)和OWL-S的特点,定义了语义过程模型的规约语言SPML,该语言可以对O-RGPS框架中各模型(不包括服务模型)进行规约。
(4)基于语义过程模型的模型语义,针对目标模型相对于过程模型的可实现性(Realizable)问题,定义了两类验证问题并提出了相应的验证方法。基于语义过程模型的模型语义,给出了目标模型相对于过程模型的可实现性定义。并给出了目标模型相对过程模型的可实现性判定定理。根据该定理,定义了两类关于目标模型相对于过程模型的可实现性的验证问题,即语义过程模型的约束验证和语义过程模型的能力一致性验证问题。一方面,约束验证是过程模型是否满足数据流和目标模型关于过程执行的时序约束；借助进程代数CSP(Communicating Sequence Processes)及其工具FDR2,提出了语义过程模型的约束验证方法。另一方面,能力一致性验证是过程模型的实际执行能力是否同过程模型的能力模型和目标模型对过程模型的能力期望是否相一致。借助谓词抽象技术(Prediate Abstraction)和可满足性求解工具SAT solver,提出了能力一致性的验证方法。
简言之,本文主要是在O-RGPS元建模框架下关于领域资产的组织结构、描述、和一致性分析与验证方面作了一定的贡献,为RGPS元建模框架的更深入应用奠定基础。
With the Internet technique development and prevalence, our society today requires higher level on the form as well as development process of software than ever before, e.g., agile and seamless integration of various businesses, high flexibility and reusability of business software system, etc. To battle for these requirements, service-oriented software as a new form appears recently. Networked software is one of such software, which is of service-oriented and networked, and embodies the principle of "Software as a Service(SaaS)". The development lifecycle of networked software is a kind of process which is user-centric, domain-oriented, and flexible. During the lifecycle of networked software development, the reusable and common domain assets play the important role for its agility and satisfying the client goals of personalized and diverse.
The domain modeling of networked software is a process of creating the reusable and common assets of application domain. The meta-modeling framework O-RGPS provides the dimensions of domain modeling as well as the meta-interrelations among them. Under the guide of the meta-modeling framework, domain modeling needs to create the domain ontology, role model assets, goal model assets, process model assets, and service assets in the application domain. These assets of different dimensions are not totally orthogonal and independent, but of multi-level, various granularity, and interconnected in the underlying semantics. As for facilitating reuse, specifying, analysis, and managing these domain assets, it is by no means trivial to propose a proper assets organization framework to efficiently organize these various dimension assets.
As a further study of the meta-modeling framework O-RGPS, this thesis focuses on the organization structure, the description, and the consistency analysis and verification of domain assets. Therefore, the scientific problem studied in the thesis is, based on the meta-modeling framework O-RGPS, how to efficiently organize the domain assets to facilitate them to be correctly reuse and managed..Considering the scientific problem, the main contributions of thesis are summarized as follows::
(1) Based on O-RGPS meta-modeling framework, a process-centric formal framework for organizing assets, named RGPS-SPM, is proposed. It is also called semantic process model framework. This process-centric feature is corresponded to the increasingly important role of process model in service-oriented computing and service-oriented software development. Starting from process model, by combing its strongly semantic-coupled role model and goal model assets, a more granular composite model, named semantic process model, is synthesized structurally and modularly, which is of high inner related and lower inter coupled. Based on many-sorted predicate logic and concurrent transaction logic CTR, the semantic process model and its inner models are defined formally.
(2) The model semantics of semantic process model is defined and, based on the model semantics, the consistency axioms of semantic process model is also presented. The semantic process model is process-centric and encapsulates the semantically related role model and goal model. The consistency of semantic process model is the prerequisite for correct reusing domain assets.
(3) Based on the formal definition and model semantics of semantic process model, a specification language for modeling semantic process model is proposed and named as SPML. Up to now, there are few languages with enough expressive power to specify domain assets under the meta-framework O-RGPS. Based on the model semantics of semantic process model, a formal specification language SPML is proposed by referring the good feature of web service modeling languages WSML and OWL-S. SPML can specify various assets except service assets under the O-RGPS framework.
(4) To address the realizable problem between goal model and process model, two sorts of verification problems and their solution are accordingly defined and proposed. Based on the model semantics of semantic process model, the realizability between goal model and process model is defined and the theorem to decide the realizability is also proposed accordingly. Based on the theorem, two sort of verification problem is defined, i.e., the constraints verification and capability compliance verification. On the one hand, the constraint verification problem concerns whether the process model satisfies the constraints about process execution temporal order imposed by dataflow and goal model. By making use of process algebra CSP(Communicating Sequence Processes) and the tool FDR2, the procedure for constraint verification is proposed; on the other hand, the capability compliance verification concern the consistency between the process actual capability and its capability model as well as capability expectation from goal model. Motivated by predicate abstraction technique and making use of SAT solver, the verification method to solve the capability compliance is proposed.
In summary, the thesis, under the O-RGPS meta-modeling framework, has made positive contributions to the organization structure, description, and consistency analysis and verification for domain assets, and paved the way for further applications of RGPS metamodeling frameowrk.
引文
[1]何克清,彭蓉,王健等著,“网络式软件”,北京：科学出版社,2008..
[2]M. Turner, D. Budgen, and P. Brereton, "Turning Software into a Service", IEEE Computer, 36(10),2003, pp.38-44.
[3]王健,“网络式软件的需求元建模框架及关键技术研究”,武汉大学,博士论文,2008.
[4]M. N. Huhns and M. P. Singh, "Service-oriented Computing:Key Concepts and Principles", IEEE Internet Computing, Vol.1-2,2005, pp.2-8.
[5]M. Turner, D. Budgen, P. Brereton, "Turning software into a service", Computer,Vol 36, Issue 10,2003:38-44.
[6]K. He, R. Peng, J. Liu, F. He, et al, "Design methodology of Networked Software Evolution Growth based on Software Patterns", Journal of System Science and Complexity, Vol.19, 2006, pp.157-181.
[7]K. He, P. Liang, R. Peng, et al, "Requirement Emergence Computation of Networked Software", Frontiers of Computer Science in China,1(3),2007, pp.322-328.
[8]W3C, "Web Services Architecture",2003. Available:http://www.w3c.org/TR/ws-arch/.
[9]岳昆,王晓玲,周傲英,“Web服务核心支撑技术：研究综述”,软件学报,2004,15(3)：428-442.
[10]I. Foster, C. Kesselman, "The Grid:Blueprint for a New Computing Infrastructure", Morgan Kaufmann Publishers,1998.
[11]A. Oram, "Peer-to-Peer:Harnessing the Power of Disruptive Technologies", ORei-lly& Associates,2001.
[12]J. Wang, K. He, P. Gong, et al, "RGPS:A Unified Requirements Meta-Modeling Frame for Networked Software", In Proc. of Third International Workshop on Advances and Applications of Problem Frames(IWAAPF'08) at 30th International Conference on Software Engineering(ICSE'08), Leipzig, Germany, May 2008.
[13]J. Wang, K. He, B. Li, et al, "Meta-models of Domain Modeling Framework for Networked Software", In Proc. of The Sixth International Conference on Grid and Cooperative Computing (GCC 2007), Urumchi, China, August 2007, pp.878-885.
[14]Z. Feng, K. He, Y. Ma, et al, "Towards Individualized Requirements Specification Evolution for Networked Software Based on Aspect", ICSP 2008, LNCS 5007, pp.88-99.
[15]I. Sommerville, P. Sawyer, "Requirement Engineering:A Good Practice Guide", John Wiley&Sons, Inc., New York, US,1997.
[16]P, Zave, M, Jackson, "Four Dark Corners of Requirements Engineering", ACM Transaction on Software Engineering and Methodology,1997,6(1), pp.1-30.
[17]M. Dorfman, R. H. Thayer, "Standards, Guidelines, and Examples on System and Software Requirements Engineering", IEEE Computer Society Press Tutorial,1990.
[18]卢梅,李明树,“软件需求工程-方法及工具评述”,计算机研究与发展,36(11),pp.1289-1300.
[19]刘玮,“面向服务的软件需求获取与分析研究”,武汉大学,博士论文,2008.
[20]K. C. Kang, S. Cohen, J. Hess, et al, "Feature-Oriented Domain Analysis (FODA):Feasibility Study", Technical Report CMU/SEI-90-TR-021, Software Engineering Institute, Carnegie Mellon University,1990.
[21]张伟,梅宏,“一种面向特征的领域模型及其建模过程”,软件学报,2003,14(8)：1345-1356.
[22]I. Jacobson, M. L. Griss, P. Jonsson, "Software Reuse:Architecture, Process and Organization for Business Success", Addison-Wesley Publishing, New York,1997.
[23]M. L. Griss, J. Favaro, M. d'Alessandro, "Integrating Feature Modeling with the RSEB", In Proc. of the 15th International Conference on Software Reuse,1998, IEEE, pp.76-85.
[24]G Chastek, P. Donohoe, K. C. Kang, et al. "Product Line Analysis:a Practical Introduction". Technical Report, CMU/DEI-2001-TR-01, Carnegie Mellon University, Software Engineering Institute.
[25]SEI, "Domain Engineering", Carnegie Mellon University,2004, Available: http://www.sei.cmu.edu/domain-engineering/domain eng.html.
[26]Olaf Zimmermann, P. K., Clive Gee. (2004). "Elements of Service-Oriented Analysis and Design." Available:http://www.ibm.com/developerworks/webservices/library/ws-soadl/
[27]N. Busi, R. Gorrieri, C. Guidi, R. Lucchi, and G. Zavattaro, "Choreography and Orchestration:A Synergic Approach for System Design". ICSOC 2005, LNCS 3826 pp. 228-240.
[28]M. A. Simos, "Organization Domain Modeling(ODM):Formalizing the Core Domain Modeling Life Cycle", In Proc. of the Symposium on Software Reusability, ACM Press, Washington,1995, pp.196-205.
[29]K. C. Kang, S. Kim, J. Lee, et al. "FORM:A Feature-oriented Reuse Method with Domain-specific Reference Architectures", Annals of Software Engineering,5(1998), pp. 143-168.
[30]M. Harsu, "FAST Product-line Architecture Process", Report 29, Institute of Software Systems, Tampere University of Technology, January 2002, Available: http://practise2.cs.tut.fi/pub/.
[31]CORDET, "Domain Engineering Methodologies Survey", Report GMV-CORDET-WP202-RP-001,2007, Available: www.pnp-software.com/cordet/download/pdf/GMV-CORDET-RP-001 Issl.pdf..
[32]P. Loucopoulos and E. Kavakli, "Enterprise Modeling and the Teleological Approach to Requirements Engineering", International Journal of Intelligent and Cooperative Information Systems,4(1),1995, pp.45-79.
[33]B. Nuseibeh, J. Kramer, and A. Finkelstein, "A Framework for Expressing the Relationships between Multiple Views in Requirements Specification", IEEE Transaction on Software Engineering,20(10),1994, pp.760-773.
[34]A. V. Lamsweerde, "Goal-oriented Requirements Engineering:a Guided Tour", In Proc. of the 5th IEEE International Symposium on Requirements Engineering, Toronto, Canada,2001, pp.249-263.
[35]E. Yu, "Modeling Strategic Relationships for Process Reengineering", PhD thesis, Department of computer science, University of Toronto,1994.
[36]J. Castro, M. Kolp, and J. Mylopoulos, "Towards Requirements-Driven Software Development Methodology:The Tropos Project", Information Systems, Vol.27,2002, pp. 365-389.
[37]A. V. Lamsweerde and E. Letier, "From Object Orientation to Goal Orientation:a Paradigm Shift for Requirements Engineering", Radical Innovations of Software and Systems Engineering in the Future,2004, pp.325-340.
[38]J. Mylopoulos, L. Chung and E. Yu, "From Object-Oriented to Goal-Oriented Requirements Analysis", Communications of the ACM,42(1), Jan.1999, pp.31-37.
[39]R. A. Falbo, G Guizzardi and K. C. Duarte, "An Ontological Approach to Domain Engineering", In Proc. of the International Conference on Software Engineering and Knowledge Engineering (SEKE'02), Ischia, Italy,2002, pp.351-358.
[40]金芝,陆汝钤,“多范例自动需求建模和分析：一种基于本体的方法”,中国科学(E辑),2003,33(4)：297-312.
[41]金芝,“基于本体的需求自动获取”,计算机学报,2000,23(5)：486-492.
[42]陆汝钤,金芝,陈刚,“面向本体的需求分析”,软件学报,2000,11(8)：1009-1017.
[43]W. M. P. van der Aalst, F. L., W. Reisig (2007). "The Role of Businesses in Service Oriented Architectures." Business Process Integration and Management 2(2007):75-80.
[44]J. Barjis,,"The importance of business process modeling in software systems design." Science of Computer Programming,2008,71:73-87.
[45]J. Cardoso, R. P. B., A. Sheth, "Workflow Management Systems and ERP Systems: Differences, Commonalities, and Applications." Information Technology and Management, 2004 (5):319-338.
[46]W. M. P. van der Aalst, K. M. v. H. "Workflow Management:Models, Methods, and Systems", MIT press, Cambridge, MA,2002.
[47]H. Smith, P. F., "Business Process Management-The Third Wave", Meghan-Kiffer Press, 2002.
[48]W. M. P. van der Aalst, A.H.M.ter Hofstede,, and M. Weske,.. "Business Process Management:A Survey", BPM2003, Springer-Verlag Berlin Heidelberg, LNCS2678, pp.1-12.
[49]W. M. P. van. der Aalst, "Business Process Management Demystified:A Tutorial on Models, Systems and Standards for Workflow Management". ACPN2004, LNCS3098, pp.1-60.
[50]F. Leymann, D. R., M. T. Schmidt "Web Services and Business Process Management." IBM Systems,2002,41(2):198-211.
[51]T. Woodley and S. Gagnon., "BPM and SOA:Synergies and Challenges", WISE'05, Springer-Verlag Berlin Heidelberg,2005, LNCS3806, pp.679-688.
[52]H. Schonenberg, R. M., N. Russell, W. M.P. van der Aalst (2008). "Process Flexibility:A Survey of Contemporary Approaches".4th International Workshop CIAO in CAiSE. Lecture Note in Information Processing,8, pp.16-30.
[53]W. M.P. van der Aalst, M. W., Dolf Grunbauer. "Case handling:a new paradigm for business process support." Data & knowledge Engineering(53),2005, pp.129-162.
[54]W. M. P. van der Aalst,., M. Pesic, "DecSerFlow:Towards a Truly Declarative Service Flow Language". WS-FM 2006, LNCS 4184, pp.1-23.
[55]Business Process Execution Language for Web Services version 1.1,2007, Available: http://www.ibm.com/developerworks/library/specification/ws-bpel/.
[56]M. Pesic, M. N. s., N.Sidorova, and W.M.P. van der Aalst. "Constraint-Based Workflow Models:Change Made Easy", OTM2007, LNCS 4803, pp 77-94.
[57]Martin Hepp, F. L., Chris Bussler, John Domingue, Alexander Wahler, et al. "Semantic Business Process Management:Using Semantic Web Services for Business Process Management", ICEBE 2005, IEEE, pp.535-540.
[58]Carlos Pedrinaci, J. D., Christian Brelage, et al., (2008). "Semantic Business Process Management:Scaling up the Management of Business Processes", IEEE International Conference on Semantic Computing, IEEE computer society,2008.
[59]I. Weber, J. H., Jan Mendling, and J. Nitzsche (2007). "Towards a Methodology for Semantic Business Process Modeling and Configuration", ICSOC Workshops 2007, pp.176-187.
[60]C.T. Jensen, I. Charters, J. Amasden, et al.,,"Leveraging SOA, BPM, and EA for Strategic Business and IT Alignment",2008, Available: http://www.ibm.com/developerworks/websphere/bpmjournal/0812_jensen/0812_jensen.html.
[61]Ivan Markovic, A. C. P, "Towards a Fromal Framework for Reuse in Business Process Modeling", BPM2007, LNCS 4928,2007, pp.484-495.
[62]Sudhir Agarwal, S. R., and Andreas Abecker, "Semantic Description of Distributed Business Processes". AAAI Spring Symposium-AI Meets Business Rules and Process Management, Stanford, USA,2008.
[63]吴步丹,金芝,赵彬,”面向服务的建模：一种全过程复用的方法.”计算机学报8(2008)：1293-1308.
[64]C. Pahl and M. Casey, "Ontology Support for Web Service Processes", In Proc.of 2003 European Software Engineering Conference and Foundations of Software Engineering (ESEC/FSE'03), ACM Press,2003, pp.208-216.
[65]S. McIlraith, T. C. Son, and H. Zeng, "Semantic Web Service", IEEE Intelligent Systems, 16(2),2001, pp.46-53.
[66]D. Martin, M. B., D. McDermott, et al.. "Bringing Semantics to Web Services with OWL-S." World Wide Web,2007,10:243-277.
[67]D. Martin, A.Ankolekar, M. Burstein, et al, "OWL-S:Semantic Markup for Web Services", W3C Candidate Recommendation,2004. Available:http://www.daml.org/services/owl-s/.
[68]D. Roman, J. d. Bruijn, A. Mocan, et al, "WWW:WSMO, WSML, and WSMX in a Nutshell", In Proc. of 1st Asian Semantic Web Conference (ASWC2006), Beijing, China, Sep.2006, pp.516-522.
[69]D. Roman, U. Keller, H. Lausen, et al, "Web Service Modeling Ontology", Applied Ontology Journal,1(1),2005, pp.77-106.
[70]J. de Bruijn, D16.3v1.0 WSML Abstract Syntax and Semantics,2008, Available: http://www.wsmo.org/TR/d16/d16.3/vl.0/.
[71]E. Borger, R. F. Stark, "Abstract State Machines:A Method for High-level System Design and Analysis", Springer,2003.
[72]A. J. Bonner, M. Kifer, "Transaction Logic Programming". ICLP 1993:257-279.
[73]A. J. Bonner, M. Kifer, "An Overview of Transaction Logic", Theor. Comput. Sci. 1994,133(2):205-265.
[74]A. J. Bonner, M. Kifer, "Concurrency and Communication in Transaction Logic". JICSLP 1996:142-156.
[75]P. van Eck, J. Engelfriet, D. Fensel, et al., "A Survey of Languages for Specifying Dynamics: A Knowledge Engineering Perspective", IEEE Transactions On Knowledge and Data Engineering,2001, vol 13, no.3, pp.462-496.
[76]H. Davulcu, M. Kifer, C. R. Ramakrishnan, I. V. Ramakrishnan:"Logic Based Modeling and Analysis of Workflows". In ACM Symposium on Principles of Database System,1998, pp. 25-33.
[77]H. Davulcu, M. Kifer., I.V. Ramakrishnan, " CTR-S:A Logic for Specifying Contracts in Semantic Web Services", WWW'04. New York, USA, ACM.
[78]D. Roman, M. Kifer, "Reasoning about the Behavior of Semantic Web Services with Concurrent Transaction Logic", VLDB 2007:627-638.
[79]D. Roman, M. Kifer, "Semantic Web Service Choreography:Contracting and Enactment', In Proc. of International Semantic Web Conference 2008:550-566.
[80]D. Roman, M. Kifer, D. Fensel, "WSMO Choreography:From Abstract State Machines to Concurrent Transaction Logic". ESWC 2008:659-673.
[81]A.W. Roscoe. "The Theory and Practice of Concurrency." Prentice-Hall,1997.
[82]E. Astesiano, M. Bidoit, H. Kirchner, et al. "CASL:the Common Algebraic Specification Language", Theoretical Computer Science,2002,286, pp.153-196.
[83]M. Bidoit, D. Sannella, A. Tarlecki, "Architectural Specifications in CASL", AMAST'98, LNCS 1548, pp.341-357.
[84]V. Dignum, "A Model for Organizational Interaction:Based on Agents, Founded in Logic" phD thesis,2004, Utrecht University.
[85]D. Grossi, F. Dignum, V. Dignum, et al., "Structural Aspects of the Evaluation of Agent Organizations", COIN 2006 Workshops, LNAI4386,2007, pp.3-18.
[86]A. Fuxman, L. Liu., M. Pistore,et al., "Specifying and analyzing early requirements:some experimental results." 11th IEEE International Requirements Engineering Conference(RE). 2003,pp.1-10.
[87]R. Milner, "Communicating and Mobile Systems:The Pi-Calculus", Cambridge University Press, Cambridge, UK,1999.
[88]王生原,余鹏,霍金健译,“系统工程Petri网：建模、验证与应用指南”,北京：电子工业出版社,2005.
[89]Y. Hirshfeld, M. Jerrum, "Bisimulation Equivalence Is Decidable for Normaed Process Algebra", ICALP'99, LNCS 1644, pp.412-421.
[90]Erhard Rahm, P. A. B. "A survey of approaches to automatic schema matching.", The VLDB Journal,2001, Vol.10:334-350.
[91]A. Oberschelp, "Order Sorted Predicate Logic", Sorts and Types in Artificial Intelligence, LNCS 418,1990, pp.7-17.
[92]G Booch, J. Rumbaugh and I. Jacobson, "The Unified Modeling Language User Guide", Addison-Wesley Longman, Inc,1999.
[93]E. M. Clarke, J. O. Grumberg, D. Peled, "Model Chekcing", MIT Press,2000.
[94]P. Haase, F. van Harmelen, Z. Huang, et al., "A Framework for Handing Inconsistency in Changing Ontologies", ISWC2005, LNCS 3729,2005, pp.353-367.
[95]K. Baclawski, M. M. Kokar, R. Waldinger, et al., "Consistency Checking of Semantic Web Ontologies", ISWC 2002, LNCS 2342,2002, pp.454-459.
[96]J. Davies, C. Crichton, "Concurrency and Refinement in the Unified Modeling Language", Fomal Aspects of Computing,2003,15, pp.118-145.
[97]M. Moller, E. R. Olderog, H. Rasch et al., "Integrating a formal method into a software engineering process with UML and Java." Formal Aspect Computing, Vol 20, pp.164-204, 2008.
[98]G. Smith. "The Object-Z Specification Language." Kluwer Academic Publisher,2000.
[99]C. Fischer and H. Wehrheim. "Model-checking CSPOZ specifications with FDR". In K. Araki, A. Galloway.and K. Taguchi, editors, Integrated Formal Methods, pp.315-334. Springer,1999.
[100]E. Yu. "Towards modeling and reasoning support for early requirements enginnering", In:Proceedings of the IEEE international symposium on requirement engineering. IEEE Computer Society, Washington, DC,,1997, pp.226-235.
[101]C. Ponsard, P. Massonet, A. Rifaut, A. van Lamsweerde and J. F. Molderez, "Early Verificatioin and Validation of Mission Critical System", Electronic Notes in Theoretical Computer Science,133,2005, pp.237-254.
[102]A. Fuxman, L. Liu, J. Mylopoulos, M. Pistore, M. Roveri and P. Traverso, "Specifying and analyzing early requirements in Tropos", Requirements Eng.,2004,9, pp.132-150.
[103]A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri. "NuSMV:a New Symbolic Model Checker". International Journal on Software Tools for Technology Transfer (STTT),2(4), 2000.
[104]D. Jackson, "Alloy:a lightweight object modeling notation", ACM Tran. Software Engineering Meth,2002,11:256-290.
[105]C. Heitmeyer, J. Kirby and B. Labaw, "The SCR method for formally specifying, verifying, and validating requirements:tool support", In:Proceedings of the 19th international conference on software engineering, ACM,1997, pp 610-611.
[106]Y. Choi, M. P. E, Heimdahl, "Model checking RSML-e requirements", In:Proceedings of the 7th IEEE international symposium on high assurance systems engineering, Tokyo, October 2002, IEEE Computer Socety, pp109-119.
[107]Franck van Breugel and Maria Koshkina, "Models and Verification of BEPL",2006, Available:www.cse.yorku.ca/-franck/research/drafts/tutorial.pdf.
[108]P, Gong. "Dynamic semantics of OWL-S in CSP-OZ". In 8th International Conference on Application of Concurrency to System Design, ACSD,2008, IEEE Press, pp.208-213.
[109]S. Graf, H. Saidi, "Construction of Abstract State Graphs with PVS", In O. Grumberg, Editor, Proc. of International Conference on Computer Aided Verfication(CAV'97), LNCS 1254,1997, pp.72-83.
[110]E. M. Clarke, D. Kroening, N. Sharygina, K. Yorav, "Predicate Abstraction of ANSI-C Programs Using SAT", Formal Methods in System Design,2004,25(2-3), pp.105-127.
[111]W. Sadiq, M. E. Orlowska, "Analyzing Process Models Using Graph Reducation Techniques", Inf. Syst.2000,25(2), pp.117-134.
[112]P. Soffer, Y. Wand, M. Kaner,"Semantic Analysis of Flow Patterns in Business Process Modeling", In G Alonso, P. Dadam, and M. Rosemann(Eds) BPM2007, LNCS 4714,2007, pp. 400-407.
[113]U. Keller, H. Lausen, M. Stollberg, "On the Semantics of Functional Descriptions of Web Services", In Y. Sure, J. Domingue(Eds) ESWC 2006, LNCS 4011,2006, pp.605-619.
[114]P. Gong, K. Q. He. "On the Capability Compliance of Annotated Process Model". In Proc. of 8th IEEE/ACIS International Conference on Computer and Information Science(ICIS'09), Shanghai China,2009, IEEE CS.
[115]Ly Linnh Thao, S. Rinderle,.P. Dadam, "Semantic Correctness in Adaptive Process Management Systems", In BPM2006 Workshops, LNCS 4102,2006, pp.193-208.
[116]G. Kolidis,. A. Ghose, "Verifying Semantic Business Process Modelsin Inter-operation", In Proceeding of International Conference on Services Computing(SCC), IEEE CS,2007.
[117]H. Meyer,"Calculating the Semantic Conformance of Processes", In BPM Workshops 2007, LNCS 4928,2008, pp.473-483.
[118]I. Weber,., J. Hoffmann,J. Mendling, "Beyond Soundness:On theSemantic Consisitency of Executable Proces Models", In Proceeding ofSixth European Conderence on Web Services, pp.102-111, IEEE CS,2008.
[2]M. Turner, D. Budgen, and P. Brereton, "Turning Software into a Service", IEEE Computer, 36(10),2003, pp.38-44.
[3]王健,“网络式软件的需求元建模框架及关键技术研究”,武汉大学,博士论文,2008.
[4]M. N. Huhns and M. P. Singh, "Service-oriented Computing:Key Concepts and Principles", IEEE Internet Computing, Vol.1-2,2005, pp.2-8.
[5]M. Turner, D. Budgen, P. Brereton, "Turning software into a service", Computer,Vol 36, Issue 10,2003:38-44.
[6]K. He, R. Peng, J. Liu, F. He, et al, "Design methodology of Networked Software Evolution Growth based on Software Patterns", Journal of System Science and Complexity, Vol.19, 2006, pp.157-181.
[7]K. He, P. Liang, R. Peng, et al, "Requirement Emergence Computation of Networked Software", Frontiers of Computer Science in China,1(3),2007, pp.322-328.
[8]W3C, "Web Services Architecture",2003. Available:http://www.w3c.org/TR/ws-arch/.
[9]岳昆,王晓玲,周傲英,“Web服务核心支撑技术：研究综述”,软件学报,2004,15(3)：428-442.
[10]I. Foster, C. Kesselman, "The Grid:Blueprint for a New Computing Infrastructure", Morgan Kaufmann Publishers,1998.
[11]A. Oram, "Peer-to-Peer:Harnessing the Power of Disruptive Technologies", ORei-lly& Associates,2001.
[12]J. Wang, K. He, P. Gong, et al, "RGPS:A Unified Requirements Meta-Modeling Frame for Networked Software", In Proc. of Third International Workshop on Advances and Applications of Problem Frames(IWAAPF'08) at 30th International Conference on Software Engineering(ICSE'08), Leipzig, Germany, May 2008.
[13]J. Wang, K. He, B. Li, et al, "Meta-models of Domain Modeling Framework for Networked Software", In Proc. of The Sixth International Conference on Grid and Cooperative Computing (GCC 2007), Urumchi, China, August 2007, pp.878-885.
[14]Z. Feng, K. He, Y. Ma, et al, "Towards Individualized Requirements Specification Evolution for Networked Software Based on Aspect", ICSP 2008, LNCS 5007, pp.88-99.
[15]I. Sommerville, P. Sawyer, "Requirement Engineering:A Good Practice Guide", John Wiley&Sons, Inc., New York, US,1997.
[16]P, Zave, M, Jackson, "Four Dark Corners of Requirements Engineering", ACM Transaction on Software Engineering and Methodology,1997,6(1), pp.1-30.
[17]M. Dorfman, R. H. Thayer, "Standards, Guidelines, and Examples on System and Software Requirements Engineering", IEEE Computer Society Press Tutorial,1990.
[18]卢梅,李明树,“软件需求工程-方法及工具评述”,计算机研究与发展,36(11),pp.1289-1300.
[19]刘玮,“面向服务的软件需求获取与分析研究”,武汉大学,博士论文,2008.
[20]K. C. Kang, S. Cohen, J. Hess, et al, "Feature-Oriented Domain Analysis (FODA):Feasibility Study", Technical Report CMU/SEI-90-TR-021, Software Engineering Institute, Carnegie Mellon University,1990.
[21]张伟,梅宏,“一种面向特征的领域模型及其建模过程”,软件学报,2003,14(8)：1345-1356.
[22]I. Jacobson, M. L. Griss, P. Jonsson, "Software Reuse:Architecture, Process and Organization for Business Success", Addison-Wesley Publishing, New York,1997.
[23]M. L. Griss, J. Favaro, M. d'Alessandro, "Integrating Feature Modeling with the RSEB", In Proc. of the 15th International Conference on Software Reuse,1998, IEEE, pp.76-85.
[24]G Chastek, P. Donohoe, K. C. Kang, et al. "Product Line Analysis:a Practical Introduction". Technical Report, CMU/DEI-2001-TR-01, Carnegie Mellon University, Software Engineering Institute.
[25]SEI, "Domain Engineering", Carnegie Mellon University,2004, Available: http://www.sei.cmu.edu/domain-engineering/domain eng.html.
[26]Olaf Zimmermann, P. K., Clive Gee. (2004). "Elements of Service-Oriented Analysis and Design." Available:http://www.ibm.com/developerworks/webservices/library/ws-soadl/
[27]N. Busi, R. Gorrieri, C. Guidi, R. Lucchi, and G. Zavattaro, "Choreography and Orchestration:A Synergic Approach for System Design". ICSOC 2005, LNCS 3826 pp. 228-240.
[28]M. A. Simos, "Organization Domain Modeling(ODM):Formalizing the Core Domain Modeling Life Cycle", In Proc. of the Symposium on Software Reusability, ACM Press, Washington,1995, pp.196-205.
[29]K. C. Kang, S. Kim, J. Lee, et al. "FORM:A Feature-oriented Reuse Method with Domain-specific Reference Architectures", Annals of Software Engineering,5(1998), pp. 143-168.
[30]M. Harsu, "FAST Product-line Architecture Process", Report 29, Institute of Software Systems, Tampere University of Technology, January 2002, Available: http://practise2.cs.tut.fi/pub/.
[31]CORDET, "Domain Engineering Methodologies Survey", Report GMV-CORDET-WP202-RP-001,2007, Available: www.pnp-software.com/cordet/download/pdf/GMV-CORDET-RP-001 Issl.pdf..
[32]P. Loucopoulos and E. Kavakli, "Enterprise Modeling and the Teleological Approach to Requirements Engineering", International Journal of Intelligent and Cooperative Information Systems,4(1),1995, pp.45-79.
[33]B. Nuseibeh, J. Kramer, and A. Finkelstein, "A Framework for Expressing the Relationships between Multiple Views in Requirements Specification", IEEE Transaction on Software Engineering,20(10),1994, pp.760-773.
[34]A. V. Lamsweerde, "Goal-oriented Requirements Engineering:a Guided Tour", In Proc. of the 5th IEEE International Symposium on Requirements Engineering, Toronto, Canada,2001, pp.249-263.
[35]E. Yu, "Modeling Strategic Relationships for Process Reengineering", PhD thesis, Department of computer science, University of Toronto,1994.
[36]J. Castro, M. Kolp, and J. Mylopoulos, "Towards Requirements-Driven Software Development Methodology:The Tropos Project", Information Systems, Vol.27,2002, pp. 365-389.
[37]A. V. Lamsweerde and E. Letier, "From Object Orientation to Goal Orientation:a Paradigm Shift for Requirements Engineering", Radical Innovations of Software and Systems Engineering in the Future,2004, pp.325-340.
[38]J. Mylopoulos, L. Chung and E. Yu, "From Object-Oriented to Goal-Oriented Requirements Analysis", Communications of the ACM,42(1), Jan.1999, pp.31-37.
[39]R. A. Falbo, G Guizzardi and K. C. Duarte, "An Ontological Approach to Domain Engineering", In Proc. of the International Conference on Software Engineering and Knowledge Engineering (SEKE'02), Ischia, Italy,2002, pp.351-358.
[40]金芝,陆汝钤,“多范例自动需求建模和分析：一种基于本体的方法”,中国科学(E辑),2003,33(4)：297-312.
[41]金芝,“基于本体的需求自动获取”,计算机学报,2000,23(5)：486-492.
[42]陆汝钤,金芝,陈刚,“面向本体的需求分析”,软件学报,2000,11(8)：1009-1017.
[43]W. M. P. van der Aalst, F. L., W. Reisig (2007). "The Role of Businesses in Service Oriented Architectures." Business Process Integration and Management 2(2007):75-80.
[44]J. Barjis,,"The importance of business process modeling in software systems design." Science of Computer Programming,2008,71:73-87.
[45]J. Cardoso, R. P. B., A. Sheth, "Workflow Management Systems and ERP Systems: Differences, Commonalities, and Applications." Information Technology and Management, 2004 (5):319-338.
[46]W. M. P. van der Aalst, K. M. v. H. "Workflow Management:Models, Methods, and Systems", MIT press, Cambridge, MA,2002.
[47]H. Smith, P. F., "Business Process Management-The Third Wave", Meghan-Kiffer Press, 2002.
[48]W. M. P. van der Aalst, A.H.M.ter Hofstede,, and M. Weske,.. "Business Process Management:A Survey", BPM2003, Springer-Verlag Berlin Heidelberg, LNCS2678, pp.1-12.
[49]W. M. P. van. der Aalst, "Business Process Management Demystified:A Tutorial on Models, Systems and Standards for Workflow Management". ACPN2004, LNCS3098, pp.1-60.
[50]F. Leymann, D. R., M. T. Schmidt "Web Services and Business Process Management." IBM Systems,2002,41(2):198-211.
[51]T. Woodley and S. Gagnon., "BPM and SOA:Synergies and Challenges", WISE'05, Springer-Verlag Berlin Heidelberg,2005, LNCS3806, pp.679-688.
[52]H. Schonenberg, R. M., N. Russell, W. M.P. van der Aalst (2008). "Process Flexibility:A Survey of Contemporary Approaches".4th International Workshop CIAO in CAiSE. Lecture Note in Information Processing,8, pp.16-30.
[53]W. M.P. van der Aalst, M. W., Dolf Grunbauer. "Case handling:a new paradigm for business process support." Data & knowledge Engineering(53),2005, pp.129-162.
[54]W. M. P. van der Aalst,., M. Pesic, "DecSerFlow:Towards a Truly Declarative Service Flow Language". WS-FM 2006, LNCS 4184, pp.1-23.
[55]Business Process Execution Language for Web Services version 1.1,2007, Available: http://www.ibm.com/developerworks/library/specification/ws-bpel/.
[56]M. Pesic, M. N. s., N.Sidorova, and W.M.P. van der Aalst. "Constraint-Based Workflow Models:Change Made Easy", OTM2007, LNCS 4803, pp 77-94.
[57]Martin Hepp, F. L., Chris Bussler, John Domingue, Alexander Wahler, et al. "Semantic Business Process Management:Using Semantic Web Services for Business Process Management", ICEBE 2005, IEEE, pp.535-540.
[58]Carlos Pedrinaci, J. D., Christian Brelage, et al., (2008). "Semantic Business Process Management:Scaling up the Management of Business Processes", IEEE International Conference on Semantic Computing, IEEE computer society,2008.
[59]I. Weber, J. H., Jan Mendling, and J. Nitzsche (2007). "Towards a Methodology for Semantic Business Process Modeling and Configuration", ICSOC Workshops 2007, pp.176-187.
[60]C.T. Jensen, I. Charters, J. Amasden, et al.,,"Leveraging SOA, BPM, and EA for Strategic Business and IT Alignment",2008, Available: http://www.ibm.com/developerworks/websphere/bpmjournal/0812_jensen/0812_jensen.html.
[61]Ivan Markovic, A. C. P, "Towards a Fromal Framework for Reuse in Business Process Modeling", BPM2007, LNCS 4928,2007, pp.484-495.
[62]Sudhir Agarwal, S. R., and Andreas Abecker, "Semantic Description of Distributed Business Processes". AAAI Spring Symposium-AI Meets Business Rules and Process Management, Stanford, USA,2008.
[63]吴步丹,金芝,赵彬,”面向服务的建模：一种全过程复用的方法.”计算机学报8(2008)：1293-1308.
[64]C. Pahl and M. Casey, "Ontology Support for Web Service Processes", In Proc.of 2003 European Software Engineering Conference and Foundations of Software Engineering (ESEC/FSE'03), ACM Press,2003, pp.208-216.
[65]S. McIlraith, T. C. Son, and H. Zeng, "Semantic Web Service", IEEE Intelligent Systems, 16(2),2001, pp.46-53.
[66]D. Martin, M. B., D. McDermott, et al.. "Bringing Semantics to Web Services with OWL-S." World Wide Web,2007,10:243-277.
[67]D. Martin, A.Ankolekar, M. Burstein, et al, "OWL-S:Semantic Markup for Web Services", W3C Candidate Recommendation,2004. Available:http://www.daml.org/services/owl-s/.
[68]D. Roman, J. d. Bruijn, A. Mocan, et al, "WWW:WSMO, WSML, and WSMX in a Nutshell", In Proc. of 1st Asian Semantic Web Conference (ASWC2006), Beijing, China, Sep.2006, pp.516-522.
[69]D. Roman, U. Keller, H. Lausen, et al, "Web Service Modeling Ontology", Applied Ontology Journal,1(1),2005, pp.77-106.
[70]J. de Bruijn, D16.3v1.0 WSML Abstract Syntax and Semantics,2008, Available: http://www.wsmo.org/TR/d16/d16.3/vl.0/.
[71]E. Borger, R. F. Stark, "Abstract State Machines:A Method for High-level System Design and Analysis", Springer,2003.
[72]A. J. Bonner, M. Kifer, "Transaction Logic Programming". ICLP 1993:257-279.
[73]A. J. Bonner, M. Kifer, "An Overview of Transaction Logic", Theor. Comput. Sci. 1994,133(2):205-265.
[74]A. J. Bonner, M. Kifer, "Concurrency and Communication in Transaction Logic". JICSLP 1996:142-156.
[75]P. van Eck, J. Engelfriet, D. Fensel, et al., "A Survey of Languages for Specifying Dynamics: A Knowledge Engineering Perspective", IEEE Transactions On Knowledge and Data Engineering,2001, vol 13, no.3, pp.462-496.
[76]H. Davulcu, M. Kifer, C. R. Ramakrishnan, I. V. Ramakrishnan:"Logic Based Modeling and Analysis of Workflows". In ACM Symposium on Principles of Database System,1998, pp. 25-33.
[77]H. Davulcu, M. Kifer., I.V. Ramakrishnan, " CTR-S:A Logic for Specifying Contracts in Semantic Web Services", WWW'04. New York, USA, ACM.
[78]D. Roman, M. Kifer, "Reasoning about the Behavior of Semantic Web Services with Concurrent Transaction Logic", VLDB 2007:627-638.
[79]D. Roman, M. Kifer, "Semantic Web Service Choreography:Contracting and Enactment', In Proc. of International Semantic Web Conference 2008:550-566.
[80]D. Roman, M. Kifer, D. Fensel, "WSMO Choreography:From Abstract State Machines to Concurrent Transaction Logic". ESWC 2008:659-673.
[81]A.W. Roscoe. "The Theory and Practice of Concurrency." Prentice-Hall,1997.
[82]E. Astesiano, M. Bidoit, H. Kirchner, et al. "CASL:the Common Algebraic Specification Language", Theoretical Computer Science,2002,286, pp.153-196.
[83]M. Bidoit, D. Sannella, A. Tarlecki, "Architectural Specifications in CASL", AMAST'98, LNCS 1548, pp.341-357.
[84]V. Dignum, "A Model for Organizational Interaction:Based on Agents, Founded in Logic" phD thesis,2004, Utrecht University.
[85]D. Grossi, F. Dignum, V. Dignum, et al., "Structural Aspects of the Evaluation of Agent Organizations", COIN 2006 Workshops, LNAI4386,2007, pp.3-18.
[86]A. Fuxman, L. Liu., M. Pistore,et al., "Specifying and analyzing early requirements:some experimental results." 11th IEEE International Requirements Engineering Conference(RE). 2003,pp.1-10.
[87]R. Milner, "Communicating and Mobile Systems:The Pi-Calculus", Cambridge University Press, Cambridge, UK,1999.
[88]王生原,余鹏,霍金健译,“系统工程Petri网：建模、验证与应用指南”,北京：电子工业出版社,2005.
[89]Y. Hirshfeld, M. Jerrum, "Bisimulation Equivalence Is Decidable for Normaed Process Algebra", ICALP'99, LNCS 1644, pp.412-421.
[90]Erhard Rahm, P. A. B. "A survey of approaches to automatic schema matching.", The VLDB Journal,2001, Vol.10:334-350.
[91]A. Oberschelp, "Order Sorted Predicate Logic", Sorts and Types in Artificial Intelligence, LNCS 418,1990, pp.7-17.
[92]G Booch, J. Rumbaugh and I. Jacobson, "The Unified Modeling Language User Guide", Addison-Wesley Longman, Inc,1999.
[93]E. M. Clarke, J. O. Grumberg, D. Peled, "Model Chekcing", MIT Press,2000.
[94]P. Haase, F. van Harmelen, Z. Huang, et al., "A Framework for Handing Inconsistency in Changing Ontologies", ISWC2005, LNCS 3729,2005, pp.353-367.
[95]K. Baclawski, M. M. Kokar, R. Waldinger, et al., "Consistency Checking of Semantic Web Ontologies", ISWC 2002, LNCS 2342,2002, pp.454-459.
[96]J. Davies, C. Crichton, "Concurrency and Refinement in the Unified Modeling Language", Fomal Aspects of Computing,2003,15, pp.118-145.
[97]M. Moller, E. R. Olderog, H. Rasch et al., "Integrating a formal method into a software engineering process with UML and Java." Formal Aspect Computing, Vol 20, pp.164-204, 2008.
[98]G. Smith. "The Object-Z Specification Language." Kluwer Academic Publisher,2000.
[99]C. Fischer and H. Wehrheim. "Model-checking CSPOZ specifications with FDR". In K. Araki, A. Galloway.and K. Taguchi, editors, Integrated Formal Methods, pp.315-334. Springer,1999.
[100]E. Yu. "Towards modeling and reasoning support for early requirements enginnering", In:Proceedings of the IEEE international symposium on requirement engineering. IEEE Computer Society, Washington, DC,,1997, pp.226-235.
[101]C. Ponsard, P. Massonet, A. Rifaut, A. van Lamsweerde and J. F. Molderez, "Early Verificatioin and Validation of Mission Critical System", Electronic Notes in Theoretical Computer Science,133,2005, pp.237-254.
[102]A. Fuxman, L. Liu, J. Mylopoulos, M. Pistore, M. Roveri and P. Traverso, "Specifying and analyzing early requirements in Tropos", Requirements Eng.,2004,9, pp.132-150.
[103]A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri. "NuSMV:a New Symbolic Model Checker". International Journal on Software Tools for Technology Transfer (STTT),2(4), 2000.
[104]D. Jackson, "Alloy:a lightweight object modeling notation", ACM Tran. Software Engineering Meth,2002,11:256-290.
[105]C. Heitmeyer, J. Kirby and B. Labaw, "The SCR method for formally specifying, verifying, and validating requirements:tool support", In:Proceedings of the 19th international conference on software engineering, ACM,1997, pp 610-611.
[106]Y. Choi, M. P. E, Heimdahl, "Model checking RSML-e requirements", In:Proceedings of the 7th IEEE international symposium on high assurance systems engineering, Tokyo, October 2002, IEEE Computer Socety, pp109-119.
[107]Franck van Breugel and Maria Koshkina, "Models and Verification of BEPL",2006, Available:www.cse.yorku.ca/-franck/research/drafts/tutorial.pdf.
[108]P, Gong. "Dynamic semantics of OWL-S in CSP-OZ". In 8th International Conference on Application of Concurrency to System Design, ACSD,2008, IEEE Press, pp.208-213.
[109]S. Graf, H. Saidi, "Construction of Abstract State Graphs with PVS", In O. Grumberg, Editor, Proc. of International Conference on Computer Aided Verfication(CAV'97), LNCS 1254,1997, pp.72-83.
[110]E. M. Clarke, D. Kroening, N. Sharygina, K. Yorav, "Predicate Abstraction of ANSI-C Programs Using SAT", Formal Methods in System Design,2004,25(2-3), pp.105-127.
[111]W. Sadiq, M. E. Orlowska, "Analyzing Process Models Using Graph Reducation Techniques", Inf. Syst.2000,25(2), pp.117-134.
[112]P. Soffer, Y. Wand, M. Kaner,"Semantic Analysis of Flow Patterns in Business Process Modeling", In G Alonso, P. Dadam, and M. Rosemann(Eds) BPM2007, LNCS 4714,2007, pp. 400-407.
[113]U. Keller, H. Lausen, M. Stollberg, "On the Semantics of Functional Descriptions of Web Services", In Y. Sure, J. Domingue(Eds) ESWC 2006, LNCS 4011,2006, pp.605-619.
[114]P. Gong, K. Q. He. "On the Capability Compliance of Annotated Process Model". In Proc. of 8th IEEE/ACIS International Conference on Computer and Information Science(ICIS'09), Shanghai China,2009, IEEE CS.
[115]Ly Linnh Thao, S. Rinderle,.P. Dadam, "Semantic Correctness in Adaptive Process Management Systems", In BPM2006 Workshops, LNCS 4102,2006, pp.193-208.
[116]G. Kolidis,. A. Ghose, "Verifying Semantic Business Process Modelsin Inter-operation", In Proceeding of International Conference on Services Computing(SCC), IEEE CS,2007.
[117]H. Meyer,"Calculating the Semantic Conformance of Processes", In BPM Workshops 2007, LNCS 4928,2008, pp.473-483.
[118]I. Weber,., J. Hoffmann,J. Mendling, "Beyond Soundness:On theSemantic Consisitency of Executable Proces Models", In Proceeding ofSixth European Conderence on Web Services, pp.102-111, IEEE CS,2008.