安全软件体系结构的形式化方法研究
|
摘要
基于组件的软件体系结构是软件工程研究领域中的一个新的而且重要的课题。基于组件及其装配连接设计出的体系结构可以提供更丰富的设计信息,它除了可以描述设计模块之间的交互作用关系之外,还可以描述设计模块之间的约束关系、利用某些预先定义好的计算模型分析每个计算模块应具有的特性,并进一步分析体系结构的整体特性。软件体系结构反映了在一定构形下软件系统所要得到的重要性质(如安全性),它为软件设计和构造提供早期决策。近年来许多基于软件体系结构描述语言和体系结构风格的支持工具和属性模型纷纷涌现。为一个复杂系统提供形式化的体系结构描述,为所有参与系统设计、实现、维护的人员提供精确的系统结构描述文本,能在系统结构层经济省时地提供分析系统性质的可能性,进行早期错误检查。
软件安全性研究同样是目前比较热和新的研究领域,研究在软件体系结构中对安全性这种非功能属性如何给予描述、分析并验证是一项十分有意义的工作。软件的安全性是软件产品的质量属性之一,软件安全性保证是指在安全临界系统(safety critical system)的软件开发生命周期中进行的一系列质量保证活动,目的在于消除隐患。对于软件体系结构的安全属性,我们可以在形式化描述的基础上给出精确的形式化证明或给出其反例。软件体系结构的形式化模型有基于操作的模型、基于进程代数的模型、基于逻辑的模型、基于网络的模型。逻辑推理的方法有其自身的不足,模型检测的方法遇到的最大问题是状态空间的爆炸。目前的软件工具大多仅限于原型系统,有其应用的局限性。从数据结构和行为两方面来刻画软件体系结构模型的本质,这种方法更全面,用进程的行为来证明安全性更合理。目前软件体系结构在学术界的理论研究尤其是形式化方面的工作还相对缺乏,将安全性和软件体系结构结合起来的工作更稀少。在一个形式化的框架内对软件体系结构的安全性进行描述、分析和验证可以保证和维持基于构件的一类软件体系结构开发的一致性和完整性。因此使用形式化方法研究安全组件以及其交互形成的软件体系结构的安全特性具有重要意义和实用价值。针对软件体系结构的安全性问题,本文对描述模型和分析验证的方法进行了系统的研究和探讨,发展和完善了基于组件的软件体系结构模型性质的有关理论和方法,并将其应用到实际问题中。
文中首先分析和总结、比较了现有的安全软件体系结构的形式化研究方法和技术,然后给出了安全软件体系结构的形式化框架。并在此过程中逐步明确:使用基于组件的软件体系结构来构造软件系统,需要建立软件体系结构模型,其本质是利用形式化方法建立形式化模型来描述和验证复杂系统,形式化方法严格的数学基础使得系统具有较高的可信度和正确性,需要用它来详细分析组件的行为、研究其同步和通信的关系。系统描述基于组件的软件体系结构模型和组件的构成语法和结构、操作、行为语义。
其次,本文针对如何在安全软件体系结构中建立行为模型和静态结构模型、功能模型、过程模型的方法展开讨论。详细介绍如何使用状态转换系统描述安全软件体系结构的行为模型,包括建模方法的符号表达、建模步骤等。定义了稳定状态、稳定的状态转换、转换可达、直至形成系统的行为树,并建立系统的Kripke结构;通过证明状态转换系统的谓词转换器上不动点的存在来实现体系结构模型的安全性。由于进程代数的描述语言具有描述组件并发行为的能力,加上其严格的代数性质和强大的可借鉴的标准等价技术工具,文中重点使用它来进行基于组件的软件体系结构的安全性研究。使用进程代数的语言描述结构和过程模型(包括语法和操作语义),并在此模型基础上给出安全软件体系结构的描述规约,规约有文本表示和图形表示两种形式。进程代数语言描述的软件体系结构模型依靠构件类型、体系结构类型和构件实例的限制语义定义得到对静态操作符引起的交互行为语义;作为补充,主要从语法的角度建立静态结构模型来定义软件体系结构,它借鉴几种类型的文法对构件、连接方式、配置方式进行规则制定、形成软件体系结构的构成语法;功能模型是操作逻辑及其与其他形式化方法的结合,它使用时序逻辑描述系统安全性;为了更有说服力,文中还对常用的体系结构描述语言UML和Wright(另一种基于进程代数的语言)的系统软件体系结构建模能力进行分析,并将它们和其他基于进程代数的体系结构描述语言进行比较,并认为UML擅长于描述体系结构的静态结构如对组件、连接件的描述、对动作特定顺序的描述,不同视图可以从不同层次对体系结构进行描述,还能够通过版型(stereotype)的扩展机制实现进程代数语言描述的体系结构的静态建模,但是其描述动态结构能力差,最终不适合用它全面构造软件体系结构模型。
本文中间部分重点介绍如何使用基于进程代数的软件体系结构描述语言和其标准观察等价技术对体系结构进行相容性检查和互操作性检查,并且通过扩展体系结构描述语言将体系结构的相容性和互操作性检查扩展到不同风格的体系结构上。它们的正确性评估分别基于一个压缩代理系统和一个导航控制系统。该方法有行为和代数的本质,其中一个体系结构的描述仅仅由有固定行为的组件和连接件的类型以及拓扑结构的约束组成。这为组合、分层、图形化的体系结构描述语言(为了基于组件的软件系统族的规约和分析所开发的)提供了一个统一的框架,它可以保证在一个与一个给定的安全的组件交互的软件组件集合之内保持安全性,并扩展这两种检查到整个体系结构中。该方法建立了软件体系结构模型并通过相容性和互操作性检查保证了模型的安全性,其中所有检查都依赖于弱互模拟等价的性质,由于效率与/或诊断相关的原因,它比直接证明软件组件集合更方便,这一点已经得到证实。作为对基于进程代数的描述语言的补充,本文还针对简单的两组件安全通信的情况引入基于组件的软件体系结构的另一种安全模型。该模型以信任逻辑为基础进行安全性分析,给出安全构件的正常交互协议(包括协议的描述、分析、验证),以及当非法入侵构件存在时构件异常交互的协议,以组件通过连接件进行安全信息交流的情况为例建立软件体系结构的安全模型,并且验证了在该安全协议基础上建立的安全软件体系结构模型中,每一次模型实现都可以得到良好的安全性保证。
本文应用部分是按照在安全控制计算机系统的实例上层次式地建立系统软件体系结构的安全模型的过程逐步展开的。模型分为整个系统的软件体系结构模型、安全控制操作系统的模型、基于安全软件模型的访问控制部分软件体系结构的模型共三层。基于给定的安全标准,分析访问控制的安全模型包括自主访问控制、强制访问控制、基于角色的访问控制和信息流等安全模型。对这些基本模型的数学性质的详细研究为新的安全模型的建立提供了坚实基础。安全操作系统软件体系结构模型的建立是分几步走的:首先建立访问控制系统的体系结构缩减流图,详细分析原模型的局限性后通过举例说明来明确模型安全改造的方向;然后进行原体系结构模型的相容性检查,发现危险状态后分析引发危险的交互,反复重定义安全组件(判定组件和实施组件)的行为,指出引发危险的原因实际上是不合理的组件划分和细分后可能出现的违反组件互操作性的交互所造成的;最后详细论述经过改造后得到的新模型的安全性。安全操作系统的实现以原Linux操作系统为基础,其强制访问控制机制和信息完整性保护、增加安全标签的保护等方法都属于操作系统功能增强改进的方法,该方法在整个安全操作系统上的实现依赖于安全调用基于增强模型的访问控制机制。增强后的安全操作系统的全局体系结构图说明系统完全符合Flask结构。此外还以登录过程为例详细描述安全系统策略和技术的有效实现。
本文的最后介绍该安全方法的应用和外延。将安全软件体系结构模型和方法和软件复用技术相结合,具体有组件的安全复用技术和软件体系结构的安全复用技术,并给出安全复用方法的定义和描述以及方法的具体实施;在文中还对安全方法的应用进行扩充,将之应用于安全组件的互操作性、交互隐私性、原子性等安全相关的非功能属性的分析。
文末对论文的主要贡献进行了总结并提出了未来将开展的研究。
The research in the field of component-based software architecture plays an increasingly important role in software engineering area. The architecture derived from the components and their assembly can provide rich information for design because it describes both the interactions among modules and the constraints on them. It makes use of some predefined computing models to analyze the intuitive quality of each computing modules and then produces the further analysis of the overall architectural properties. Software architecture reflects the critical properties such as safety under some given configuration desired by the system, thus the decision is made for the design and construct at the early stage. In recent years many ADLs (architectural describing languages) and supporting kits and attributes models for architectural styles have come into being one by one. It enables the possibility of time- and labor-saving analysis of system properties on architectural level and the early error- checking that provides a formal architectural description for a complex software system.
At the same time, more and more research is focusing on the safety of software—a new topic in information community. It is a challenging work to make it clear that how to describe, analyze and verify such a non-functional property as safety in software architecture. As one of the quality attributes, the safety ensures that the series of activities can be carried out smoothly in the life cycle of the software development. The target is to eliminate the potential hazard. A precise formal verification or contrary examples can be given on the base of formal description. Formal architectural models include operation-, process algebra-, logic- and net-based ones. However current software tools are mainly restricted original systems and show various limitations on application, the features of description on data structure and its behavior require the process algebra as the main method to verify the security properties. There is considerately lack of the formal research on software architecture, especially on the combination of safety and software architecture. The consistency and complement of component- based architectural development are assumed and maintained through describing, analyzing and verifying the safety of software architecture within a formal framework. So it is of great importance and valuable for practical applications to explore the formal methods on safety of the components and their architecture.
In response to the safety problems in software architecture, our main contribution lies in the following:
This paper advances systematic research on the model- describing and analyzing, verifying methods for software architectures on various viewpoints;
This paper provides a formal framework on the safe software architectures and formally clarifies the conception of safe software architecture;
This paper integrates the related theories and approaches about the safe properties of models especially in formal methods;
This paper introduces the process algebra language with its powerful standard model-checking tools for safe software architectures and applies them successfully into practice.
On the basis of analysis of the existing formal methods and technologies, this paper proposes a formal framework for the safe software architecture in the first part. The necessity of establishing architectural models using components-based software architecture for constructing software systems is explained. The nature of the establishment is to achieve formal models through formal methods in order to describe and verify complex systems. The rigorous mathematical basis of the formal methods guarantees systems confidence and correctness. The system description is based on the architectural models, structural grammars and semantics of the construct, operation and behaviors.
Then we discuss how to model behavior, static structure, function, and process of the system. In details we introduce how to describe the behavioral models of safe architecture using states transition system that consists of the notation, modeling steps, etc. The system’s Kripke structure is established after the series definitions of stable states, stable sates transitions, reachable transitions, and system behavioral trees. We achieve the safety of the architectural model by verifying the existence of the fixed point on the predicate transformer in the states transition system. Because of the capabilities of describing the parallel behaviors of components, its rigorous algebra nature and its powerful standard equivalences tools, so this paper focuses on process algebra to carry out the research on safety of component-based software architecture. We describe the structure and process models using process-algebra-based language (including its syntax and operational semantics), and then provide the description specification (textual and graphical) on the model. From the definition of the constraint semantics of the component types, architecture types, and components instances, we achieve the semantic of the interactive behaviors arising from the static operator. To be supplement, the static structure model mainly provides architectural definition on the viewpoint of grammar. The functional model combining the operating logic and other formal approaches makes use of temporal logic to describe the system’s safety. Additionally, the abilities of the used describing language UML and Wright are analyzed and compared with other languages based on the process algebra.
In this paper, we concentrate on a process algebra-based architectural description language, which deals with incompatibility between two components due to a single interaction or the combination of several interactions and with the lack of interoperability among a set of components through architectural compatibility check and interoperability check relying on standard observational equivalences. The adequacy of the architectural compatibility check is assessed on a compressing proxy system, while the adequacy of the architectural interoperability check is assessed on a cruise control system. We then address the issue of scaling the checks to architectural styles though extension of the language, and we show that all the architectures conforming to the same architectural types possess the same compatibility and interoperability properties. This method has the nature of behavior and algebra, by which an architectural description is made up of only the types of components and connectors and the constraint on the topology. Thus a uniform framework is provided for the compositional, hierarchical, graphical architectural description language based on the component-based software architectural specification and analysis. It can ensure the safety within a given set of components interacting with a certain safe component. The architectural model established by such method owns the safety by both checks that turn out to be more convenient for efficiency and/or diagnosis-related reasons than directly verifying safety for the considered set of software components. As a complement of the process algebra-based language, we introduce another architectural safety model aiming at simple communication between two safe components, whose analysis of safety is based on the belief logic. It provides both normal and abnormal interaction protocols between safe components, including the protocol description, analysis and verification. The communicating model is built up taking the safe information fluent through safe components and safe connectors for example. We verify that each time the implement of the model is well remained safe in the existing safe architectural model.
The application part is hierarchically carried out in the project of security control personal computer system. Safe software architectural model is made up of software architectural model, the security control operating system model, and the safe access control model, three levels in all. Based on the given security standard, the analysis for the mathematical features of such models as mandatory access control and role-based access control enables the strong basis of the enhanced new model. The establishment of the safe operating system model is completed during the course of the reduce flow graph of the access control architecture, the architectural checks into the original system and the improvement of redefined safe components. The whole procedure shows that the true reason leading to danger is the incorrect division of components and the possible interactions that don’t conform the interoperability. Safe operating system on base of the original Linux system uses such improved approaches as information completeness protection, newly adding safe tag. Its realization relies on the safe call of the safe access control mechanism. The overall architectural structure graph of the enhanced security operating system illustrates that the system conforms the Flask structure completely. Additionally as a sample, the LOGIN process illustrates the effective realization of the safe technologies. Finally we introduce the application and expansion of the safe method. We combine the safe architectural models and methods and the software reuse technique. They are safe reuse technologies of the components, software architecture, and the definition of the methods and its practice. The method is also expanded to such other safety-related nonfunctional attributes as interoperability, privacy and the atomic properties.
Finally, we summarize what we have achieved and discuss our future work.
软件安全性研究同样是目前比较热和新的研究领域,研究在软件体系结构中对安全性这种非功能属性如何给予描述、分析并验证是一项十分有意义的工作。软件的安全性是软件产品的质量属性之一,软件安全性保证是指在安全临界系统(safety critical system)的软件开发生命周期中进行的一系列质量保证活动,目的在于消除隐患。对于软件体系结构的安全属性,我们可以在形式化描述的基础上给出精确的形式化证明或给出其反例。软件体系结构的形式化模型有基于操作的模型、基于进程代数的模型、基于逻辑的模型、基于网络的模型。逻辑推理的方法有其自身的不足,模型检测的方法遇到的最大问题是状态空间的爆炸。目前的软件工具大多仅限于原型系统,有其应用的局限性。从数据结构和行为两方面来刻画软件体系结构模型的本质,这种方法更全面,用进程的行为来证明安全性更合理。目前软件体系结构在学术界的理论研究尤其是形式化方面的工作还相对缺乏,将安全性和软件体系结构结合起来的工作更稀少。在一个形式化的框架内对软件体系结构的安全性进行描述、分析和验证可以保证和维持基于构件的一类软件体系结构开发的一致性和完整性。因此使用形式化方法研究安全组件以及其交互形成的软件体系结构的安全特性具有重要意义和实用价值。针对软件体系结构的安全性问题,本文对描述模型和分析验证的方法进行了系统的研究和探讨,发展和完善了基于组件的软件体系结构模型性质的有关理论和方法,并将其应用到实际问题中。
文中首先分析和总结、比较了现有的安全软件体系结构的形式化研究方法和技术,然后给出了安全软件体系结构的形式化框架。并在此过程中逐步明确:使用基于组件的软件体系结构来构造软件系统,需要建立软件体系结构模型,其本质是利用形式化方法建立形式化模型来描述和验证复杂系统,形式化方法严格的数学基础使得系统具有较高的可信度和正确性,需要用它来详细分析组件的行为、研究其同步和通信的关系。系统描述基于组件的软件体系结构模型和组件的构成语法和结构、操作、行为语义。
其次,本文针对如何在安全软件体系结构中建立行为模型和静态结构模型、功能模型、过程模型的方法展开讨论。详细介绍如何使用状态转换系统描述安全软件体系结构的行为模型,包括建模方法的符号表达、建模步骤等。定义了稳定状态、稳定的状态转换、转换可达、直至形成系统的行为树,并建立系统的Kripke结构;通过证明状态转换系统的谓词转换器上不动点的存在来实现体系结构模型的安全性。由于进程代数的描述语言具有描述组件并发行为的能力,加上其严格的代数性质和强大的可借鉴的标准等价技术工具,文中重点使用它来进行基于组件的软件体系结构的安全性研究。使用进程代数的语言描述结构和过程模型(包括语法和操作语义),并在此模型基础上给出安全软件体系结构的描述规约,规约有文本表示和图形表示两种形式。进程代数语言描述的软件体系结构模型依靠构件类型、体系结构类型和构件实例的限制语义定义得到对静态操作符引起的交互行为语义;作为补充,主要从语法的角度建立静态结构模型来定义软件体系结构,它借鉴几种类型的文法对构件、连接方式、配置方式进行规则制定、形成软件体系结构的构成语法;功能模型是操作逻辑及其与其他形式化方法的结合,它使用时序逻辑描述系统安全性;为了更有说服力,文中还对常用的体系结构描述语言UML和Wright(另一种基于进程代数的语言)的系统软件体系结构建模能力进行分析,并将它们和其他基于进程代数的体系结构描述语言进行比较,并认为UML擅长于描述体系结构的静态结构如对组件、连接件的描述、对动作特定顺序的描述,不同视图可以从不同层次对体系结构进行描述,还能够通过版型(stereotype)的扩展机制实现进程代数语言描述的体系结构的静态建模,但是其描述动态结构能力差,最终不适合用它全面构造软件体系结构模型。
本文中间部分重点介绍如何使用基于进程代数的软件体系结构描述语言和其标准观察等价技术对体系结构进行相容性检查和互操作性检查,并且通过扩展体系结构描述语言将体系结构的相容性和互操作性检查扩展到不同风格的体系结构上。它们的正确性评估分别基于一个压缩代理系统和一个导航控制系统。该方法有行为和代数的本质,其中一个体系结构的描述仅仅由有固定行为的组件和连接件的类型以及拓扑结构的约束组成。这为组合、分层、图形化的体系结构描述语言(为了基于组件的软件系统族的规约和分析所开发的)提供了一个统一的框架,它可以保证在一个与一个给定的安全的组件交互的软件组件集合之内保持安全性,并扩展这两种检查到整个体系结构中。该方法建立了软件体系结构模型并通过相容性和互操作性检查保证了模型的安全性,其中所有检查都依赖于弱互模拟等价的性质,由于效率与/或诊断相关的原因,它比直接证明软件组件集合更方便,这一点已经得到证实。作为对基于进程代数的描述语言的补充,本文还针对简单的两组件安全通信的情况引入基于组件的软件体系结构的另一种安全模型。该模型以信任逻辑为基础进行安全性分析,给出安全构件的正常交互协议(包括协议的描述、分析、验证),以及当非法入侵构件存在时构件异常交互的协议,以组件通过连接件进行安全信息交流的情况为例建立软件体系结构的安全模型,并且验证了在该安全协议基础上建立的安全软件体系结构模型中,每一次模型实现都可以得到良好的安全性保证。
本文应用部分是按照在安全控制计算机系统的实例上层次式地建立系统软件体系结构的安全模型的过程逐步展开的。模型分为整个系统的软件体系结构模型、安全控制操作系统的模型、基于安全软件模型的访问控制部分软件体系结构的模型共三层。基于给定的安全标准,分析访问控制的安全模型包括自主访问控制、强制访问控制、基于角色的访问控制和信息流等安全模型。对这些基本模型的数学性质的详细研究为新的安全模型的建立提供了坚实基础。安全操作系统软件体系结构模型的建立是分几步走的:首先建立访问控制系统的体系结构缩减流图,详细分析原模型的局限性后通过举例说明来明确模型安全改造的方向;然后进行原体系结构模型的相容性检查,发现危险状态后分析引发危险的交互,反复重定义安全组件(判定组件和实施组件)的行为,指出引发危险的原因实际上是不合理的组件划分和细分后可能出现的违反组件互操作性的交互所造成的;最后详细论述经过改造后得到的新模型的安全性。安全操作系统的实现以原Linux操作系统为基础,其强制访问控制机制和信息完整性保护、增加安全标签的保护等方法都属于操作系统功能增强改进的方法,该方法在整个安全操作系统上的实现依赖于安全调用基于增强模型的访问控制机制。增强后的安全操作系统的全局体系结构图说明系统完全符合Flask结构。此外还以登录过程为例详细描述安全系统策略和技术的有效实现。
本文的最后介绍该安全方法的应用和外延。将安全软件体系结构模型和方法和软件复用技术相结合,具体有组件的安全复用技术和软件体系结构的安全复用技术,并给出安全复用方法的定义和描述以及方法的具体实施;在文中还对安全方法的应用进行扩充,将之应用于安全组件的互操作性、交互隐私性、原子性等安全相关的非功能属性的分析。
文末对论文的主要贡献进行了总结并提出了未来将开展的研究。
The research in the field of component-based software architecture plays an increasingly important role in software engineering area. The architecture derived from the components and their assembly can provide rich information for design because it describes both the interactions among modules and the constraints on them. It makes use of some predefined computing models to analyze the intuitive quality of each computing modules and then produces the further analysis of the overall architectural properties. Software architecture reflects the critical properties such as safety under some given configuration desired by the system, thus the decision is made for the design and construct at the early stage. In recent years many ADLs (architectural describing languages) and supporting kits and attributes models for architectural styles have come into being one by one. It enables the possibility of time- and labor-saving analysis of system properties on architectural level and the early error- checking that provides a formal architectural description for a complex software system.
At the same time, more and more research is focusing on the safety of software—a new topic in information community. It is a challenging work to make it clear that how to describe, analyze and verify such a non-functional property as safety in software architecture. As one of the quality attributes, the safety ensures that the series of activities can be carried out smoothly in the life cycle of the software development. The target is to eliminate the potential hazard. A precise formal verification or contrary examples can be given on the base of formal description. Formal architectural models include operation-, process algebra-, logic- and net-based ones. However current software tools are mainly restricted original systems and show various limitations on application, the features of description on data structure and its behavior require the process algebra as the main method to verify the security properties. There is considerately lack of the formal research on software architecture, especially on the combination of safety and software architecture. The consistency and complement of component- based architectural development are assumed and maintained through describing, analyzing and verifying the safety of software architecture within a formal framework. So it is of great importance and valuable for practical applications to explore the formal methods on safety of the components and their architecture.
In response to the safety problems in software architecture, our main contribution lies in the following:
This paper advances systematic research on the model- describing and analyzing, verifying methods for software architectures on various viewpoints;
This paper provides a formal framework on the safe software architectures and formally clarifies the conception of safe software architecture;
This paper integrates the related theories and approaches about the safe properties of models especially in formal methods;
This paper introduces the process algebra language with its powerful standard model-checking tools for safe software architectures and applies them successfully into practice.
On the basis of analysis of the existing formal methods and technologies, this paper proposes a formal framework for the safe software architecture in the first part. The necessity of establishing architectural models using components-based software architecture for constructing software systems is explained. The nature of the establishment is to achieve formal models through formal methods in order to describe and verify complex systems. The rigorous mathematical basis of the formal methods guarantees systems confidence and correctness. The system description is based on the architectural models, structural grammars and semantics of the construct, operation and behaviors.
Then we discuss how to model behavior, static structure, function, and process of the system. In details we introduce how to describe the behavioral models of safe architecture using states transition system that consists of the notation, modeling steps, etc. The system’s Kripke structure is established after the series definitions of stable states, stable sates transitions, reachable transitions, and system behavioral trees. We achieve the safety of the architectural model by verifying the existence of the fixed point on the predicate transformer in the states transition system. Because of the capabilities of describing the parallel behaviors of components, its rigorous algebra nature and its powerful standard equivalences tools, so this paper focuses on process algebra to carry out the research on safety of component-based software architecture. We describe the structure and process models using process-algebra-based language (including its syntax and operational semantics), and then provide the description specification (textual and graphical) on the model. From the definition of the constraint semantics of the component types, architecture types, and components instances, we achieve the semantic of the interactive behaviors arising from the static operator. To be supplement, the static structure model mainly provides architectural definition on the viewpoint of grammar. The functional model combining the operating logic and other formal approaches makes use of temporal logic to describe the system’s safety. Additionally, the abilities of the used describing language UML and Wright are analyzed and compared with other languages based on the process algebra.
In this paper, we concentrate on a process algebra-based architectural description language, which deals with incompatibility between two components due to a single interaction or the combination of several interactions and with the lack of interoperability among a set of components through architectural compatibility check and interoperability check relying on standard observational equivalences. The adequacy of the architectural compatibility check is assessed on a compressing proxy system, while the adequacy of the architectural interoperability check is assessed on a cruise control system. We then address the issue of scaling the checks to architectural styles though extension of the language, and we show that all the architectures conforming to the same architectural types possess the same compatibility and interoperability properties. This method has the nature of behavior and algebra, by which an architectural description is made up of only the types of components and connectors and the constraint on the topology. Thus a uniform framework is provided for the compositional, hierarchical, graphical architectural description language based on the component-based software architectural specification and analysis. It can ensure the safety within a given set of components interacting with a certain safe component. The architectural model established by such method owns the safety by both checks that turn out to be more convenient for efficiency and/or diagnosis-related reasons than directly verifying safety for the considered set of software components. As a complement of the process algebra-based language, we introduce another architectural safety model aiming at simple communication between two safe components, whose analysis of safety is based on the belief logic. It provides both normal and abnormal interaction protocols between safe components, including the protocol description, analysis and verification. The communicating model is built up taking the safe information fluent through safe components and safe connectors for example. We verify that each time the implement of the model is well remained safe in the existing safe architectural model.
The application part is hierarchically carried out in the project of security control personal computer system. Safe software architectural model is made up of software architectural model, the security control operating system model, and the safe access control model, three levels in all. Based on the given security standard, the analysis for the mathematical features of such models as mandatory access control and role-based access control enables the strong basis of the enhanced new model. The establishment of the safe operating system model is completed during the course of the reduce flow graph of the access control architecture, the architectural checks into the original system and the improvement of redefined safe components. The whole procedure shows that the true reason leading to danger is the incorrect division of components and the possible interactions that don’t conform the interoperability. Safe operating system on base of the original Linux system uses such improved approaches as information completeness protection, newly adding safe tag. Its realization relies on the safe call of the safe access control mechanism. The overall architectural structure graph of the enhanced security operating system illustrates that the system conforms the Flask structure completely. Additionally as a sample, the LOGIN process illustrates the effective realization of the safe technologies. Finally we introduce the application and expansion of the safe method. We combine the safe architectural models and methods and the software reuse technique. They are safe reuse technologies of the components, software architecture, and the definition of the methods and its practice. The method is also expanded to such other safety-related nonfunctional attributes as interoperability, privacy and the atomic properties.
Finally, we summarize what we have achieved and discuss our future work.
引文
[1] Leveson and Nancy, G., “Software Safety in Embedded Computers Systems”, Communication of the CAN, Feb 1991, Vol.34, No.2.
[2] Keene, Jr. and Samuel, J., “Assuring Software Safety”, Proceedings Annual Reliability and Maintainability Symposium, 1992.
[3] 孙昌爱, 金茂忠, 刘超, “软件体系结构综述”, 软件学报, 2002, Vol.7, No.13, pp: 1228-1237.
[4] Oscar Nierstrasz and Theo Dirk Meijler, “Research Directions in Software Composition”, ACM Computing Surveys, Jun 1995, Vol.27, No.2, pp: 262-264.
[5] Boehm, B, “Engineering context (for software architecture)”, invited talk, In: Garlan, D., ed. Proceedings of the 1st International Workshop on Architecture for Software Systems Settle, New York, ACM Press, 1995, pp: 1-8.
[6] Shaw, M. and Garlan, D., “Software Architecture: Perspectives on an Emerging Discipline”, 1996, Prentice-Hall, Englewood Cliffs, New Jersey.
[7] Booch, G., “Software Components with Ada, Structures, Tools and Subsystems”, 1987, Benjamin/ Cummings Publishing Company, Menlo Park.
[8] Hugo Fierz. “The CIP Method: Component-and Model-Based Construction of Embedded Systems”, Software Engineering Notes, 1999, Vol.24, No 6, pp: 375-393.
[9] Abowd, G. D., Allen, R., and Garlan, D, “Formalizing style to understand descriptions of software architecture”, ACM Trans. Software Engineering, Math. 4, 1995, pp: 319-364.
[10] Colin Boyd, “Security Architectures Using Formal Methods”, IEEE Journal on Selected Areas in Communications, June 1993, Vol. 11, No. 5.
[11] 周之英,“现代软件工程——基本方法篇”,2000 年 1 月,第一版,科学出版社.
[12] 周莹新,艾波, “软件体系结构建模研究”, 软件学报,1998, Vol 9, pp: 867-872.
[13] ISO 7482-2, Information Process System—Open systems Interconnection Reference Security Architecture, 1988.
[14] David Garlan and Dewayne E. Perry, “Introduction to the Special Issue on Software Architecture”, IEEE Transactions on Software Engineering, Apr 1995, Vol.21, No.4, pp: 269-274.
[15] Devayne E. Perry, Alexander L. Wolf, “Foundation for the Study of Software Architecture,” ACM SIGSOFT, 1992, Vol.10, No.4.
[16] Nenad Medvidovic and Richard N. Taylor, “A Classification and Comparison Framework for Software Architecture Description Languages,” IEEE Transactions On Software Engineering, JAN. 2000, Vol.26, No.1.
[17] Shaw, M., Deline, R., Klein, D. V., Ross, T. L., Young, D. M., and Zelesnik, G.,“Abstractions for software architecture and tools to support them”, IEEE Transaction of Software Engineering, 1995, Vol.21, pp: 314-335.
[18] R. Allen, D. Garlan, “A Formal Basis for Architectural Connection,” ACM Trans. Software Engineering and Methodology, Vol.6, No.3, July 1997, pp: 213-249.
[19] Luckham, D., Lary, C., and Augustin, M, “ Specification and analysis of system architecture using rapide”, IEEE Transactions on Software Engineering 1995, Vol.21, No.4, pp: 336-355.
[20] J. Magee, J. Kramer, “Dynamic Structure in Software Architectures”, Proc. ACM SIGSOFT’96, Oct 1996, pp: 3-14.
[21] J. M. Spivey, “the Z Notation: a Reference Manual”, 1989, Englewood Cliffs, NJ: Prentice-Hall.
[22] 张广泉, “基于 XYZ/E 的软件体系结构描述语言研究”,计算机科学,2000,Vol. 27, No. 9, pp: 155-157
[23] 唐稚松等, “时序逻辑程序设计与软件工程”,2002 年 5 月,北京,科学出版社.
[24] 张广泉,唐稚松, “一种新的软件体系结构描述语言”,中国博士后学术大会论文集,2001年 2 月,北京,科学出版社.
[25] 骆华俊,唐稚松,郑建丹,“可视化体系结构描述语言 XYZ/ADL”,软件学报,2000,Vol. 11, No. 8, pp: 1024-1029.
[26] Abowd G., Allen R., and Garlan, D, “Using style to understand description of Software Architecture”, ACM SIGSOFT Software Engineering Notes, 1993, pp: 9-20.
[27] D. Garlan, “An Introduction to the Aesop System”, July 1995.
[28] http://www.cs.cmu.edu/afs/cs/project/table/aesop/html/aesop_overview.ps.
[29] R. N. Taylor, “Using Object-Oriented Typing to Support Architectural Design in the C2 Style,” Proc. ACM SIGSOFT’96, Oct 1996. pp: 24-32.
[30] M. Moriconi, X. Qian, R. A. Riemenschanaider, “Correct Architecture Refinement,” IEEE Trans Software Eng., Apr 1995, Vol.21, No.4, pp: 356-372.
[31] M. Shaw, R. Deline, G. Zelesnik, “Abstractions and Implementations for Architectural Connections,” Proc. Third Int’l Conf. Configurable Distributed System, May 1996.
[32] S. Vestal, “MetaH Programmer’s Manual, Version 1.09,” technical report, Honeywell Technology Center, April 1996.
[33] Allen R., Garlan D, “Formal Connectors”, Technology Report, CMU-CS-94-115, Pittsburg: Carnegie Mellon University, 1994.
[34] D. C. Luckham, J. Vera, “Event-Based Architecture Definition Language,” IEEE Trans. Software Eng., Sept 1995, Vol.21, No.9, pp: 717-734.
[35] D. Garlan, R. Monroe, D. Wile, ”ACME: An Architecture Description Interchange Language,” Proc.CASCON’97, Nov 1997.
[36] M. M. Gorlick and R. R. Razouk, “Using Weaves for Software Construction and Analysis,”Proc.13th Int’l Conf. Software Eng. (ICSE13), May 1991, pp: 23-34.
[37] Jeremy Bryans, Steve Schneider, “CSP, PVS and a recursive authentication protocol”, In DIMACS Workshop on Design and Formal Verification of Security Protocols, September 1997.
[38] Hoare, C. A. R., “Communicating Sequential Process”, 1985, Prentice Hall, Englewood Cliffs, New Jersey.
[39] Jan Wessels, “Applications of BAN-LOGIC”, IPA Spring Days on Security, April 18-20, 2001.
[40] M. Nail, G. Ostrolenk, M. Tobin, “Lessons from using Z to Specify a Software Tool”, IEEE Trans. Soft. Eng., 1998, Vol.24, No.1, pp: 15-23.
[41] 屈延文, “形式化语义学基础与形式说明”, 1998, 科学出版社.
[42] 陆汝铃, “形式语义”, 1992, 科学出版社.
[43] R. Milner, “A Calculus of Communication System”, LNCS92, 1980, Springer-Verlag.
[44] 郑红军,张乃孝, “软件开发中的形式化方法”, 计算机科学, 1997, Vol.24, No.6.
[45] Leonor Barroca, Jon Hall, Patrick Hall, “Software Architecture Advance and Applications”, 2000, Springer-Verlag, London.
[46] 张家晨,冯铁,陈伟,金淳兆, “基于主动连接件的软件体系结构及其描述方法”, 软件学报, 2000, Vol.11, pp: 1047-1052.
[47] Clarke, E.M., Grumberg, O., and Peled, D. A, “Model Checking”, 1999, MIT Press.
[48] M. Burrows, M. Abadi, and R. Needham, “A logic of authentication”, ACM Transactions on Computer Systems, 8, February 1990.
[49] D. Kindred and J. M. Wing, “Fast, automatic checking of security protocols”, In USENIX 2nd Workshop on Electronic Commerce, 1996.
[50] Balsamo, S., Bernardo, M. and Simeoni, M., “Combining stochastic process algebras and queuing networks for software architecture analysis”, In Proceedings of the 3rd International Workshop on Software and Performance (WOSP 2002), ACM, New York, 2002, pp: 190-202.
[51] C. Meadows, “A System for the specification and analysis of key management protocols”, in Proc. 1991 IEEE Computer Society. Symp, Security Privacy, IEEE Computer Society Press, 1991, pp: 182-195.
[52] R. A. Rueppel, “A formal approach to security architectures”, in Proc. Eurocrypt91. New York: Springer-Verlag, 1991.
[53] L. Gong, R. Needham, and R. Yahalom, “Reasoning about belief in cryptographic protocols”, in Proc 1990 IEEE Computer Society. Symp, Security Privacy, IEEE Computer Society Press, 1990, pp: 234-248.
[54] M. Burrows, M. Abadi, R. Needham, “A Logic of authentication”, ACM Trans. ComputerSystem, Feb 1990, Vol. 8, No. 1, pp: 18-36.
[55] R. Kailar and V. D. Gilgor, “on belief evolution in authentication protocols”, in Proc. Computer Security Foundations Workshop IV. New York: IEEE Press, 1991, pp: 103-116.
[56] M. Bernardo, P. Ciancarini, L. Donatiello, “Architecture families of software systems with process algebras.” ACM Transactions on Software Engineering and Methodology, October 2002, Vol.11, No.4.
[57] Apt. K. R., “Ten years of Hoare Logic: A Survey”, ACM Transaction on Programming Languages and Systems, 1981, Vol.3, No.4, pp: 431-483.
[58] Constable, et al, “Implementing Mathematics of with Nuprl Proof Development System”, New Jersey: Prentice-Hall, Englewood Cliffs, 1986.
[59] E. M. Clarke and J. M. Wing, “Formal Methods: State of the Art and Future Directions”, ACM Computing Surveys, 1996, Vol.28, No.4, pp: 626-643.
[60] J. Mitchell, M. Mitchell, U. Stern, “Automated analysis of cryptographic protocols using Murφ”, In Proceedings of the 1997 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, May 1997, pp: 141--151.
[61] M. Debbabi, M. Mejri, N. Tawbi, and I. Yahmadi, “A new algorithm for the automatic verification of authentication protocols: From specifications to flaws and attack scenarios”, In DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997.
[62] Lin Liu, Eric Yu, John Mylopoulos, “Analyzing Security Requirements as Relationships among Strategic Actors”, Proceeding of 20th International Conference on Conceptual Modeling (ER-2001), Yokohama, Japan, November 27-30, 2001.
[63] Riccardo Focardi and Roberto Gorrieri, “the Compositional Security Checker: a Tool for the Verification of Information Flow Security Properties”, IEEE Trans on Software Engineering, Vol. 23, No. 9, September 1997.
[64] C. R. Tsal, V. D. Gilger, and C. S. Chanclesekaran, “on the discipline of covert Storage channels in secure systems”, IEEE Trans on Software Eng., June 1990, pp: 569-580.
[65] P. Y., A. Ryan, “A CSP Formulation of Noninterference”, Proc Computer Security Foundation Workshop, Franconia, 1990, IEEE CS Press.
[66] A. W. Rosore, J. C. P. Woodcook and L. Wolf, “Noninterference through Determination”, Proc European Symposium, Research in Computer Security 1994 (ESORJCS94), pp: 33-53.
[67] A. W. Rosore, “ Model Checking CSP——A classical Mind”, 1994, Prentice Hall.
[68] 傅建明, “基于 Ada 并行计算模型的安全性研究”, 武汉大学博士学位论文,2000 年 4月.
[69] Bashar Nuseibeh, “Weaving together Requirements and Architectures.” IEEE Computer, 2001, Vol. 34, No. 3, pp: 115-117.
[70] John G. Hall, Michael Jackson, Robin C. Laney, Bashar Nuseibeh, Lucia Rapanotti,“Relating Software requirements and architectures using problem frames”, Proceedings of IEEE International Requirements Engineering Conference (RE'02), Essen, 2002, Vol. 9,Vol. 13, pp: 137-144.
[71] K. Heninger, D. L. Parnas, J. E. Shore, J. W. Kallander, “Software requirements for the A7E aircraft”, TR3876, 1978, Naval Research lab, Washington, DC.
[72] C. L. Heitmeyer, R. D. Jeffords, B. G. Labaw, “Automated consistency checking of requirements specifications”, ACM Transactions on Software Engineering and Methodology, 1996, Vol. 5,Nov. 3, pp: 231-261.
[73] Kolp M. Castro, J. Mylopoulos, “A Social Organization Perspective on Software Architectures”, In Proc. of the First Int. Workshop From Software Requirements to Architectures, STRAW'01, Toronto, May 2001, pp: 5-12.
[74] J. Mylopoulos, A. Borgida, M. Jarke, M. Koubarakis, “Telos: Representing Knowledge About Information Systems”, ACM Trans. Info. Sys, Vol.8, Nov.4, Oct.1990, pp: 325-362.
[75] P. Grunbacher, A. Egyed, N. Medvidovic, “Reconciling software requirements and architectures: The CBSP Approach”, Proceedings of the 5th International Symposium on Requirements Engineering (RE’01), IEEE CS Presss2001, pp: 202-211.
[76] Alexander Egyed, Paul Grünbacher, Nenad Medvidovic, “Refinement and Evolution Issues in Bridging requirements and architecture – the CBSP approach”, IEEE Trans on Software Engineering, 1996, Vol.22, Nov.6, pp: 390-406.
[77] Boehm B., Gruenbacher P, “Supporting Collaborative Requirements Negotiation: The EasyWinWin Approach”, Proceeding of SCS on Virtual Worlds and Simulation, San Diego, 2000.
[78] Medvidovic N., Gruenbacher P., Egyed A., Boehm B., “Software Lifecycle Connectors: Bridging Models across the Lifecycle”, the 23rd International Conference on Software Engineering (ICSE 2001), Toronto, 2001.
[79] Brandozzi M., Perry D.E, “Transforming Goal-Oriented Requirement Specifications into Architecture Prescriptions”, ICSE 2001.
[80] Liu, L., Yu. E, “From Requirements to Architectural Design - Using Goals and Scenarios”, ICSE-2001 Workshop: From Software Requirements to Architectures (STRAW 2001) Toronto, Canada, May 2001, pp: 22-30.
[81] Klaus Pohl, Mathias Brandenburg, Alexander Gulich, “Integrating requirement and architecture information: a scenario and meta-model based approach”, Paper of the Seventh International Workshop on Requirements Engineering: Foundation for Software Quality (REFSQ), June 2001.
[82] 魏峻, “基于规范的软件形式方法的研究一种时序逻辑的框架”, 武汉大学博士学位论文,1997.
[83] N. Medvidovic and R. N. Taylor, “Exploiting architectural style to develop a family of applications”, IEE Proceedings Software Engineering, Oct.-Dec.1997, Vol.144, No.5-6, pp: 237-248.
[84] Richard N. Taylor, Nenad Medvidovic, Kenneth M, Anderson, et al., “A Component-and Message-Based Architectural Style for GUI Software”, IEEE Transactions on Software Engineering, June 1996, Vol.22, No.6, pp: 390-406.
[85] 鲍敢峰,尤晋元, “软件体系结构的图形语法”, 计算机工程, Dec 1997, Vol.23, Special Issue.
[86] Andersen, H. R, “Partial model checking”, In Proceedings of the 10th IEEE International Symposium on Logic in Computer Science (LICS1995), 1995, IEEE-CS Press, New York, pp: 398-407.
[87] Bruno Dutertre and Steve Schneider, “Using a PVS Embedding of CSP to Verify Authentication Protocols”, In Theorem Proving in Higher Order Logics, number 1275 in LNCS. 1997, Springer-Verlag.
[88] Fu. K. S. and Booth. T. H, “Grammatical Inference Introduction and Survey”, IEEE Trans. On SMC-5, 1975, pp: 395-409.
[89] A.D. Rubin and P. Honeyman, “Formal Methods for the Analysis of Authentication Protocols”, Technical Report Technical report 93-7, Technical Report, Center for Information Technology Integration, 1993. University of Michigan.
[90] 邵维忠,麻志毅,张文娟,孟祥文(译), “UML 用户指南”, 2001, 北京, 机械工业出版社.
[91] 邵维忠,梅宏, “统一建模语言 UML 述评”, 计算机研究与发展,1999, Vol. 36, No. 4, pp: 1-8.
[92] OMG. “OMG Unified Modeling Language Specification 1.3,1.4”, http://www.omg.org/uml/
[93] 邵维忠,蒋严冰,麻志毅, “UML 现存的问题和发展道路”, Apr. 2003, Vol. 40, No. 4, pp: 509-515.
[94] 蒋慧, 林东, 谢希仁, “UML 状态机的形式语义”,软件学报, 2002, Vol.23, No.12, pp: 2244-2250.
[95] Bernardo, M., Ciancarini, P., and Donatiello, L., “On the formalization of architectural types with process algebras”, In Proceedings of the 8th ACM International Symposium on the Foundations of Software Engineering (FSE-8), 2000, ACM, New York, pp: 140-148.
[96] Bernardo, M., Ciancarini, P., and Donatiello, L., “Detecting architectural mismatches in process algebraic descriptions of software systems”, In Proceedings of the 1st Working IEEE/IFIP Conference on Software Architecture (WICSA 2001), 2001, IEEE-CS Press, New York, pp: 77-86.
[97] Bernardo, M., Donatiello, L., and Ciancarini, P., “Stochastic process algebra: from analgebraic formalism to an architectural description language”, In Performance Evaluation of Complex Systems: Techniques and Tools, Calzarossa, M. C., and Tucci, S., Eds, Lecture Notes in Computer Science, 2002, Vol.2459, Springer-Verlag, New York, pp: 236-260.
[98] Bernardo, M., Franze, F., “Architectural types revisited: extensible and/or connections”, In Proceedings of the 5th International Conference on Fundamental Approaches to Software Engineering (FASE 2002), Lecture Notes in Computer Science, 2002, Vol.2306, Springer, New York, pp: 113-128.
[99] Bernardo, M., Franze, F., “Exogenous and endogenous extensions of architectural types”, In Proceedings of the 5th International Conference on Coordination Models and Languages (COORDINATION 2002), Lecture Notes in Computer Science, 2002, Vol.2306, Springer, New York, pp: 44-55.
[100] Bravetti, M. and Bernardo, M., “Compositional asymmetric co-operations for process algebras with probabilities, priorities, and time”, In Proceedings of the 1st Workshop on Models for Time Critical Systems (MTCS 2000), ENTCS, 2000, Vol.39, No.3, Elsevier, Amsterdam, The Netherlands.
[101] Colin Boyd and Wenbo Mao, “On a limitation of ban logic”, Advances in Cryptology: Proceedings of Eurocrypt 93, 1993, pp: 240—247.
[102] Clarke, E. M., Long, D. E., McMillan, K. L., “Compositional model checking”, In Proceedings of the 4th IEEE International Symposium on Logic in Computer Science (LICS 1989), IEEE-CS Press, New York, 1989, pp: 353-362.
[103] David M., “Kronecker products and shuffle algebras”, IEEE Trans, Computer, 1981, Vol.30, pp: 116-125.
[104] Dean, T. R. and Cordy, J. R., “A syntactic theory of software architecture”, IEEE Trans. Software Engineering, 1995, Vol.21, pp: 302-313.
[105] De Remer, F. and Kron, H. H., “Programming-in-the-large versus programming-in-the-small”, IEEE Trans. Software Engineering, 1976, Vol.2, pp: 80-86.
[106] Van Glabbeek, R. J., “The linear time-branching time spectrum I The semantics of concrete, sequential processes”, In Handbook of Process Algebra, Bergstra, J. A., Ponse, A., and Smolka, S. A., Eds, Elsevier, 2001, pp: 3-99.
[107] Kramer, J. and Magee, J., “Exposing the skeleton in the coordination closet”, In Proceedings of the 2nd International Conference on Coordination Models and Languages (COORDINATION 1997), Lecture Notes in Computer Science, Vol.1282, Springer-verlag, New York, 1997, pp: 18-31.
[108] Lavenberg, S. S., Ed, “Computer Performance Modeling Handbook”, Academic Press, Orlando, Fla, 1983.
[109] Martin Abadi and Mark Tuttle, “A Semantics for a Logic of Authentication”, In Proceedingsof the Tenth ACM Symposium on Principles of Distributed Computing, ACM Press, August 1991, pp: 201--216.
[110] L. Gong, R. Needham, and R. Yahalom, “Reasoning about Belief in Cryptographic Protocols”, Proc. of the IEEE 1990 Symp on Security and Privacy Oakland, California, May 1990, pp: 234-248.
[111] Klaus Grader, Einar Snekkenes, “Applying a Formal Analysis Technique to the CCITT X.509 Strong Two-Way Authentication Protocol”, Journal Of Cryptology, 1991, Vol.3, pp: 81-98.
[112] Wenbo Mao and Colin Boyd, “Towards formal analysis of security protocols”, Proceedings of the Computer Security Foundation Workshop VI, June 1993, pp: 147-158.
[113] E. A. Campbell, R. Safavi, Naini, P. A, “Pleasant Partial belief and probabilistic reasoning in the analysis of secure protocols,” In Proceedings of the Compute.
[114] 刘克龙, “安全 Linux 操作系统及安全 Web 系统的形式化建模与实现”, 中国科学院软件研究所博士论文,2001.
[115] Allen, R. and Garlan, D., “A case study in architectural modeling: the aegis system”, In Proceedings of the 8th International Workshop on Software Specification and Design (IWSSD8), 1998.
[116] E. Yu, “Modeling Strategic Relationships for Process Reengineering”, Ph. D. thesis, Department of Computer Science, University of Toronto, Canada, 1995.
[117] Boehm B. W., Ross R, “Theory W Software Project Management: Principles and Examples”, IEEE Trans on Software Engineering, 1989, pp: 902-916.
[118] Taylor R. N., Medvidovic N., Anderson K. N., Whitehead E. J. Jr., et al, “A component- and message-Based Architectural Style for GUI Software”, IEEE Trans on Software Engineering, 1996, Vol.22, Nov.6, pp: 390-406.
[119] Medvidovic N., Rosenblum D. S., Taylor R. N, “A language and environment for architecture-based software development and evolution”, Proceedings of the 21st International Conference on Software Engineering (ICSE'99), LosAngeles, May 16-22, 1999, pp: 44-53.
[120] Anne Dardenne, Axel van Lamweerde, Stephen. Fickas, “Goal-directed Requirements Acquisition. Science of Computer Programming”, Vol.20, 1993, pp: 3-50.
[121] Yu, E., Mylopoulos. J, “Why Goal-Oriented Requirements Engineering”, In Proceedings of the 4th International Workshop on Requirements Engineering: Foundations of Software Quality, 1998, pp: 15-22.
[122] Buhr, R.J.A., Casselman, R.S, “Use Case Maps for Object Oriented Systems”, Prentice-Hall, USA, 1995.
[123] D.M. Weiss, C.T.R. Lai, “Software Product Line Engineering: A Family-Based Software Development Process”, Addison-Wesley, 1999.
[124] D, Wile, “Residual Requirements and Architectural Residues”, Proceedings of the 5th International Symposium on Requirements Engineering (RE’01), Toronto, 2001, IEEE CS Press, pp: 194-201.
[125] J. Hammond, R. Rawlings, A. Hall, “Will it Work”, Proceedings of the 5th International Symposium on Requirements Engineering (RE’01), 2001, IEEE CS Press, pp: 102-109.
[126] A. Van Lamsweerde, “Goal-Oriented requirements engineering: A Guided Tour”, Proceedings of the 5th International Symposium on Requirements Engineering (RE’01), 2001, IEEE CS Press, pp: 249-261.
[127] L. Chung, B.A. Nixon, E. Yu, J, “Mylopoulos. Non-functional Requirements in Software Engineering, Kluwer Academic Publishers, 2000.
[128] E. Letier, A. Van Lamsweerde, “Agent-based Tactics for Goal-Oriented Requirements Elaboration”, Proceedings of 24th International Conference on Software Engineering, ACM Press, May 2001.
[129] Magee, J., Dulay, N., Eisenbach, S., and Kramer, J., “Specifying distributed software architectures”, In Proceedings of the 5th European Software Engineering Conference (ESEC 1995), Lecture Notes in Computer Science, Vol.989, Springer-Verlag, New York, 1995, pp: 137-153.
[130] Milner, R., “Communication and Concurrency”, Prentice-Hall, Englewood Cliffs, N.J., 1989.
[131] Moriconi, M., Qian, X., and Riemenschneider, R. A., “Correct architecture refinement”, IEEE Trans. Software Engineering, Vol.21, 1995, pp: 356-372.
[132] Gamma E, Helm R, Johnson R, Vlissides J., “Design patterns – Elements of Reusable Object-Oriented Software”, Addison-Wesley, Reading, Massachusetts, 1995.
[133] Mcllroy M., “Mass-Produced Software Components in Software Engineering Concepts and Techniques”, Petrocelli/Charter, Belgium, 1976, pp: 88-98.
[134] 刘文清,刘海峰,卿斯汉, “基于 Linux 开发安全操作系统的研究”, 计算机科学,2001,Vol. 28, No. 2, pp: 52-54.
[135] Inverardi, P. Wolf, A. L., and Yankelevich. D., “Static checking of system behaviors using derived component assumptions,” ACM Trans. Software. Eng. Method. Vol. 9, pp: 239-272, 2000.
[136] Inverardi, P. and Uchitel, S., “Proving deadlock freedom in component-based programming”, In Proceedings of the 4th International Conference on Approaches to Software Engineering (FASE 2001), Lecture Notes in Computer Science, Vol. 2029, Springer-Verlag, New York, pp: 60-75, 2001.
[137] Karmer, J. and Magee, J., “Exposing the skeleton in the coordination closet”, In Proceedingsof the 2nd International Conference on Coordination Models and Languages (COORDINATION 1997), Lecture Notes in Computer Science, Vol.1282, Springer-verlag, New York, 1997, pp: 18-31.
[138] Dean, T. R. and Cordy, J. R., “A syntactic theory of software architecture”, IEEE Trans. Software Engineering, Vol.21, 1995, pp: 302-313.
[139] Allen, R. and Garlan, D., “A case study in architectural modeling: the aegis system”, In Proceedings of the 8th International Workshop on Software Specification and Design (IWSSD8), 1998.
[140] Clarke, E. M., Long, D. E., McMillan, K. L., “Compositional model checking”, In Proceedings of the 4th IEEE International Symposium on Logic in Computer Science (LICS 1989), IEEE-CS Press, New York, 1989, pp: 353-362.
[141] Bernardo, M., Franze, F., “Architectural types revisited: extensible and/or connections”, In Proceedings of the 5th International Conference on Fundamental Approaches to Software Engineering (FASE 2002), Lecture Notes in Computer Science, Vol.2306, Springer, New York, 2002, pp: 113-128.
[142] Bernardo, M., Franze, F., “Exogenous and endogenous extensions of architectural types”, In Proceedings of the 5th International Conference on Coordination Models and Languages (COORDINATION 2002), Lecture Notes in Computer Science, Vol.2306, Springer, New York, 2002, pp: 44-55.
[143] Lavenberg, S. S., Ed, “Computer Performance Modeling Handbook”, Academic Press, Orlando, Fla., 1983.
[144] Balsamo, S., Bernardo, M. and Simeoni, M., “Combining stochastic process algebras and queuing networks for software architecture analysis”, In Proceedings of the 3rd International Workshop on Software and Performance (WOSP 2002), ACM, New York, 2002, pp: 190-202.
[145] Bernardo, M., Donatiello, L., and Ciancarini, P., “Stochastic process algebra: from an algebraic formalism to an architectural description language”, In Performance Evaluation of Complex Systems: Techniques and Tools, Calzarossa, M. C., and Tucci, S., Eds. Lecture Notes in Computer Science, Vol.2459, Springer-Verlag, New York, 2002, pp: 236-260.
[146] Schell, R. R., “Effectiveness- The Reason for a security kernel”, Proc. Nat1 Computer Conf., 1974, pp: 975-976.
[147] Dept. of Defense Standard, “Department of Defense Trusted Computer System Evaluation Criteria”, DoD5200.28-STD, GPO 1986-623-963, Dec.26, 1985.
[148] Commission of the European Communities, “Information Technology Security Evaluation Criteria (ITSEC)”, Provisional Harmonized Criteria: Version1.2, office for official Publications of the European Communities, Luxembourg, June 1991.
[149] Classified criteria for security protection of computer information system, GB 17859-1999, 13 September 1999(in Chinese).
[150] Hollingworth, Glaseman D S, Hopwood M. “Security test and evaluation tools: An approach to operating system security analysis”, Rand Corporation, Santa Monica, California: Technical Report P-5278, 1974.
[151] Abbott R P et al. “Security analysis and enhancement of computer operating systems”, NBSIR 76-1041, Nat1 Bureau of Standards, ICST, Gaithersburg, Md., Apr. 1976.
[152] Israel, H., “Design of Originator Controls in a Computer Systems: A Trusted Discretionary Access Control Mechanism”, Proc. 3rd Symp. Physical/Electronics Security, Armed Forces Communications and Electronics Assoc., Philadelphia, Aug. 1987, pp: 3k1-3k6.
[153] S. Osborn, “Mandatory access control and role-based access control revisited”, In Proceedings of the Second ACM Workshop on Role Based Control, 1996.
[154] Cetin Kaya Koc, MT5104 Computer Security Lecture3, http://www.cccure.org/Documents/Security_models/models.pdf.
[155] Bell, D. E. and L. J. Lapadula, “Secure Computer Systems: Mathematical Foundations”, Technical Report M74-244, The MITRE Corporation, Bedford, Massachusetts, May 1973.
[156] D. Batory and S. Omalley, “the Design and Implementation of Hierarchical Software Systems with Reusable Components”, ACM Transaction on Software Engineering and Methodology, 1992, Vol. 1, No. 4, pp: 355-398.
[157] K. Czarnecki and U. W. Eisenecker, “Components and generative programming”, Software engineering notes, 1999, Vol. 24, No. 6, pp: 2-19.
[158] M. Mezini and K. Lieberherr, “Adaptive plug-and-play Components for evolutionary software development”, ACM SIGPLAN Notes, 1998, Vol. 33, No. 10, pp: 97-116.
[159] 吴志刚,方滨兴,孙鹏,李亚萍,“一个安全、原子的电子商务协议及其形式化验证”,计算机研究与发展,Vol.37, No.7, July 2000, pp: 869-873.
[2] Keene, Jr. and Samuel, J., “Assuring Software Safety”, Proceedings Annual Reliability and Maintainability Symposium, 1992.
[3] 孙昌爱, 金茂忠, 刘超, “软件体系结构综述”, 软件学报, 2002, Vol.7, No.13, pp: 1228-1237.
[4] Oscar Nierstrasz and Theo Dirk Meijler, “Research Directions in Software Composition”, ACM Computing Surveys, Jun 1995, Vol.27, No.2, pp: 262-264.
[5] Boehm, B, “Engineering context (for software architecture)”, invited talk, In: Garlan, D., ed. Proceedings of the 1st International Workshop on Architecture for Software Systems Settle, New York, ACM Press, 1995, pp: 1-8.
[6] Shaw, M. and Garlan, D., “Software Architecture: Perspectives on an Emerging Discipline”, 1996, Prentice-Hall, Englewood Cliffs, New Jersey.
[7] Booch, G., “Software Components with Ada, Structures, Tools and Subsystems”, 1987, Benjamin/ Cummings Publishing Company, Menlo Park.
[8] Hugo Fierz. “The CIP Method: Component-and Model-Based Construction of Embedded Systems”, Software Engineering Notes, 1999, Vol.24, No 6, pp: 375-393.
[9] Abowd, G. D., Allen, R., and Garlan, D, “Formalizing style to understand descriptions of software architecture”, ACM Trans. Software Engineering, Math. 4, 1995, pp: 319-364.
[10] Colin Boyd, “Security Architectures Using Formal Methods”, IEEE Journal on Selected Areas in Communications, June 1993, Vol. 11, No. 5.
[11] 周之英,“现代软件工程——基本方法篇”,2000 年 1 月,第一版,科学出版社.
[12] 周莹新,艾波, “软件体系结构建模研究”, 软件学报,1998, Vol 9, pp: 867-872.
[13] ISO 7482-2, Information Process System—Open systems Interconnection Reference Security Architecture, 1988.
[14] David Garlan and Dewayne E. Perry, “Introduction to the Special Issue on Software Architecture”, IEEE Transactions on Software Engineering, Apr 1995, Vol.21, No.4, pp: 269-274.
[15] Devayne E. Perry, Alexander L. Wolf, “Foundation for the Study of Software Architecture,” ACM SIGSOFT, 1992, Vol.10, No.4.
[16] Nenad Medvidovic and Richard N. Taylor, “A Classification and Comparison Framework for Software Architecture Description Languages,” IEEE Transactions On Software Engineering, JAN. 2000, Vol.26, No.1.
[17] Shaw, M., Deline, R., Klein, D. V., Ross, T. L., Young, D. M., and Zelesnik, G.,“Abstractions for software architecture and tools to support them”, IEEE Transaction of Software Engineering, 1995, Vol.21, pp: 314-335.
[18] R. Allen, D. Garlan, “A Formal Basis for Architectural Connection,” ACM Trans. Software Engineering and Methodology, Vol.6, No.3, July 1997, pp: 213-249.
[19] Luckham, D., Lary, C., and Augustin, M, “ Specification and analysis of system architecture using rapide”, IEEE Transactions on Software Engineering 1995, Vol.21, No.4, pp: 336-355.
[20] J. Magee, J. Kramer, “Dynamic Structure in Software Architectures”, Proc. ACM SIGSOFT’96, Oct 1996, pp: 3-14.
[21] J. M. Spivey, “the Z Notation: a Reference Manual”, 1989, Englewood Cliffs, NJ: Prentice-Hall.
[22] 张广泉, “基于 XYZ/E 的软件体系结构描述语言研究”,计算机科学,2000,Vol. 27, No. 9, pp: 155-157
[23] 唐稚松等, “时序逻辑程序设计与软件工程”,2002 年 5 月,北京,科学出版社.
[24] 张广泉,唐稚松, “一种新的软件体系结构描述语言”,中国博士后学术大会论文集,2001年 2 月,北京,科学出版社.
[25] 骆华俊,唐稚松,郑建丹,“可视化体系结构描述语言 XYZ/ADL”,软件学报,2000,Vol. 11, No. 8, pp: 1024-1029.
[26] Abowd G., Allen R., and Garlan, D, “Using style to understand description of Software Architecture”, ACM SIGSOFT Software Engineering Notes, 1993, pp: 9-20.
[27] D. Garlan, “An Introduction to the Aesop System”, July 1995.
[28] http://www.cs.cmu.edu/afs/cs/project/table/aesop/html/aesop_overview.ps.
[29] R. N. Taylor, “Using Object-Oriented Typing to Support Architectural Design in the C2 Style,” Proc. ACM SIGSOFT’96, Oct 1996. pp: 24-32.
[30] M. Moriconi, X. Qian, R. A. Riemenschanaider, “Correct Architecture Refinement,” IEEE Trans Software Eng., Apr 1995, Vol.21, No.4, pp: 356-372.
[31] M. Shaw, R. Deline, G. Zelesnik, “Abstractions and Implementations for Architectural Connections,” Proc. Third Int’l Conf. Configurable Distributed System, May 1996.
[32] S. Vestal, “MetaH Programmer’s Manual, Version 1.09,” technical report, Honeywell Technology Center, April 1996.
[33] Allen R., Garlan D, “Formal Connectors”, Technology Report, CMU-CS-94-115, Pittsburg: Carnegie Mellon University, 1994.
[34] D. C. Luckham, J. Vera, “Event-Based Architecture Definition Language,” IEEE Trans. Software Eng., Sept 1995, Vol.21, No.9, pp: 717-734.
[35] D. Garlan, R. Monroe, D. Wile, ”ACME: An Architecture Description Interchange Language,” Proc.CASCON’97, Nov 1997.
[36] M. M. Gorlick and R. R. Razouk, “Using Weaves for Software Construction and Analysis,”Proc.13th Int’l Conf. Software Eng. (ICSE13), May 1991, pp: 23-34.
[37] Jeremy Bryans, Steve Schneider, “CSP, PVS and a recursive authentication protocol”, In DIMACS Workshop on Design and Formal Verification of Security Protocols, September 1997.
[38] Hoare, C. A. R., “Communicating Sequential Process”, 1985, Prentice Hall, Englewood Cliffs, New Jersey.
[39] Jan Wessels, “Applications of BAN-LOGIC”, IPA Spring Days on Security, April 18-20, 2001.
[40] M. Nail, G. Ostrolenk, M. Tobin, “Lessons from using Z to Specify a Software Tool”, IEEE Trans. Soft. Eng., 1998, Vol.24, No.1, pp: 15-23.
[41] 屈延文, “形式化语义学基础与形式说明”, 1998, 科学出版社.
[42] 陆汝铃, “形式语义”, 1992, 科学出版社.
[43] R. Milner, “A Calculus of Communication System”, LNCS92, 1980, Springer-Verlag.
[44] 郑红军,张乃孝, “软件开发中的形式化方法”, 计算机科学, 1997, Vol.24, No.6.
[45] Leonor Barroca, Jon Hall, Patrick Hall, “Software Architecture Advance and Applications”, 2000, Springer-Verlag, London.
[46] 张家晨,冯铁,陈伟,金淳兆, “基于主动连接件的软件体系结构及其描述方法”, 软件学报, 2000, Vol.11, pp: 1047-1052.
[47] Clarke, E.M., Grumberg, O., and Peled, D. A, “Model Checking”, 1999, MIT Press.
[48] M. Burrows, M. Abadi, and R. Needham, “A logic of authentication”, ACM Transactions on Computer Systems, 8, February 1990.
[49] D. Kindred and J. M. Wing, “Fast, automatic checking of security protocols”, In USENIX 2nd Workshop on Electronic Commerce, 1996.
[50] Balsamo, S., Bernardo, M. and Simeoni, M., “Combining stochastic process algebras and queuing networks for software architecture analysis”, In Proceedings of the 3rd International Workshop on Software and Performance (WOSP 2002), ACM, New York, 2002, pp: 190-202.
[51] C. Meadows, “A System for the specification and analysis of key management protocols”, in Proc. 1991 IEEE Computer Society. Symp, Security Privacy, IEEE Computer Society Press, 1991, pp: 182-195.
[52] R. A. Rueppel, “A formal approach to security architectures”, in Proc. Eurocrypt91. New York: Springer-Verlag, 1991.
[53] L. Gong, R. Needham, and R. Yahalom, “Reasoning about belief in cryptographic protocols”, in Proc 1990 IEEE Computer Society. Symp, Security Privacy, IEEE Computer Society Press, 1990, pp: 234-248.
[54] M. Burrows, M. Abadi, R. Needham, “A Logic of authentication”, ACM Trans. ComputerSystem, Feb 1990, Vol. 8, No. 1, pp: 18-36.
[55] R. Kailar and V. D. Gilgor, “on belief evolution in authentication protocols”, in Proc. Computer Security Foundations Workshop IV. New York: IEEE Press, 1991, pp: 103-116.
[56] M. Bernardo, P. Ciancarini, L. Donatiello, “Architecture families of software systems with process algebras.” ACM Transactions on Software Engineering and Methodology, October 2002, Vol.11, No.4.
[57] Apt. K. R., “Ten years of Hoare Logic: A Survey”, ACM Transaction on Programming Languages and Systems, 1981, Vol.3, No.4, pp: 431-483.
[58] Constable, et al, “Implementing Mathematics of with Nuprl Proof Development System”, New Jersey: Prentice-Hall, Englewood Cliffs, 1986.
[59] E. M. Clarke and J. M. Wing, “Formal Methods: State of the Art and Future Directions”, ACM Computing Surveys, 1996, Vol.28, No.4, pp: 626-643.
[60] J. Mitchell, M. Mitchell, U. Stern, “Automated analysis of cryptographic protocols using Murφ”, In Proceedings of the 1997 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, May 1997, pp: 141--151.
[61] M. Debbabi, M. Mejri, N. Tawbi, and I. Yahmadi, “A new algorithm for the automatic verification of authentication protocols: From specifications to flaws and attack scenarios”, In DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997.
[62] Lin Liu, Eric Yu, John Mylopoulos, “Analyzing Security Requirements as Relationships among Strategic Actors”, Proceeding of 20th International Conference on Conceptual Modeling (ER-2001), Yokohama, Japan, November 27-30, 2001.
[63] Riccardo Focardi and Roberto Gorrieri, “the Compositional Security Checker: a Tool for the Verification of Information Flow Security Properties”, IEEE Trans on Software Engineering, Vol. 23, No. 9, September 1997.
[64] C. R. Tsal, V. D. Gilger, and C. S. Chanclesekaran, “on the discipline of covert Storage channels in secure systems”, IEEE Trans on Software Eng., June 1990, pp: 569-580.
[65] P. Y., A. Ryan, “A CSP Formulation of Noninterference”, Proc Computer Security Foundation Workshop, Franconia, 1990, IEEE CS Press.
[66] A. W. Rosore, J. C. P. Woodcook and L. Wolf, “Noninterference through Determination”, Proc European Symposium, Research in Computer Security 1994 (ESORJCS94), pp: 33-53.
[67] A. W. Rosore, “ Model Checking CSP——A classical Mind”, 1994, Prentice Hall.
[68] 傅建明, “基于 Ada 并行计算模型的安全性研究”, 武汉大学博士学位论文,2000 年 4月.
[69] Bashar Nuseibeh, “Weaving together Requirements and Architectures.” IEEE Computer, 2001, Vol. 34, No. 3, pp: 115-117.
[70] John G. Hall, Michael Jackson, Robin C. Laney, Bashar Nuseibeh, Lucia Rapanotti,“Relating Software requirements and architectures using problem frames”, Proceedings of IEEE International Requirements Engineering Conference (RE'02), Essen, 2002, Vol. 9,Vol. 13, pp: 137-144.
[71] K. Heninger, D. L. Parnas, J. E. Shore, J. W. Kallander, “Software requirements for the A7E aircraft”, TR3876, 1978, Naval Research lab, Washington, DC.
[72] C. L. Heitmeyer, R. D. Jeffords, B. G. Labaw, “Automated consistency checking of requirements specifications”, ACM Transactions on Software Engineering and Methodology, 1996, Vol. 5,Nov. 3, pp: 231-261.
[73] Kolp M. Castro, J. Mylopoulos, “A Social Organization Perspective on Software Architectures”, In Proc. of the First Int. Workshop From Software Requirements to Architectures, STRAW'01, Toronto, May 2001, pp: 5-12.
[74] J. Mylopoulos, A. Borgida, M. Jarke, M. Koubarakis, “Telos: Representing Knowledge About Information Systems”, ACM Trans. Info. Sys, Vol.8, Nov.4, Oct.1990, pp: 325-362.
[75] P. Grunbacher, A. Egyed, N. Medvidovic, “Reconciling software requirements and architectures: The CBSP Approach”, Proceedings of the 5th International Symposium on Requirements Engineering (RE’01), IEEE CS Presss2001, pp: 202-211.
[76] Alexander Egyed, Paul Grünbacher, Nenad Medvidovic, “Refinement and Evolution Issues in Bridging requirements and architecture – the CBSP approach”, IEEE Trans on Software Engineering, 1996, Vol.22, Nov.6, pp: 390-406.
[77] Boehm B., Gruenbacher P, “Supporting Collaborative Requirements Negotiation: The EasyWinWin Approach”, Proceeding of SCS on Virtual Worlds and Simulation, San Diego, 2000.
[78] Medvidovic N., Gruenbacher P., Egyed A., Boehm B., “Software Lifecycle Connectors: Bridging Models across the Lifecycle”, the 23rd International Conference on Software Engineering (ICSE 2001), Toronto, 2001.
[79] Brandozzi M., Perry D.E, “Transforming Goal-Oriented Requirement Specifications into Architecture Prescriptions”, ICSE 2001.
[80] Liu, L., Yu. E, “From Requirements to Architectural Design - Using Goals and Scenarios”, ICSE-2001 Workshop: From Software Requirements to Architectures (STRAW 2001) Toronto, Canada, May 2001, pp: 22-30.
[81] Klaus Pohl, Mathias Brandenburg, Alexander Gulich, “Integrating requirement and architecture information: a scenario and meta-model based approach”, Paper of the Seventh International Workshop on Requirements Engineering: Foundation for Software Quality (REFSQ), June 2001.
[82] 魏峻, “基于规范的软件形式方法的研究一种时序逻辑的框架”, 武汉大学博士学位论文,1997.
[83] N. Medvidovic and R. N. Taylor, “Exploiting architectural style to develop a family of applications”, IEE Proceedings Software Engineering, Oct.-Dec.1997, Vol.144, No.5-6, pp: 237-248.
[84] Richard N. Taylor, Nenad Medvidovic, Kenneth M, Anderson, et al., “A Component-and Message-Based Architectural Style for GUI Software”, IEEE Transactions on Software Engineering, June 1996, Vol.22, No.6, pp: 390-406.
[85] 鲍敢峰,尤晋元, “软件体系结构的图形语法”, 计算机工程, Dec 1997, Vol.23, Special Issue.
[86] Andersen, H. R, “Partial model checking”, In Proceedings of the 10th IEEE International Symposium on Logic in Computer Science (LICS1995), 1995, IEEE-CS Press, New York, pp: 398-407.
[87] Bruno Dutertre and Steve Schneider, “Using a PVS Embedding of CSP to Verify Authentication Protocols”, In Theorem Proving in Higher Order Logics, number 1275 in LNCS. 1997, Springer-Verlag.
[88] Fu. K. S. and Booth. T. H, “Grammatical Inference Introduction and Survey”, IEEE Trans. On SMC-5, 1975, pp: 395-409.
[89] A.D. Rubin and P. Honeyman, “Formal Methods for the Analysis of Authentication Protocols”, Technical Report Technical report 93-7, Technical Report, Center for Information Technology Integration, 1993. University of Michigan.
[90] 邵维忠,麻志毅,张文娟,孟祥文(译), “UML 用户指南”, 2001, 北京, 机械工业出版社.
[91] 邵维忠,梅宏, “统一建模语言 UML 述评”, 计算机研究与发展,1999, Vol. 36, No. 4, pp: 1-8.
[92] OMG. “OMG Unified Modeling Language Specification 1.3,1.4”, http://www.omg.org/uml/
[93] 邵维忠,蒋严冰,麻志毅, “UML 现存的问题和发展道路”, Apr. 2003, Vol. 40, No. 4, pp: 509-515.
[94] 蒋慧, 林东, 谢希仁, “UML 状态机的形式语义”,软件学报, 2002, Vol.23, No.12, pp: 2244-2250.
[95] Bernardo, M., Ciancarini, P., and Donatiello, L., “On the formalization of architectural types with process algebras”, In Proceedings of the 8th ACM International Symposium on the Foundations of Software Engineering (FSE-8), 2000, ACM, New York, pp: 140-148.
[96] Bernardo, M., Ciancarini, P., and Donatiello, L., “Detecting architectural mismatches in process algebraic descriptions of software systems”, In Proceedings of the 1st Working IEEE/IFIP Conference on Software Architecture (WICSA 2001), 2001, IEEE-CS Press, New York, pp: 77-86.
[97] Bernardo, M., Donatiello, L., and Ciancarini, P., “Stochastic process algebra: from analgebraic formalism to an architectural description language”, In Performance Evaluation of Complex Systems: Techniques and Tools, Calzarossa, M. C., and Tucci, S., Eds, Lecture Notes in Computer Science, 2002, Vol.2459, Springer-Verlag, New York, pp: 236-260.
[98] Bernardo, M., Franze, F., “Architectural types revisited: extensible and/or connections”, In Proceedings of the 5th International Conference on Fundamental Approaches to Software Engineering (FASE 2002), Lecture Notes in Computer Science, 2002, Vol.2306, Springer, New York, pp: 113-128.
[99] Bernardo, M., Franze, F., “Exogenous and endogenous extensions of architectural types”, In Proceedings of the 5th International Conference on Coordination Models and Languages (COORDINATION 2002), Lecture Notes in Computer Science, 2002, Vol.2306, Springer, New York, pp: 44-55.
[100] Bravetti, M. and Bernardo, M., “Compositional asymmetric co-operations for process algebras with probabilities, priorities, and time”, In Proceedings of the 1st Workshop on Models for Time Critical Systems (MTCS 2000), ENTCS, 2000, Vol.39, No.3, Elsevier, Amsterdam, The Netherlands.
[101] Colin Boyd and Wenbo Mao, “On a limitation of ban logic”, Advances in Cryptology: Proceedings of Eurocrypt 93, 1993, pp: 240—247.
[102] Clarke, E. M., Long, D. E., McMillan, K. L., “Compositional model checking”, In Proceedings of the 4th IEEE International Symposium on Logic in Computer Science (LICS 1989), IEEE-CS Press, New York, 1989, pp: 353-362.
[103] David M., “Kronecker products and shuffle algebras”, IEEE Trans, Computer, 1981, Vol.30, pp: 116-125.
[104] Dean, T. R. and Cordy, J. R., “A syntactic theory of software architecture”, IEEE Trans. Software Engineering, 1995, Vol.21, pp: 302-313.
[105] De Remer, F. and Kron, H. H., “Programming-in-the-large versus programming-in-the-small”, IEEE Trans. Software Engineering, 1976, Vol.2, pp: 80-86.
[106] Van Glabbeek, R. J., “The linear time-branching time spectrum I The semantics of concrete, sequential processes”, In Handbook of Process Algebra, Bergstra, J. A., Ponse, A., and Smolka, S. A., Eds, Elsevier, 2001, pp: 3-99.
[107] Kramer, J. and Magee, J., “Exposing the skeleton in the coordination closet”, In Proceedings of the 2nd International Conference on Coordination Models and Languages (COORDINATION 1997), Lecture Notes in Computer Science, Vol.1282, Springer-verlag, New York, 1997, pp: 18-31.
[108] Lavenberg, S. S., Ed, “Computer Performance Modeling Handbook”, Academic Press, Orlando, Fla, 1983.
[109] Martin Abadi and Mark Tuttle, “A Semantics for a Logic of Authentication”, In Proceedingsof the Tenth ACM Symposium on Principles of Distributed Computing, ACM Press, August 1991, pp: 201--216.
[110] L. Gong, R. Needham, and R. Yahalom, “Reasoning about Belief in Cryptographic Protocols”, Proc. of the IEEE 1990 Symp on Security and Privacy Oakland, California, May 1990, pp: 234-248.
[111] Klaus Grader, Einar Snekkenes, “Applying a Formal Analysis Technique to the CCITT X.509 Strong Two-Way Authentication Protocol”, Journal Of Cryptology, 1991, Vol.3, pp: 81-98.
[112] Wenbo Mao and Colin Boyd, “Towards formal analysis of security protocols”, Proceedings of the Computer Security Foundation Workshop VI, June 1993, pp: 147-158.
[113] E. A. Campbell, R. Safavi, Naini, P. A, “Pleasant Partial belief and probabilistic reasoning in the analysis of secure protocols,” In Proceedings of the Compute.
[114] 刘克龙, “安全 Linux 操作系统及安全 Web 系统的形式化建模与实现”, 中国科学院软件研究所博士论文,2001.
[115] Allen, R. and Garlan, D., “A case study in architectural modeling: the aegis system”, In Proceedings of the 8th International Workshop on Software Specification and Design (IWSSD8), 1998.
[116] E. Yu, “Modeling Strategic Relationships for Process Reengineering”, Ph. D. thesis, Department of Computer Science, University of Toronto, Canada, 1995.
[117] Boehm B. W., Ross R, “Theory W Software Project Management: Principles and Examples”, IEEE Trans on Software Engineering, 1989, pp: 902-916.
[118] Taylor R. N., Medvidovic N., Anderson K. N., Whitehead E. J. Jr., et al, “A component- and message-Based Architectural Style for GUI Software”, IEEE Trans on Software Engineering, 1996, Vol.22, Nov.6, pp: 390-406.
[119] Medvidovic N., Rosenblum D. S., Taylor R. N, “A language and environment for architecture-based software development and evolution”, Proceedings of the 21st International Conference on Software Engineering (ICSE'99), LosAngeles, May 16-22, 1999, pp: 44-53.
[120] Anne Dardenne, Axel van Lamweerde, Stephen. Fickas, “Goal-directed Requirements Acquisition. Science of Computer Programming”, Vol.20, 1993, pp: 3-50.
[121] Yu, E., Mylopoulos. J, “Why Goal-Oriented Requirements Engineering”, In Proceedings of the 4th International Workshop on Requirements Engineering: Foundations of Software Quality, 1998, pp: 15-22.
[122] Buhr, R.J.A., Casselman, R.S, “Use Case Maps for Object Oriented Systems”, Prentice-Hall, USA, 1995.
[123] D.M. Weiss, C.T.R. Lai, “Software Product Line Engineering: A Family-Based Software Development Process”, Addison-Wesley, 1999.
[124] D, Wile, “Residual Requirements and Architectural Residues”, Proceedings of the 5th International Symposium on Requirements Engineering (RE’01), Toronto, 2001, IEEE CS Press, pp: 194-201.
[125] J. Hammond, R. Rawlings, A. Hall, “Will it Work”, Proceedings of the 5th International Symposium on Requirements Engineering (RE’01), 2001, IEEE CS Press, pp: 102-109.
[126] A. Van Lamsweerde, “Goal-Oriented requirements engineering: A Guided Tour”, Proceedings of the 5th International Symposium on Requirements Engineering (RE’01), 2001, IEEE CS Press, pp: 249-261.
[127] L. Chung, B.A. Nixon, E. Yu, J, “Mylopoulos. Non-functional Requirements in Software Engineering, Kluwer Academic Publishers, 2000.
[128] E. Letier, A. Van Lamsweerde, “Agent-based Tactics for Goal-Oriented Requirements Elaboration”, Proceedings of 24th International Conference on Software Engineering, ACM Press, May 2001.
[129] Magee, J., Dulay, N., Eisenbach, S., and Kramer, J., “Specifying distributed software architectures”, In Proceedings of the 5th European Software Engineering Conference (ESEC 1995), Lecture Notes in Computer Science, Vol.989, Springer-Verlag, New York, 1995, pp: 137-153.
[130] Milner, R., “Communication and Concurrency”, Prentice-Hall, Englewood Cliffs, N.J., 1989.
[131] Moriconi, M., Qian, X., and Riemenschneider, R. A., “Correct architecture refinement”, IEEE Trans. Software Engineering, Vol.21, 1995, pp: 356-372.
[132] Gamma E, Helm R, Johnson R, Vlissides J., “Design patterns – Elements of Reusable Object-Oriented Software”, Addison-Wesley, Reading, Massachusetts, 1995.
[133] Mcllroy M., “Mass-Produced Software Components in Software Engineering Concepts and Techniques”, Petrocelli/Charter, Belgium, 1976, pp: 88-98.
[134] 刘文清,刘海峰,卿斯汉, “基于 Linux 开发安全操作系统的研究”, 计算机科学,2001,Vol. 28, No. 2, pp: 52-54.
[135] Inverardi, P. Wolf, A. L., and Yankelevich. D., “Static checking of system behaviors using derived component assumptions,” ACM Trans. Software. Eng. Method. Vol. 9, pp: 239-272, 2000.
[136] Inverardi, P. and Uchitel, S., “Proving deadlock freedom in component-based programming”, In Proceedings of the 4th International Conference on Approaches to Software Engineering (FASE 2001), Lecture Notes in Computer Science, Vol. 2029, Springer-Verlag, New York, pp: 60-75, 2001.
[137] Karmer, J. and Magee, J., “Exposing the skeleton in the coordination closet”, In Proceedingsof the 2nd International Conference on Coordination Models and Languages (COORDINATION 1997), Lecture Notes in Computer Science, Vol.1282, Springer-verlag, New York, 1997, pp: 18-31.
[138] Dean, T. R. and Cordy, J. R., “A syntactic theory of software architecture”, IEEE Trans. Software Engineering, Vol.21, 1995, pp: 302-313.
[139] Allen, R. and Garlan, D., “A case study in architectural modeling: the aegis system”, In Proceedings of the 8th International Workshop on Software Specification and Design (IWSSD8), 1998.
[140] Clarke, E. M., Long, D. E., McMillan, K. L., “Compositional model checking”, In Proceedings of the 4th IEEE International Symposium on Logic in Computer Science (LICS 1989), IEEE-CS Press, New York, 1989, pp: 353-362.
[141] Bernardo, M., Franze, F., “Architectural types revisited: extensible and/or connections”, In Proceedings of the 5th International Conference on Fundamental Approaches to Software Engineering (FASE 2002), Lecture Notes in Computer Science, Vol.2306, Springer, New York, 2002, pp: 113-128.
[142] Bernardo, M., Franze, F., “Exogenous and endogenous extensions of architectural types”, In Proceedings of the 5th International Conference on Coordination Models and Languages (COORDINATION 2002), Lecture Notes in Computer Science, Vol.2306, Springer, New York, 2002, pp: 44-55.
[143] Lavenberg, S. S., Ed, “Computer Performance Modeling Handbook”, Academic Press, Orlando, Fla., 1983.
[144] Balsamo, S., Bernardo, M. and Simeoni, M., “Combining stochastic process algebras and queuing networks for software architecture analysis”, In Proceedings of the 3rd International Workshop on Software and Performance (WOSP 2002), ACM, New York, 2002, pp: 190-202.
[145] Bernardo, M., Donatiello, L., and Ciancarini, P., “Stochastic process algebra: from an algebraic formalism to an architectural description language”, In Performance Evaluation of Complex Systems: Techniques and Tools, Calzarossa, M. C., and Tucci, S., Eds. Lecture Notes in Computer Science, Vol.2459, Springer-Verlag, New York, 2002, pp: 236-260.
[146] Schell, R. R., “Effectiveness- The Reason for a security kernel”, Proc. Nat1 Computer Conf., 1974, pp: 975-976.
[147] Dept. of Defense Standard, “Department of Defense Trusted Computer System Evaluation Criteria”, DoD5200.28-STD, GPO 1986-623-963, Dec.26, 1985.
[148] Commission of the European Communities, “Information Technology Security Evaluation Criteria (ITSEC)”, Provisional Harmonized Criteria: Version1.2, office for official Publications of the European Communities, Luxembourg, June 1991.
[149] Classified criteria for security protection of computer information system, GB 17859-1999, 13 September 1999(in Chinese).
[150] Hollingworth, Glaseman D S, Hopwood M. “Security test and evaluation tools: An approach to operating system security analysis”, Rand Corporation, Santa Monica, California: Technical Report P-5278, 1974.
[151] Abbott R P et al. “Security analysis and enhancement of computer operating systems”, NBSIR 76-1041, Nat1 Bureau of Standards, ICST, Gaithersburg, Md., Apr. 1976.
[152] Israel, H., “Design of Originator Controls in a Computer Systems: A Trusted Discretionary Access Control Mechanism”, Proc. 3rd Symp. Physical/Electronics Security, Armed Forces Communications and Electronics Assoc., Philadelphia, Aug. 1987, pp: 3k1-3k6.
[153] S. Osborn, “Mandatory access control and role-based access control revisited”, In Proceedings of the Second ACM Workshop on Role Based Control, 1996.
[154] Cetin Kaya Koc, MT5104 Computer Security Lecture3, http://www.cccure.org/Documents/Security_models/models.pdf.
[155] Bell, D. E. and L. J. Lapadula, “Secure Computer Systems: Mathematical Foundations”, Technical Report M74-244, The MITRE Corporation, Bedford, Massachusetts, May 1973.
[156] D. Batory and S. Omalley, “the Design and Implementation of Hierarchical Software Systems with Reusable Components”, ACM Transaction on Software Engineering and Methodology, 1992, Vol. 1, No. 4, pp: 355-398.
[157] K. Czarnecki and U. W. Eisenecker, “Components and generative programming”, Software engineering notes, 1999, Vol. 24, No. 6, pp: 2-19.
[158] M. Mezini and K. Lieberherr, “Adaptive plug-and-play Components for evolutionary software development”, ACM SIGPLAN Notes, 1998, Vol. 33, No. 10, pp: 97-116.
[159] 吴志刚,方滨兴,孙鹏,李亚萍,“一个安全、原子的电子商务协议及其形式化验证”,计算机研究与发展,Vol.37, No.7, July 2000, pp: 869-873.