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

摘要

基于构件的软件系统在运行过程中需要适应环境和用户需求的变化对自身的结构进行动态的重新配置.本文提出了一个用形式化语言Alloy实现的求解重新配置协议的关系逻辑模型.该模型定义了构件和连接的各种状态,状态之间的转换操作,和每种操作的前置和后置条件.这些前置和后置条件具体实现了保证系统一致性的不变式.在利用Alloy分析器验证了该模型的一致性的基础上,进一步将其转换成一个可以自动生成重新配置协议的多项式时间算法.与定理证明器相比,Alloy模型的修改和验证更加简便.