Abstraction-based verification of hierarchical statecharts

OData support
Supervisor:
Hajdu Ákos
Department of Measurement and Information Systems

Nowadays, as embedded systems take an increasingly important part in every aspect of our life, checking their correct behavior becomes more and more essential, especially in safety-critical cases, where a future of an enterprise or human lives rely on them. Formal verification is an important method, providing strong mathematical basis to check the correctness of the models in the design phase of the system’s lifecycle.

Hierarchical statecharts, as a frequently used behavioral model, are one of the foundations of system design, so their verification has an increased relevance. However in many cases, even the verification of a simple statechart can be challenging, since the large state space can prevent the verification as it grows exponentially with the number of variables in the system. There are several algorithms in the literature to efficiently handle and explore the state space. One of the most common amongst them is the bounded state reachability analysis, which is often realized with logical solvers, such as SAT and SMT solvers. In order to perform the analysis, the transition relation of the statechart is transformed to logical formulas, and these formulas are fed to the solver.

However, even these algorithms may not handle the complex behavior caused by the various data types and constructions used in the component models. To reduce the complexity caused by the huge state space, a possible solution is to use abstraction, even though it can fade details that are inevitable for successful verification. In these cases, the abstraction needs to be refined and the represented details should be enriched. This concept is the so-called Counterexample-Guided Abstraction Refinement (CEGAR) approach.

Most of the verification techniques used in practice do not exploit the information underlying in the hierarchical structure of the statecharts. The aim of my work is to develop algorithms that can handle hierarchical statecharts efficiently, and furthermore, that can benefit from the underlying information encoded in the state hierarchy during verification. I present a novel approach that can be used to effectively transform complex statecharts into logical formulas, taking benefits from the hierarchy. Improving that, I introduce an algorithm based on abstraction refinement (CEGAR), that takes hierarchy information into consideration during the refinement, and makes it possible to verify complex statecharts using logical solvers. The efficiency of the previously presented algorithms is demonstrated and compared on an industrial case study.

Downloads

Please sign in to download the files of this thesis.