Model checking domain models: state-of-the-practice

by Pudovkin Dmitriy, dopudovkin@edu.hse.ru

Nowadays many model checking tools are used for formal verification of systems consisting of software or hardware. There are a lot of model checking tools available, such as PRISM, AT, FDR, NuSMV, UPPAAL, and so on[1]. Experts have demonstrated the use of model checking tools in a wide variety of fields. This study discusses the reasons for using model checking tools, some methods that are available today and identifies the key reasons for the weak alignment of these tools.

Model checking is an algorithmic verification technique. Model checking algorithms are able to answer the question of consistency of domain model, and when the answer is negative, they give counterexamples that can help improve the model. Model checking tries to construct a model of the software system and verify the validity of the set of properties of the system represented as a logical expression. A model is usually an abstraction of a real system.

Model checkers are classified by type of verification algorithms.

Explicit Model Checker. This checker represents the system as a finite state machine. The main idea is to visit each reachable state explicitly and check that every behavior satisfies the specifications. Graph of states is created using DFS or BFS algorithms. Explicit state algorithms, the states of the system are generated on-the-fly as the algorithm executes, and tools are often distinguished by the type of the encoding.

Symbolic Model Checker. This checker represents the state of the system as a boolean function. Instead of enumerating reachable states one at a time as in the previous method, the state can sometimes be depicted more efficiently by considering large numbers of states at a single step. This method applies to binary decision diagrams (BDD). The achievements in developing effective methods to solve (Boolean satisfiability problem) SAT problem helps symbolic model checking become popular. The model and set of steps are represented symbolically. For symbolic methods, there are two essential approaches that are used to solve the generated boolean formulae: SAT and (Satisfiability Modulo Theories) SMT[1].

Bounded Model Checker. This checker represents a state transition system. Bounded model checking uses LTL (Linear Time Logic) for a checking formula. This method specifies a boundary K and obtains counterexamples by searching from the initial state of a system to states reachable by K-steps. The basic idea of a bounded model checker is to represent a counterexample-trace of bounded length symbolically and verify the resulting formula with a SAT solver. If the formula is correct and thus the path achievable, a satisfying assignment returned by the SAT solver can be translated into a concrete counterexample trace that shows that the property is violated[2].

Software complexity. The development of domain models is always accompanied by the difficulty of defining domain models that would correctly display real objects and meet system requirements. Currently, the complexity of the designed systems has increased many times. Large modern systems have a lot of obvious and hidden model constraints. It becomes difficult to recognize how these constraints will affect the interactions of models in such a large system[3].

Importance of reliability. Today, software systems are a key component for many critical sectors of human life, from aviation to healthcare. The possibility of a malfunction in a working product can lead to serious consequences. Verification of models using model checking tools is used to reduce the probability of such a failure[4].

Cost of development and maintenance. Checking models at the initial design stage can prevent the development of software that will later prove difficult to expand and expensive to maintain. The cost of maintaining such systems can be much more expensive than the initial design using the model checking tools.

Additional efforts. Formal modeling requires additional effort and increases software development time. Computational complexity. Many of the methods that are used to test models are resource-intensive for computer computing. An example of some bounded model checkers are based on the SAT, which is an NP complete problem in general form[5].

Design complexity. Designing models for complex software that covers a wide subject area is accompanied by complex models for which it is problematic to use model checking tools[4].

Knowledge and experience. In order to use the tools and formal methods that allow testing models, it needs special knowledge that most developers and domain experts do not have.

Human factor. The process of using model checking tools requires as much precision as the software development process. Therefore, the influence of the human factor in the design of models and their constraints can have an extremely negative impact on the result of using any of the methods.

At the moment, there are many formal methods that are used to check models. The key mathematical approaches in these methods are extended versions of boolean algebra and finite automata theory. Using these methods in practice requires special knowledge. The software utilities currently developed using this approach are highly specialized and are mainly used for hardware verification, due to the constraints on these methods imposed by logic algebra. In addition, the complexity of model checking can be comparable to the complexity of its construction or even higher. This study lists the signs that are a serious constraints for the further development of existing formal approaches.

1. Shubha Raj K B and Suryaprasad J Model checkers – tools and languages for system design / International Conference on Advanced Information Technologies and Applications. — 2016. — № 5. — С. 40-51.
2. Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh Bounded Model Checking Handbook of Satisfiability. - 2021. - 336 с.
3. John Penix, Charles Pecheur and Klaus Havelund Using Model Checking to Validate AI Planner Domain Models / 1990
4. Dibyendu Baksi Model checking of healthcare domain models / PubMed. - 1990. - №2009
5. Paolo Liberatore and Marco Schaerf Belief Revision and Update: Complexity of Model Checking Journal of Computer and System Sciences. - 2001. - №62. - С. 43-72.