一种构件系统重新配置协议的关系逻辑模型  

A Relational Logic Model for the Reconfiguration Protocol of Component-based Systems

作　　者：罗奇鸣[1] 

机构地区：[1]中国科学技术大学计算机科学与技术学院,合肥230027

出　　处：《小型微型计算机系统》2014年第12期2686-2690,共5页Journal of Chinese Computer Systems

基　　金：MOE-MS多媒体计算与通信实验室基金项目(07122807)资助

摘　　要：基于构件的软件系统在运行过程中需要适应环境和用户需求的变化对自身的结构进行动态的重新配置.本文提出了一个用形式化语言Alloy实现的求解重新配置协议的关系逻辑模型.该模型定义了构件和连接的各种状态,状态之间的转换操作,和每种操作的前置和后置条件.这些前置和后置条件具体实现了保证系统一致性的不变式.在利用Alloy分析器验证了该模型的一致性的基础上,进一步将其转换成一个可以自动生成重新配置协议的多项式时间算法.与定理证明器相比,Alloy模型的修改和验证更加简便.Component-based software systems need to do dynamic reconfiguration at runtime in order to adapt to changing environments and user requirements. This paper proposes a relational logic model for solving reconfiguration protocols, which is implemented in a formal language Alloy. The model defines the following ： the states of components, the states of links among components, state transitions for components and links, and the pre-conditions and post-conditions for each state transition. These pre-conditions and postconditions concretely specify the invariants for ensuring architectural consistency. Based on verification of its consistency by the Alloy analyzer, the model is further transformed into a polynomial - time algorithm for automatically generating a reconfiguration protocol. It is much easier to modify and verify models built in Alloy than those built in theorem provers.

关 键 词：构件 重新配置 关系逻辑 ALLOY 软件体系结构 

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