Runtime Verification for Generic Classes with CONGU2 - Formal Methods: Foundations and Applications - page 33

Runtime Verification for Generic Classes with C ON G U 2

Pedro Crispim, Antonia Lopes, and Vasco T. Vasconcelos

LaSIGE and Faculty of Sciences, University of Lisbon,
Campo Grande, 1749-016 Lisboa, Portugal
{ pedro.crispim,mal,vv } @di.fc.ul.pt

Abstract. Even though generics became quite popular in mainstream object-
oriented (OO) languages, approaches for checking at runtime the conformance
of such programs against formal specifications still lack appropriate support.
In order to overcome this limitation within C ON G U , a tool-based approach we
have been developing to support runtime conformance checking of Java
programs against algebraic specifications, we recently proposed a notion of re-
finement mapping that allows to define correspondences between parametric spec-
ifications and generic classes. Based on such mappings, we also put forward a
notion of conformance between the two concepts. In this paper we present how
the new notion of conformance is supported by version 2 of the C ON G U tool.

1 Introduction

The formal specification of software components is an important activity in the process
of software development, insofar as specifications are useful, on the one hand, to un-
derstand and reuse software and, on the other, to automatically verify the correctness
of components implementations. Among the several approaches that can be adopted
for automatically analysing the reliability of software components one finds runtime
verification . This approach involves the monitoring and analysis of system executions.
As the system executes, the behaviour of its components is tested for correction with
respect to the specification. Runtime monitoring has the advantage that can be used to
analyse properties for which static verification fails. Moreover, it does not require the
user expertise and effort typically required of a static verification system.
Although generics became quite popular in mainstream OO languages, existent ap-
proaches for runtime checking the conformance of generic OO programs against for-
mal specifications still lack appropriate support. This was also the case of C ON G U ,a
tool-based approach to runtime verification of Java implementations against algebraic
specifications [10,17]. C ON G U is intensively used by our undergraduate students in the
context of a course on algorithms and data structures for checking abstract data types
(ADTs) implementations.
Given that generics became extremely useful and popular in the implementation of
ADTs in Java, in particular those that are traditionally covered in such courses, the lack
of support for generics became a major drawback. In order to overcome this limitation,
we recently proposed a notion of refinement mapping that allows to define correspon-
dences between parameterized specifications and generic classes [16]. Based on such
mappings, we also put forward a more comprehensive notion of conformance between