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