【作者】 任洪敏；

【导师】 钱乐秋；

【作者基本信息】 复旦大学 ， 计算机软件与理论， 2003， 博士

【摘要】 伴随计算机软件系统的规模和复杂程度不断提高，软件系统的结构变得日益复杂，软件设计重心从“算法+数据结构”设计转变成为体系结构设计。软件体系结构已经成为决定软件系统质量的重要因素，是软件产品线开发的关键技术之一，并因此成为当前软件工程领域的一个研究热点。 体系结构规约是软件体系结构重要的研究课题。运用自然语言和图表描述体系结构存在众多不足，难以有效实现软件体系结构预期的诸多好处。于是众多学者开始运用通用的形式化方法、提出专门的体系结构描述语言描述软件体系结构，这两类方法具有各自的特点和不足，并且它们通常在软件体系结构的演化、精化、分析和实现等方面缺乏支持，从而阻碍了软件体系结构在实践当中的应用。 据此，基于移动进程理论π演算，结合体系结构形式化方法和体系结构描述语言，我们提出软件体系结构形式化描述语言πADL，并以此作为基础，展开软件体系结构演化、精化、实现和分析等课题的探索和研究。具体如下： 1．基于移动进程代数π演算，提出软件体系结构形式化描述语言πADL，形式化描述软件系统的结构和行为。提出端口组装和六种构件组装机制及相应的组装推导算法，以有效支持体系结构层次化配置。 2．对动态体系结构进行研究，提出πADL描述动态体系结构的方法和相应的形式语义。该方法运用独立的π进程描述动态配置行为并，并与系统的计算行为交互，能够描述动态体系结构的诸多要素，包括动态演化的起因、时间、操作、非瞬时特性、断点继续执行等。 3．对体系结构精化进行研究，指出复合构件层次规约存在的不足，提出复合行为和体系结构行为精化的概念、规约的方法和法则及推导算法，确保精化过程中高层体系结构的行为特性得到保持，并自动生成低层体系结构。 4．对体系结构实现进行研究，指出运用现有构件技术实现体系结构存在的问题，分析体系结构领域和构件技术领域中软件构件的特点，提出面向体系结构的构件接口模型AOCIM，形式化给出AOCIM两级接口行为协议规约的方法，用以支持体系结构的实现。 5．对体系结构分析进行研究，基于π演算基本理论，结合体系结构领域的需求和特点，形式化定义有关概念和多种进程关系，并以此作为理论基础，提出πADL规约的8种静态检测方法，用以提高体系结构规约和系统组装的质量。 运用πADL及其相关研究工作，能够准确描述软件体系结构、推导系统的行为属性和分析系统规约的一致性，从而能够更好地支持体系结构驱动的软件开发方法，提升运用构件技术组装生成的软件系统的质量，向可预测系统组装这一软件工程的宏伟目标迈进一步。更多还原

【Abstract】 As the size and complexity of software increase, the overall system structure is becoming more and more complicated. Consequently, software design has its focus shifted from algorithm and data structure to software architecture. Software architecture has become one of the important factors in assuring software system qualities and one of the key technologies to the development of software product line. Therefore, it is emerging as a discipline of intense research in software engineering.Architectural specification is an important research subject in software architecture. Current representation of software architecture is in terms of natural languages and box-and-arrow drawings, which is a great disadvantage for implementing what software architecture promises as a separate discipline. Now a large amount of researchers begin both exploiting general formal methods and developing special architecture description languages to characterize software architecture precisely. Both approaches have important benefits and some weakness, that is, none of them can alone provide sufficient basis for architectural description. Moreover, they usually provide little supports for architecture evolution, refinement, analysis, implementation, etc., thereby significantly hamper software architecture application in practice.A formal architecture description language, πADL, therefore, is proposed as groundwork in this dissertation, based on mobile process theory π calculus and combining formal methods and architecture description languages. Then a series of architectural subjects, such as evolution, refinement, analysis, etc. are explored and studied systematically. Specifically, major contributions are as follows:Firstly, a formal architecture description language πADL is proposed based on process algebra π calculus, to express the structure and behavior of software architecture in a precise and practical way. Furthermore, port composition and six component composition mechanisms as well as their compositional reasoning algorithms are provided to support hierarchical configurations of software architecture effectively.Secondly, an π ADL modeling approach and corresponding formal semantics for dynamic software architecture are developed, which independently models both architectural computation behaviors and dynamic reconfiguration behaviors, with responsibility for the interactions between them as well. It, therefore, can specifymany aspects of dynamic architecture, including cause, time, operations and non-instantaneous change, etc.Thirdly, based on an insight into deficiencies in current architecture hierarchical configuration, ideas of composite behavior and architectural behavior refinement, related specification methods, principles and reasoning algorithm are proposed. They can ensure preserving the higher-level architectural behavior properties across refinement and generating lower-level architectures automatically and correctly.Fourthly, after illustrating of obstacles to implement software architecture according to today’s component technologies, the characteristics of software components in both software architecture field and component technology field are analyzed. Then, an architecture-oriented component interface model (AOCIM) is proposed and a two-level formal specification method of AOCIM component behavior protocols is developed in order to support architecture implementation effectively.Finally, based on the theory of π calculus and aiming at the characteristics and requirements of software architecture, a collection of concepts and process relationships are defined formally as a theory foundation, then eight static check methods to determine consistency of π ADL architecture specifications are developed, to raise qualities of architectural specifications and system composition,Briefly, in terms of πADL and related research, software architecture can be described precisely, system behavior properties can be reasoned formally and architectural specification can be analyzed rigorousl更多还原