基于 Kind 2 的功绩与归责分配
计算机科学中的逻辑
2021-05-17 v1
摘要
我们介绍了开源模型检验器 Kind 2 的两个新的主要特性，它们提供了同步反应式系统模型中规约与设计元素（如假设、保证或其他行为约束）之间的可追溯性信息。这个新版 Kind 2 能够识别足以证明给定一组安全属性的最小设计元素集合（称为最小归纳有效性核），并确定 MUST 元素集合，即证明给定属性所必需的设计元素。此外，Kind 2 能够找到最小设计约束集合（称为最小割集），其违反会导致系统进入不安全状态。所计算的信息可用于多种目的，包括评估系统规约的质量、跟踪模型变更的安全影响，以及分析系统对故障或网络攻击的容忍度与弹性。我们较为详细地描述了这些新能力，并报告了对其中部分能力的初步实验评估。
引用
@article{arxiv.2105.06575,
title = {Merit and Blame Assignment with Kind 2},
author = {Daniel Larraz and Mickaël Laurent and Cesare Tinelli},
journal= {arXiv preprint arXiv:2105.06575},
year = {2021}
}