On Efficiently Specifying Models for Model Checking

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 statespace 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.