Usability requirements of formal verification tools: A survey

Rozilawati Razali, Paul Garratt

Research output: Contribution to journalArticle

6 Citations (Scopus)

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.

Original languageEnglish
Pages (from-to)1189-1198
Number of pages10
JournalJournal of Computer Science
Volume6
Issue number10
DOIs
Publication statusPublished - 2010

Fingerprint

Formal methods
Formal verification
Standardization

Keywords

  • Empirical assessment
  • Formal verification tools
  • Usability requirement

ASJC Scopus subject areas

  • Software
  • Computer Networks and Communications
  • Artificial Intelligence

Cite this

Usability requirements of formal verification tools : A survey. / Razali, Rozilawati; Garratt, Paul.

In: Journal of Computer Science, Vol. 6, No. 10, 2010, p. 1189-1198.

Research output: Contribution to journalArticle

@article{d2a87f20be524944bec3a95aeb2c3b60,
title = "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.",
keywords = "Empirical assessment, Formal verification tools, Usability requirement",
author = "Rozilawati Razali and Paul Garratt",
year = "2010",
doi = "10.3844/jcssp.2010.1189.1198",
language = "English",
volume = "6",
pages = "1189--1198",
journal = "Journal of Computer Science",
issn = "1549-3636",
publisher = "Science Publications",
number = "10",

}

TY - JOUR

T1 - Usability requirements of formal verification tools

T2 - A survey

AU - Razali, Rozilawati

AU - Garratt, Paul

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

KW - Empirical assessment

KW - Formal verification tools

KW - Usability requirement

UR - http://www.scopus.com/inward/record.url?scp=78049465798&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=78049465798&partnerID=8YFLogxK

U2 - 10.3844/jcssp.2010.1189.1198

DO - 10.3844/jcssp.2010.1189.1198

M3 - Article

AN - SCOPUS:78049465798

VL - 6

SP - 1189

EP - 1198

JO - Journal of Computer Science

JF - Journal of Computer Science

SN - 1549-3636

IS - 10

ER -