论文标题
确定性和组成性可以在RML中共存吗？ （扩展版）
Can determinism and compositionality coexist in RML? (extended version)
论文作者
论文摘要
运行时验证（RV）在于动态验证审查（SUS）的单个系统生成的事件迹线符合其预期属性的正式规范。 RML（运行时监视语言）是RV的简单但表现力的特定语言；它的语义是基于由确定性重写系统正式形式化的痕量演算，该系统驱动了RML编译器从规格中生成的显示器的解释器的实现。虽然痕量演算的确定性确保了生成的监视器的更好性能，但它使其运算符的语义降低了直观。在本文中，我们通过将其基本运算符解释为实例化事件迹线的操作，并证明这种解释等同于计算的操作语义，将其基本运算符解释为RML Trace conculus的组成语义的第一步。
Runtime verification (RV) consists in dynamically verifying that the event traces generated by single runs of a system under scrutiny (SUS) are compliant with the formal specification of its expected properties. RML (Runtime Monitoring Language) is a simple but expressive Domain Specific Language for RV; its semantics is based on a trace calculus formalized by a deterministic rewriting system which drives the implementation of the interpreter of the monitors generated by the RML compiler from the specifications. While determinism of the trace calculus ensures better performances of the generated monitors, it makes the semantics of its operators less intuitive. In this paper we move a first step towards a compositional semantics of the RML trace calculus, by interpreting its basic operators as operations on sets of instantiated event traces and by proving that such an interpretation is equivalent to the operational semantics of the calculus.
