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

基于联代数模态逻辑和博弈的软件族定量验证

• 批准号: EP/X019373/1
• 负责人: Harsh Beohar
• 金额: $ 30.05万
• 依托单位: University of Sheffield
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2023
• 资助国家: 英国
• 起止时间: 2023 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FX019373%2F1
• 关键词: Quantitative; verification; software; families; based

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.

为了通过大规模自定义促进软件，许多软件供应商从核心软件基础开发产品。结果，不仅要考虑一种产品，而且要同时建模和开发软件系统系列已经变得越来越普遍。现在，将单一产品设计给软件系统家族的这种转变通常对正式方法面临两个重大挑战。首先，建立对单个产品的一致性的传统形式验证技术具有可扩展性，因为无法用形式主义表达软件家族的行为。其次，当说为等效关系时，一致性不是行为比较W.R.T.的强大概念。规格，需要以行为距离的形式进行更细粒度的比较。当软件包含与不确定环境相互作用的组件（例如在自主驾驶的背景下）时，这一点尤其重要，并且这种安全性 - 流界系统的正确性是可解释AI的全球趋势的一部分。因此，我们的总体目的是通过启用基于行为差异的软件家庭的更为细粒度的行为分析来推进前最新的验证技术。特别是，我们将开发抽象的数学模型来指定软件家族的行为，开发FixPoint算法以计算此类模型上的行为距离，并开发分析技术以诊断实现不合格时诊断。在我们最近关于软件家族行为等价的工作的基础上，我们将在山地抽象的水平上提出和解决我们的研究问题。优点是，可以创建一个通用的核心框架来推理一个基于状态的固定分支类型的基于状态的系统，可以将其实例化为软件产品线（静态或自适应）或参数Markov模型等混凝土域。换句话说，该提案列出了对造型为山结构的软件家族进行定量验证所必需的理论基础。此外，这项研究还提供了发展山地理论的动力，因为许多基本问题（例如表达性的模态逻辑和游戏）尚未开发出具有副作用的山地行为距离。

项目成果

Hennessy-Milner Theorems via Galois Connections

通过伽罗瓦连接的 Hennessy-Milner 定理

• DOI: 10.4230/lipics.csl.2023.12
• 发表时间: 2023
• 作者: Beohar H