Quantitative verification of software families based on coalgebraic modal logic and games

To facilitate software with mass customisation, many software vendors develop a product from a core software base. As a result, it has become increasingly common to consider not only a single product, but to model and develop a family of software systems at the same time. Now this transformation of designing a single product to a family of software systems poses, in general, two significant challenges for Formal Methods. First, the traditional formal verification techniques for establishing conformance on a single product suffers from scalability since the inability of underlying formalisms to express behaviour of a software family. Second, conformance when stated as an equivalence relation is not a robust notion of behavioural comparison w.r.t. a specification, where a more fine-grained comparison in the form of behavioural distance is required. This is particularly relevant when software includes components that interact with an uncertain environment (like in the context of autonomous driving) and the correctness of such safety-crticial systems is part of the global trend on explainable AI.

So our overarching aim is to advance the state-of-art verification techniques by enabling a more fine-grained behavioural analysis of software families based on behavioural distances. In particular, we will develop abstract mathematical models to specify behaviour of software families, develop fixpoint algorithms to compute behavioural distances on such models, and develop analysis technqiues to diagnose when an implementation is nonconforming. Building upon our recent work on behavioural equivalences for software families, we will pose and tackle our research questions at the abstract level of coalgebras. The advantage is that one can create a generic core framework to reason about a family of state-based systems of fixed branching types, which can be instantiated to concrete domains like software product lines (both static or adaptive) or parametric Markov models. In other words, this proposal lays out the theoretical underpinning necessary for the quantitative verification of software families modelled as coalgebras. Furthermore, this research also provides an impetus for evolving the theory of coalgebras since many fundamental questions (like expressive modal logics and games) for behavioural distances on coalgebras with side effects are not yet developed.