Systematic assessment of formal methods based models quality criteria

Maldini, Lorenzo; Wright, Stephen

Abstract

When presented with two fully proved formal methods-based specifications, how can a System Engineer decide which is superior when both models specify the same requirements, but in two different ways? This paper investigates and propose a methodology by which formal methods (using the specific example of the Event-B notation) can be differentiated in terms of their quality, using criteria that may be highly subjective in nature. Established complexity functions applied to software are not applicable to formal methods, thus the paper proposes a new function which quantifies the “quality” of a given model. Complexity is not the only factor involved in determining the quality of formal methods, the quality of system thinking involved also play an impactful role. We propose a quality function which uses the well-established properties of axiomatic systems in theoretical mathematics with the addition of a specifically formulated complexity function. The distinction criteria are based on evaluating how four main properties have been achieved: “Consistency”, “Completeness”, “Independence” and “Complexity”. We base our approach according to the paradigm of; “if the formal specification looks visually complicated for a set-theory novice, then it is a poorly modeled specification”. Furthermore, we explore the notion of Miller’s rule (magic No. 7) to define what “good” should look like. We conclude that we need more than Miller’s 7, we need 1, 2 and 3 to help us with defining what good quality looks like, by taking human cognitive capacity as a benchmark. This novel approach implies considerable further research, described in future work section.

• Presentation Conference Type: Conference Paper (published)
• Conference Name: MEDI 2021 International Workshops: DETECT, SIAS, CSMML, BIOC, HEDA
• Start Date: Jun 21, 2021
• End Date: Jun 23, 2021
• Acceptance Date: May 1, 2021
• Online Publication Date: Oct 7, 2021
• Publication Date: Jan 1, 2021
• Deposit Date: Jun 17, 2022
• Publisher: Springer Verlag (Germany)
• Volume: 1481 CCIS
• Pages: 31-45
• Series Title: Communications in Computer and Information Science (CCIS, volume 1481)
• Series Number: CCIS, volume 1481
• Edition: 1st
• Book Title: Advances in Model and Data Engineering in the Digitalization Era MEDI 2021 International Workshops: DETECT, SIAS, CSMML, BIOC, HEDA, Tallinn, Estonia, June 21–23, 2021, Proceedings
• Chapter Number: 9
• ISBN: 9783030876562
• DOI: https://doi.org/10.1007/978-3-030-87657-9_3
• Keywords: Formal methods; Systems engineering; System thinking; Event-B; Model based system engineering; Miller’s rule; System complexity function; Information processing capacity
• Public URL: https://uwe-repository.worktribe.com/output/9530414
• Publisher URL: https://link.springer.com/chapter/10.1007/978-3-030-87657-9_3
• Related Public URLs: https://link.springer.com/content/pdf/10.1007/978-3-030-87657-9.pdf; ; https://link.springer.com/conference/medi