Portal de Periódicos da CAPES

The LIME Interface Specification Language and Runtime Monitoring Tool

2009; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-642-04694-0_7

1611-3349

Kari Kähkönen, Jani Lampinen, Keijo Heljanko, Ilkka Niemelä,

Formal Methods in Verification

This paper describes an interface specification language designed in the LIME project (LIME ISL) and the supporting runtime monitoring tool. The interface specification language is tailored for the Java programming language and supports two kinds of specifications: (i) call specifications that specify requirements for the allowed call sequences to a Java object instance and (ii) return specifications that specify the allowed behaviors of the Java object instance. Both the call and return specifications can be expressed with Java annotations in several different ways: as past time LTL formulas, as (safety) future LTL formulas, as regular expressions, and as nondeterministic finite automata. We also describe the supporting LIME interface monitoring tool which is an open source implementation of runtime monitoring for the interface specifications implemented using AspectJ.