English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Runtime verification (RV) consists in dynamically verifying that the eventtraces generated by single runs of a system under scrutiny (SUS) are compliantwith the formal specification of its expected properties. RML (RuntimeMonitoring Language) is a simple but expressive Domain Specific Language forRV; its semantics is based on a trace calculus formalized by a deterministicrewriting system which drives the implementation of the interpreter of themonitors generated by the RML compiler from the specifications. Whiledeterminism of the trace calculus ensures better performances of the generatedmonitors, it makes the semantics of its operators less intuitive. In this paperwe move a first step towards a compositional semantics of the RML tracecalculus, by interpreting its basic operators as operations on sets ofinstantiated event traces and by proving that such an interpretation isequivalent to the operational semantics of the calculus.

Can determinism and compositionality coexist in RML? (extended version)