Usability Requirements of Formal Verification Tools: A Survey

Abstract

Problem statement: Formal notations employ mathematical symbols and interpretation to illustrate system elements. The formality imposed by the notations allows the accuracy and consistency of a system model to be confirmed by verification tools. Formal notations on the other hand are difficult to understand and use by most users. As supporting instruments, verification tools are expected to be as usable as possible to overcome this limitation. Approach: This study presented a survey conducted on two instances of verification tools that support a formal method, namely B. The focus of the survey was to identify the important features that are necessary for verification tools to become usable to users. The survey assessed the tools’ usability based on the Cognitive Dimensions of Notations (CD) framework and several criteria suggested by the International Organization for Standardization (ISO). Sixty-three participants responded to the survey. The data was analyzed by using the grounded theory. Results: The analysis enabled the identification of abstract concepts and properties that formed a design guideline for usable verification tools. The guideline includes there main aspects; Interface, Utilities and Resources Management. Conclusion: The guideline acts as a roadmap for tool designers to design verification tools that promote the use of formal notations.