Journal of Computer Science

Usability Requirements of Formal Verification Tools: A Survey

Rozilawati Razali and Paul Garratt

DOI : 10.3844/jcssp.2010.1189.1198

Journal of Computer Science

Volume 6, Issue 10

Pages 1189-1198

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.

Copyright

© 2010 Rozilawati Razali and Paul Garratt. This is an open access article distributed under the terms of the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.