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

Aspect-Oriented Distributed Formal Specification Language

分布式系统复杂性的不断增加以及对可配置性和可重用性要求的不断提高,需要面向方面软件工程方法的支持,而形式化方法能保证分布式系统的正确性。本文对分布式规格说明语言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.