APPLIED SYSTEMS SCIENCE TO HOLISTIC QUALITY ASSESSMENT METRICS FOR FORMAL METHODS-BASED MODELS

Abstract

In MBSE, deciding on the superiority of one formal method-based specification over another can be challenging, especially when both fulfil the exact requirements in distinct manners. This paper delves into a methodology for distinguishing between formal methods, using Event-B notation as a primary example, based on inherently subjective quality aspects. Traditional complexity metrics used in software assessment do not align well with formal methods, prompting the need for a novel quality function that considers the impact on the reader’s cognitive stress. The quality function incorporates classical axiomatic properties from theoretical mathematics and a bespoke complicatedness metric to evaluate model quality. Four critical properties—Consistency, Completeness, Independence, and Complicatedness—serve as the basis for this evaluation. Our approach suggests that if a formal specification appears visually complicated to someone with basic set-theory knowledge, it likely indicates a less helpful model regarding assurance. Additionally, the paper reconsiders Miller’s magic number seven, proposing that understanding human cognitive limits and using magical numbers 1, 2, and 3 is essential for defining high-quality formal specifications. This innovative perspective underscores the need for extensive further research, as outlined in the discussions of future work.