arrow
返回

DSLs for Runtime Verification

delete2026-01-01
delete0
PRE
AI
H
Havelund, Klaus
O
Omer, Moran
P
Peled, Doron *
DOI:10.1007/978-3-032-05435-7_2delete
delete原文链接
delete原文求助
delete分享
delete收藏
摘要

摘要

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

期刊

R
RUNTIME VERIFICATION, RV 2025
IF:
0
论文数:
27
被引数:
0

机构

N
national aeronautics & space administration (nasa)
学者数:
3.1W
论文数: 2.6W
被引数: 46
N
nasa jet propulsion laboratory (jpl)
学者数:
6.9K
论文数: 5.3K
被引数: 14
引用论文

引用论文

err分享
err收藏
MarQ: Monitoring at Runtime with QEA
err2015-01-01
err0
PREAI
errReger,Giles; Cruz,Helena Cuenca; Rydeheard,David
err分享
err收藏
LarvaStat: Monitoring of Statistical Properties
err2010-01-01
err0
PREAI
errChristian Colombo; Andrew Gauci; Gordon J. Pace
err分享
err收藏
Monitoring modulo theories
err2016-04-01
err0
PREAI
errDecker,Normann; Leucker,Martin; Thoma,Daniel
err分享
err收藏
err分享
err收藏
LOLA: Runtime Monitoring of Synchronous Systems
err2024-10-23
err0
errOAAI
errB. D'Angelo; S. Sankaranarayanan; C. Sanchez; W. Robinson; B. Finkbeiner; H.B. Sipma; S. Mehrotra; Z. Manna
err分享
err收藏
学者 查看更多内容