去中心化系统中自适应行为形式化验证的案例研究

自适应是管理现代软件系统复杂性的一种有前景的方法。自适应系统能够自主适应内部动态和环境变化，以实现特定的质量目标。我们特别关注去中心化自适应系统，其中集中式自适应控制不可行。自适应系统（特别是那些具有去中心化自适应控制的系统）面临的一个重要挑战是提供关于预期运行时质量的保证。本文介绍了一个案例研究，其中我们使用模型检测来验证去中心化自适应系统的行为属性。具体而言，我们贡献了一个去中心化交通监控系统的形式化架构模型，并证明了若干关于灵活性和鲁棒性的自适应属性。为了对系统中的主要进程进行建模，我们使用了时间自动机（timed automata），并使用时序计算树逻辑（timed computation tree logic）来规范所需属性。我们使用 Uppaal 工具来指定系统并验证灵活性和鲁棒性属性。