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.
| Original language | English |
|---|---|
| Title of host publication | Proceedings - 2020 International Symposium on Theoretical Aspects of Software Engineering, TASE 2020 |
| Editors | Toshiaki Aoki, Qin Li |
| Place of Publication | Piscataway NJ USA |
| Publisher | IEEE, Institute of Electrical and Electronics Engineers |
| Pages | 169-176 |
| Number of pages | 8 |
| ISBN (Electronic) | 9781728140865 |
| ISBN (Print) | 9781728164625 |
| DOIs | |
| Publication status | Published - 2020 |
| Externally published | Yes |
| Event | International Symposium on Theoretical Aspects of Software Engineering 2020 - Hangzhou, China Duration: 11 Dec 2020 → 13 Dec 2020 Conference number: 14th https://ieeexplore.ieee.org/xpl/conhome/9405291/proceeding (Proceedings) https://tase2021.github.io/ (Website) |
Conference
| Conference | International Symposium on Theoretical Aspects of Software Engineering 2020 |
|---|---|
| Abbreviated title | TASE 2020 |
| Country/Territory | China |
| City | Hangzhou |
| Period | 11/12/20 → 13/12/20 |
| Internet address |
|
Keywords
- abstract machine
- B-method
- model checking
- model quality
- software quality