A User-Study Protocol for Evaluation of Formal Verification Results and their Explanation
This addresses usability issues for engineers in safety-critical industries, but it is incremental as it focuses on presentation rather than core method improvements.
The study tackled the problem of low adoption of formal methods in safety-critical industries due to difficulty understanding verification results, by evaluating if user-friendly presentations improve engineer acceptance through surveys and experiments.
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.