面向方面分布式系统形式化规格说明语言  

Aspect-Oriented Distributed Formal Specification Language

作　　者：陈广明[1] 张立臣[2] 陈生庆[1] 

机构地区：[1]嘉应学院计算机系,梅州514015 [2]广东工业大学计算机学院,广州510090

出　　处：《计算机科学》2007年第6期258-261,共4页Computer Science

基　　金：国家自然科学基金(No.60474072;No.60174050);广东省自然科学基金(No.04009465;No.010059);广东省高校自然科学研究项目(No.Z03024)基金资助。

摘　　要：分布式系统复杂性的不断增加以及对可配置性和可重用性要求的不断提高,需要面向方面软件工程方法的支持,而形式化方法能保证分布式系统的正确性。本文对分布式规格说明语言Ocsid进行了面向方面的扩展,讨论了面向方面的Ocsid的框架结构、语法要求、方面的联结和功能接口。定义了面向方面的Ocsid规格说明语言中叠加和组合的形式化描述,该形式化描述覆盖了各个精化阶段,使精化体系的各个独立视点被协调地组合,并能形式化地验证规格说明的时态属性和系统行为。本文的工作针对的是分布式系统的形式化规格说明,提出了面向方面Ocsid的形式基础和方面扩展,其基本思想同样适用于更一般的情况。Increasing complexity of distributed system, and demands for enabling their configurability and reusability are strong motivations for aspect-oriented, and correctness of distributed systems requires that formal development methods are taken during software development cycle. This paper attempts to establish an aspect-oriented formal development method for distributed systems with the aspect oriented extension of Ocsid. The framework, syntax, weaving aspects, and interface of function are discussed in the paper. We present a formalization of how specifications are constructed using superposition and composition in the Ocsid specification language. The formalization covers stepwise refinement using superposition and composition of independent refinements. Independent views of a refinement hierarchy are reconciled. In the formalization, we can to construct formally verified temporal properties and action of distributed systems. The work that formalizaion and refactoring of Ocsid has been done in the context of aspect oriented formal specification of distributed systems,but we believe the ideas to be useful in a more general setting as well.

关 键 词：面向方面 分布式系统 形式化方法 Ocsid 

分 类 号：TP312[自动化与计算机技术—计算机软件与理论]