Measuring the Quality of B Abstract Machines with ISO/IEC 25010

TL;DR

This paper introduces a set of ISO/IEC 25010-based criteria for quantitatively assessing the quality of B abstract machines, enhancing software development reliability.

Contribution

It proposes a novel quality measurement framework for B abstract machines using standardized software quality standards and model checking techniques.

Findings

Criteria effectively quantify abstract machine quality.

Implementation as a B model quality evaluator demonstrates practical applicability.

Examples validate the proposed measurement approach.

Abstract

The B method has facilitated the development of software by specifying the design of software as abstract machines and formally verifying the correctness of the abstract machines. The quality of B abstract machines can significantly impact the quality of final software products. In this paper, we propose a set of criteria for measuring the quality of B abstract machines based on ISO/IEC 25010, which is one of the latest international standards for evaluating software quality in software engineering. These criteria evaluate abstract machines using a number of general-purpose and domain-independent equations and model checking techniques, so that the quality of abstract machines can be quantified as vectors. The proposed criteria are implemented as a B model quality evaluator, and they are explained and justified using a number of examples.