Mykhaylo Nykolaichuk, Michael Lipaczewski, Tino Liebusch, Frank Ortmeier: On Efficiently Specifying Models for Model Checking. In: Proceedings of 4th International Symposium on Model Based Safety and Assessment (IMBSA 2014), 2014.

Abstract

Using formal methods for quality assurance is recommended in many standards for safety critical applications. In most industrial contexts, model checking is the only viable option for formal verification, as interactive approaches often require very highly specialized experts. However, model checking typically suffers from the well-known state-space explosion problem. Due to this problem, engineers typically have to decide on a trade-off between readability and completeness of the model on one side, and the state space size, and thus, computational feasibility on the other. In this paper, we propose a method for reducing the state space by restructuring models. The core idea is to introduce as few additional states as possible by model design making state transitions more complex. To avoid unreadability and infeasible model sizes, we introduce a concept for hierarchical boolean formulas to efficiently specify state transitions. For evaluation purposes, we applied this approach to a case study using the VECS toolkit. In this exemplary case study, we were able to reduce the state space size significantly and make verification time feasible.

BibTeX (Download)

@inproceedings{nykolaychukIMBSA_2014,
title = {On Efficiently Specifying Models for Model Checking},
author = { Mykhaylo Nykolaichuk and Michael Lipaczewski and Tino Liebusch and Frank Ortmeier},
url = {http://link.springer.com/chapter/10.1007/978-3-319-12214-4_2
https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/Nykolaychuk_IMBSA_2014.pdf
},
year  = {2014},
date = {2014-01-01},
booktitle = {Proceedings of 4th International Symposium on Model Based Safety and Assessment (IMBSA 2014)},
abstract = {Using formal methods for quality assurance is recommended in many standards for safety critical applications. In most industrial contexts, model checking is the only viable option for formal verification, as interactive approaches often require very highly specialized experts. However, model checking typically suffers from the well-known state-space explosion problem. Due to this problem, engineers typically have to decide on a trade-off between readability and completeness of the model on one side, and the state space size, and thus, computational feasibility on the other. In this paper, we propose a method for reducing the state space by restructuring models. The core idea is to introduce as few additional states as possible by model design making state transitions more complex. To avoid unreadability and infeasible model sizes, we introduce a concept for hierarchical boolean formulas to efficiently specify state transitions. For evaluation purposes, we applied this approach to a case study using the VECS toolkit. In this exemplary case study, we were able to reduce the state space size significantly and make verification time feasible.},
keywords = {model-based, VECS},
pubstate = {published},
tppubtype = {inproceedings}
}