A User-Study Protocol for Evaluation of Formal Verification Results and their Explanation

TL;DR

This paper proposes a user-study protocol to evaluate whether presenting formal verification results in a user-friendly way increases acceptance among engineers, addressing usability challenges in safety-critical system verification.

Contribution

It introduces a structured protocol combining surveys and experiments to assess the impact of improved result explanations on formal methods adoption.

Findings

Engineers face challenges in understanding formal verification results.

Simplified explanations may improve acceptance of formal methods.

Preliminary results suggest increased understanding post-explanation.

Abstract

Context: The complexity of modern safety-critical systems in industries keep on increasing due to the rising number of features and functionalities. This calls for formal methods in order to entrust confidence in such systems. Nevertheless, using formal methods in industry is demanding because of usability issues, e.g., the difficulty of understanding model checking results. Thus the hypothesis is, presenting the result of model checker results in a user-friendly manner could promote formal methods usage in industries. Objective: We aim to evaluate the acceptance of formal methods by engineers if the complexity of understanding verification results is made easy. Method: We perform two different exploratory studies. First, we conduct an online survey to explore challenges in identifying inconsistent specifications and using formal methods from engineers. Second, we perform a one group pretest and posttest experiment to collect impressions from engineers using formal methods if understanding verification results is eased. Limitations: The main limitation of this study is the generalization because the survey focuses on a particular target group and it uses a pre-experimental design.