监控累积代价属性
软件工程
2021-04-26 v1
摘要
本文考虑一类带有量化算子的非功能属性(NFP)即累积代价属性的去中心化监控问题。NFP的去中心化监控可能因若干原因而成为非平凡任务:(i)它们通常在高层抽象表达,其中事件间依赖被隐藏;(ii)NFP难以以去中心化方式监控;(iii)缺乏有效的分解技术。我们通过提供带有量化算子的LTL公式去中心化监控的形式化框架来解决这些问题。所提出的框架采用表构造和公式展开技术(即保留原公式语义的变换技术),以拆分并分发输入的LTL公式及相应量化约束,使得监控可以去中心化方式执行。这些技术的使用使进程能够及早检测被监控属性的违例并执行某些纠正或恢复动作。我们基于Fischertechnik训练模型(一个依据颜色将令牌分拣至存储仓的分拣线)的案例研究展示了该框架的有效性。案例分析表明,所提框架不仅在违例早期检测方面有效,而且在制定故障恢复计划方面有效,可帮助避免故障对系统性能的严重冲击。
引用
@article{arxiv.2104.11474,
title = {Monitoring Cumulative Cost Properties},
author = {Omar Al-Bataineh and Daniel Jun Xian Ng and Arvind Easwaran},
journal= {arXiv preprint arXiv:2104.11474},
year = {2021}
}
备注
12 pages, 8 figures, 5 tables, accepted in FormaliSE 2021