论通过抑制实现的运行时强制
计算机科学中的逻辑
2018-07-04 v1
摘要
运行时强制是一种动态分析技术，它使用监视器对执行系统强制实施由某正确性属性所指定的行为。一种逻辑的可强制性刻画了该逻辑可表达的属性在运行时能被强制的程度。我们研究了带递归的Hennessy-Milner逻辑（muHML）相对于抑制强制的可强制性。我们开发了一个用于强制的操作框架，并随后用它形式化了一个监视器何时强制实施muHML属性。我们还通过提供一个自动综合函数（该函数从sHML公式生成正确的抑制监视器）表明该逻辑的安全语法片段sHML是可强制的。
引用
@article{arxiv.1807.01004,
title = {On Runtime Enforcement via Suppressions},
author = {Luca Aceto and Ian Cassar and Adrian Francalanza and Anna Ingolfsdottir},
journal= {arXiv preprint arXiv:1807.01004},
year = {2018}
}
备注
38 pages