确定性与组合性能否在 RML 中共存？（扩展版）
计算机科学中的逻辑
2020-08-18 v2 编程语言
摘要
运行时验证（RV）由动态验证被审查系统（SUS）单次运行所生成的事件轨迹是否符合其预期属性的形式化规约组成。RML（Runtime Monitoring Language，运行时监控语言）是一种简单但富有表达力的 RV 领域特定语言；其语义基于一种轨迹演算，该演算由确定性重写系统形式化，并驱动由 RML 编译器从规约生成的监视器解释器的实现。虽然轨迹演算的确定性确保了所生成监视器的更好性能，但它使其算子的语义不够直观。本文通过将其基本算子解释为实例化事件轨迹集合上的运算，并证明此种解释等价于该演算的操作语义，朝着 RML 轨迹演算的组合语义迈出了第一步。
引用
@article{arxiv.2008.06453,
title = {Can determinism and compositionality coexist in RML? (extended version)},
author = {Davide Ancona and Angelo Ferrando and Viviana Mascardi},
journal= {arXiv preprint arXiv:2008.06453},
year = {2020}
}