A lightweight LTL runtime verification tool for java
A lightweight LTL runtime verification tool for java
复制标题
一个轻量级的java LTL运行时验证工具
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
E. Bodden
中科院分区：
文献类型：
--
作者：
E. Bodden
验证是运行时测试的一种特殊形式，使用形式化的方法和语言。在这项工作中，我们利用下一次自由的线性时间时序逻辑（LTL extbackslash X）作为正式框架。该规程的目的是断言有关面向对象（OO）实体（如对象、方法等）的某些设计时假设。本文提出了一种基于连接点的线性时间逻辑citeLaddad03AidoJ，并介绍了一个基于该逻辑的轻量级运行时验证工具J2SE 5元数据citeJSR175和一个基于AidoJ的citeAidoJ运行时后端。到目前为止，已经提出了命令式和函数式语言的实现citeHuchStolz04a。据我们所知，我们的方法是第一个允许解决整个状态集，也超过子类边界，从而利用OO的性质。
Runtime verification is a special form of runtime testing, employing formal methods and languages. In this work, we utilize next-time free linear-time temporal logic (LTL extbackslash X) as formal framework. The discipline serves the purpose of asserting certain design-time assumptions about object-oriented (OO) entities such as objects, methods, and so forth. In this paper we propose a linear-time logic over joinpoints citeLaddad03AspectJ, and introduce a lightweight runtime veri-fication tool based on this logic, J2SE 5 metadata citeJSR175 and an AspectJ-based citeAspectJ runtime backend. Implementations have been proposed so far for imperative and functional languages citeHuchStolz04a. To our knowledge our approach is the first to allow addressing of entire sets of states, also over subclass boundaries, thus exploiting the OO nature.