返回
DSLs for Runtime Verification
DOI:10.1007/978-3-032-05435-7_2.png)
摘要
En 中文
运行时验证(RV)允许对系统的执行进行形式化规范的监控。提高形式化方法的能力和范围的主要挑战源于在增加所使用规范形式化表达力的同时,降低所涉及算法的复杂度并保持规范的简洁性之间的权衡。RV对一次执行的关注允许在实现方式和实现这些目标方面具有极大的灵活性。本文重点探讨将RV逻辑作为外部DSL(领域特定语言)、内部DSL和混合DSL(两者的混合)实现的可能性。我们还讨论了使用AI从自然语言需求生成监控器的应用。我们调研了这些可能性,并特别关注其对实现所需表达力水平的影响。本文关注的特定挑战是允许在监控事件中出现的数据上使用算术运算和关系。
Keyword:
Runtime verification
Domain-specific languages
Formal specifications
Monitor generation
Arithmetic operations

