博世形式化验证结果及其解释评估的用户研究

背景：由于功能和特性的数量不断增加，确保任何复杂系统的安全性正变得愈发复杂。这要求采用形式化方法以赋予此类系统可信度。然而，由于可用性不足以及理解验证结果的困难，在工业中使用形式化方法颇具挑战。目标：我们评估博世汽车工程师对形式化方法的接受度，特别是理解验证结果的困难是否可以被降低。方法：我们进行两项不同的探索性研究。首先，我们开展用户调查，以探究博世汽车工程师在识别不一致规范和运用形式化方法方面的挑战。其次，我们实施一组前测-后测实验，收集熟悉形式化方法的博世工程师的反馈，以评估我们的反例解释方法是否简化了对验证结果的理解。结果：用户调查结果表明，识别精化不一致性、理解形式化符号以及解释验证结果具有挑战性。尽管如此，工程师仍对在实际开发流程中使用形式化方法感兴趣，因为它可减少验证的人工投入。此外，他们也相信形式化方法能使系统更安全。并且，一组前测-后测实验结果表明，相较于原始模型检验器输出，工程师对反例解释的理解更为轻松。局限性：本研究的主要局限性在于超越博世汽车工程师目标群体后的可推广性。