形式化方法与人类可解释性之间的桥梁
软件工程
2025-06-12 v1
摘要
标记转移系统（LTS）是模型检验和设计修复工具的核心组成部分。系统工程师在模型检验或设计修复过程中频繁检查LTS设计，以调试、识别不一致性并验证系统行为。尽管LTS具有重要意义，但此前尚无研究考察人类对这些设计的理解。为解决这一问题，我们借鉴传统软件工程和图论，识别出7个关键指标：圈复杂度、状态空间大小、平均分支因子、最大深度、Albin复杂度、模块化和冗余度。我们创建了一个包含148个LTS设计的数据集，从中采样48个进行324组配对比较，并使用Bradley-Terry模型进行排序。通过Kendall's Tau相关性分析，我们发现Albin复杂度（τ=0.444）、状态空间大小（τ=0.420）、圈复杂度（τ=0.366）和冗余度（τ=0.315）最准确地反映了人类对LTS设计的理解。为展示这些指标的实用性，我们将Albin复杂度指标应用于Fortis设计修复工具中对系统重设计进行排序。该排序使标注者的理解时间减少了39%，表明强调人类因素的指标可以增强形式化设计的可解释性。
引用
@article{arxiv.2506.09759,
title = {Towards Bridging Formal Methods and Human Interpretability},
author = {Abhijit Paul and Proma Chowdhury and Kazi Sakib},
journal= {arXiv preprint arXiv:2506.09759},
year = {2025}
}
备注
Need to improve data annotation process in methodology section