Towards a Runtime Verification Framework for the Ada Programming Language
Ref: CISTER-TR-140305 Publication Date: 23 to 27, Aug, 2014
Towards a Runtime Verification Framework for the Ada Programming LanguageRef: CISTER-TR-140305 Publication Date: 23 to 27, Aug, 2014
Runtime verification is an emerging discipline that investigates methods and tools to enable the verification of program properties during the execution of the application. The goal is to complement static analysis approaches, in particular when static verification leads to the explosion of states. Therefore, non-functional properties, such as the ones presented by real-time systems are an ideal target for this kind of verification methodology, as are usually out of the range of the power and expressiveness of classic static analyses. In this paper, we present a framework that allows real-time programs written in Ada to be augmented by such runtime verification power. Our framework provides the code infrastructures needed to instrument the code with runtime monitors. Such monitors are responsible for observing a system and reach verdicts about whether its behavior is compliant with its non-functional requirements. We also sketch a contract language to extend the one current provided by Ada, with the long term goal of having an elegant way in which runtime monitors can be automatically synthesized and instrumented into the target systems. This usefulness of the approach is demonstrated by showing its use for an application scenario.
Lecture Notes in Computer Science, Reliable Software Technologies – Ada-Europe 2014 (LNCS), Springer International Publishing, 8454, pp 58-73.