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.