Extending the classes of montorable properties in detectER

Abstract

The emergence of concurrent computing in software development has resulted in systems where multiple thread interleavings are possible at execution time [1]. In consequence to the exponential growth of states associated with this behaviour, static verification techniques, such as model checking, do not scale well with such systems [2]. Runtime verification [3] mitigates this problem by verifying the correctness of a system exclusively along the path of execution undertaken at runtime. In terms of verifiable properties, however, this is achieved at the expense of lower expressiveness when compared to model checking [4]. In [5], Francalanza et al. propose a prototype tool, DETECTER, for monitoring properties specified using sHML, a subset of Hennessy-Milner Logic with recursion (RECH ML) [6]. The latter is a reformulation of the µ-calculus [7], which is intended to express correctness requirements of reactive systems. Although the identified sub-logic is well-suited for specifying safety properties for a system, the set of all monitorable properties extends well beyond this subset [4, 8]. This exposes the inherently limited expressiveness of DETECTER in its current form. In the presented work, we extend DETECTER to synthesise monitors for a wider spectrum of properties. Whereas safety properties are associated with invariants describing violations, there are also co-safety properties which describe satisfying behaviour along a finite trace [4]. In this regard, we identify an alternative sub-logic of RECHML, coined as cHML, for specifying co-safety properties, and implement this functionality within DETECTER. We also investigate the possibility of combining cHML and sHML in the formulation of obligation properties]. This is a superset afore mentioned classes of safety and co-safety properties. Finally, by virtue of a case study using Yaws [10], we demonstrate how this monitoring framework may be effectively employed for verifying the correctness of message passing systems.