Exploiting Hierarchy in the Abstraction-Based Verification of Statecharts Using SMT Solvers

摘要: Statecharts are frequently used as a modeling formalism in the design of state-based systems. Formal verification techniques also often applied to prove certain properties about behavior system. One most efficient for formal is Counterexample-Guided Abstraction Refinement (CEGAR), which reduces complexity systems by automatically building and refining abstractions. In our paper we present novel adaptation CEGAR approach hierarchical statechart models. First introduce an encoding logical formulas that preserves information state hierarchy. Based on this propose abstraction refinement utilize structure statecharts handle variables model. The allows us use SMT solvers systematic exploration abstract model, including bounded model checking. We demonstrate applicability efficiency with measurements industry-motivated example.