软件组件的共代数语意

Coalgebraic Semantics for Software Components

基于组件的软件开发能够有效提高软件开发的质量与效率。但在一些安全关键的领域,由于形式化模型与方法的缺乏,使得基于组件的开发方法不能成功应用。为了得到一套完整的形式化模型用于描述软件组件及其组成的系统,首先必须对软件组件的形式化语意进行定义。文中提出了一种基于共代数概念的语意,使得满足接口和组件规约的组件对应于一个具体的共代数,并由此推导出了接口和组件的功能契约的形式语意以及接口依赖的共代数语意。通过对一个简单的堆栈进行规约,体现了这种方法的可应用性。

The component-based software development is regarded as an effective solution to improve the quality and productivity of software development,lack of formal models and methods supporting hampering its application in some safety-critical areas.To formally specify software components and composed system,a formal semantics of software components is required.In this paper,based on coalgebra notions,treated a component which implements specifications as a concrete coalgebra and thus reasoned out the formal semantics of these specifications.The coalgebraic semantics for components dependencies on interfaces was also involved.The applicability of our approach was demonstred by a good simple example.