基于线性时序逻辑的动态软件体系结构模型验证

摘要

如何有效地保证软件体系结构能够正确地进行动态演化是目前软件工程领域中一个亟待解决的问题。模型验证是一种关于系统性质验证的算法方法,它通常采用状态空间搜索的方法来检查一个给定的计算模型是否满足用某个时序逻辑公式描述的特定性质。模型验证的复杂性主要依赖于系统状态空间大小,所以模型验证方法所面临的最大问题是状态空间爆炸和内存不足。针对大规模动态软件体系结构模型验证方法的不足,本文提出了一种基于线性时序逻辑的模块化模型验证方法,从系统组成模块和整体系统两个不同层次探讨了验证动态软件体系结构的方法,给出了相应的实现算法,并结合实例说明了本方法的实用性。