定量验证的一种通用方法

本论文关注定量验证，即对定量系统的定量性质进行验证。这类系统出现在众多应用中，其定量验证十分重要，但也颇具挑战。特别是，鉴于应用中出现的大多数系统都相当庞大，验证方法的组合性与增量性至关重要。为确保验证的鲁棒性，我们用距离取代标准验证中的布尔是非答案。根据应用背景，定量验证中采用了许多不同类型的距离。因此，需要一套抽象于具体距离、在独立于距离的层面上发展定量验证的系统距离通用理论。我们认为，在定量验证理论中，定量方面应像定性方面一样被视为验证问题的输入。本文发展了这样一套定量验证的通用理论。我们假设输入为迹（或执行）之间的距离，然后利用具有定量目标的博弈理论来定义定量系统之间的距离。定量互模拟博弈的不同变体产生了不同类型的距离，即互模拟距离、模拟距离、迹等价距离等，使我们能够构建 van Glabbeek 线性时间—分支时间谱的定量推广。我们还将定量验证的通用理论扩展为定量规范理论。为此我们使用模态迁移系统，并发展了行为规范理论常用算子的定量性质。