Title: Refinement Annotations for LARVA's DATEs

Abstract:
LARVA is a runtime verification framework for evaluating executing programs against a set of specifications described in terms of DATEs (Dynamic Automata with Timers and Events). Expressing various properties as DATEs on different levels of abstraction and defining the relationships which hold between these levels can significantly enhance the output of the framework. This output can aid to pinpoint not only that a program does not obey its specification but also whether a specification has been designed correctly with respect to those on its preceding levels. We shall be presenting the proposed syntax (and corresponding LARVA evaluation mechanism) to enhance the DATE specification notation with the necessary annotations, to organise property expressions from individual DATEs, and to express the refinement relations that must hold between these expressions.