Runtime verification for API based software

Abstract

The modern world is increasingly dependent on communication-centred and distributed software systems. Application Programming Interfaces (APIs) are what enable these systems to interact and share information with one another. The correctness of their interaction is of utmost importance since the consequences of failure can be quite severe. Behavioural types offer a promising approach to address this matter by enabling the description of correct interactions which systems are then verified against. This work investigates the design and implementation of a hybrid (static and dynamic) approach for the verification of these types. In particular, we address those scenarios with two communicating components where one is available prior-deployment and the other must be treated as a black box. We propose an approach in which the available component is statically checked whereas the black box component is verified dynamically at runtime (i.e., during execution) via a monitor. At the centre of our approach is a synthesis algorithm which generates monitor descriptions from a behavioural type. We show that these generated monitors are themselves correct, and that they only flag an erroneous action when the monitored component indeed commits one. This is crucial since the monitors can negatively affect the behaviour of the other components if they are not correct. To validate the implementability of this approach, we present a tool in Scala as a case study. We show that the executable code closely follows the theory, which suggests that the notion of correctness established in the theory carries over into the implementation. Furthermore, the proposed theory and implementability aspects of our approach are not limited to this technology but can be applied to those cases where static analysis of session types is possible and the dynamic verification of the interaction of a component is required.