Context: Ensuring safety for any sophisticated system is getting more complex due to the rising number of features and functionalities. This calls for formal methods to entrust confidence in such systems. Nevertheless, using formal methods in industry is demanding because of their lack of usability and the difficulty of understanding verification results. Objective: We evaluate the acceptance of formal methods by Bosch automotive engineers, particularly whether the difficulty of understanding verification results can be reduced. Method: We perform two different exploratory studies. First, we conduct a user survey to explore challenges in identifying inconsistent specifications and using formal methods by Bosch automotive engineers. Second, we perform a one-group pretest-posttest experiment to collect impressions from Bosch engineers familiar with formal methods to evaluate whether understanding verification results is simplified by our counterexample explanation approach. Results: The results from the user survey indicate that identifying refinement inconsistencies, understanding formal notations, and interpreting verification results are challenging. Nevertheless, engineers are still interested in using formal methods in real-world development processes because it could reduce the manual effort for verification. Additionally, they also believe formal methods could make the system safer. Furthermore, the one-group pretest-posttest experiment results indicate that engineers are more comfortable understanding the counterexample explanation than the raw model checker output. Limitations: The main limitation of this study is the generalizability beyond the target group of Bosch automotive engineers.

翻译：背景：随着功能和特性的不断增加，确保任何复杂系统的安全性变得愈发困难。这要求采用形式化方法来增强对此类系统的信心。然而，在工业界使用形式化方法因其可用性不足以及验证结果难以理解而面临挑战。目标：我们评估博世汽车工程师对形式化方法的接受程度，特别是验证结果理解难度是否能够降低。方法：我们进行了两项探索性研究。首先，通过用户调查探究博世汽车工程师在识别不一致规范和使用形式化方法时面临的挑战。其次，开展单组前测-后测实验，收集熟悉形式化方法的博世工程师的反馈，以评估我们的反例解释方法是否简化了验证结果的理解。结果：用户调查表明，识别精化不一致性、理解形式化符号以及解读验证结果存在挑战。尽管如此，工程师仍对在实际开发过程中使用形式化方法感兴趣，因其可减少验证的手动工作量。此外，他们认为形式化方法能使系统更安全。同时，单组前测-后测实验结果显示，与原始模型检查器输出相比，工程师更易于理解反例解释。局限：本研究的主要局限性在于结论难以推广至博世汽车工程师以外的目标群体。