基于组件系统的运行时强制
软件工程
2014-06-24 v1
摘要
运行时强制是一种日益流行且有效的动态验证技术，旨在利用所谓的强制监控器确保系统相对于形式规范的正确运行时行为。本文介绍了在 BIP（行为、交互和优先级）框架中建模的基于组件系统 (CBS) 上的规范运行时强制。BIP 是一个用于异构系统形式化构建的强大且富有表现力的基于组件的框架。然而，由于 BIP 的表现力，在设计时强制复杂的行为属性仍然困难。首先，我们提出了一个针对 CBS 的理论运行时强制框架，根据系统允许偏离属性的观察步数（即 k 步强制性的概念），划分了可强制属性集（即可被强制的属性）的层次结构。为了确保初始系统的正确执行与受监控系统之间的观察等价性，我们证明了：i) 使用我们的监控器时，仅应在 CBS 上强制 stutter-invariant 属性；ii) 安全属性是 1 步可强制的。给定针对某些 1 步可强制规范的抽象强制监控器（作为有限状态机），我们在给定的 BIP 系统的相关位置进行形式化插桩以集成该监控器。在运行时，监控器观察并自动避免系统行为中相对于规范的任何错误。我们的方法已完全实现在一个可用工具中，我们使用该工具：i) 避免了哲学家进餐基准测试中的死锁发生；ii) 确保了机器人在地图上的正确放置。
引用
@article{arxiv.1406.5708,
title = {Runtime Enforcement for Component-Based Systems},
author = {Hadil Charafeddine and Khalil El-Harake and Yliès Falcone and Mohamad Jaber},
journal= {arXiv preprint arXiv:1406.5708},
year = {2014}
}
备注
arXiv admin note: text overlap with arXiv:1109.5505 by other authors