USABILITY REQUIREMENT OF FORMAL VERIFICATION TOOLS

Abstract

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. This study presents a survey conducted on two instances of verification tools that support formal notations, namely ProB and B-Toolkit. 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 were analyzed by using the Grounded Theory. The analysis enabled the identification of abstract features and properties that formed a design guideline for usable verification tools. The 38guideline includes three main categories of feature; Interface, Utilities and Resources Management. The features are further elaborated through the specification of specific properties and dimensions for implementation. The guideline could act as a roadmap for tool designers to design verification tools that promote the use of formal notations.

Keywords

• : usability requirement
• formal verification tools
• empirical study