  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.
