一种用于评估形式化验证结果及其解释的用户研究协议

背景：由于功能与特性数量的上升，现代工业安全关键系统的复杂性持续增加。这要求采用形式化方法以对这些系统建立信任。然而，由于可用性问题（例如理解模型检测结果困难），在工业中使用形式化方法要求很高。因此假设是，以用户友好的方式呈现模型检测器的检测结果可促进形式化方法在工业中的使用。目标：我们旨在评估若降低理解验证结果的复杂性，工程师对形式化方法的接受度。方法：我们执行两项不同的探索性研究。首先，我们开展在线调查，以探究工程师在识别不一致规约与使用形式化方法方面的挑战。其次，我们执行一组前测-后测实验，以收集工程师在使用形式化方法时若理解验证结果变容易的印象。局限性：本研究的主要局限性在于泛化性，因为调查聚焦于特定目标群体且采用了前实验设计。