Bounded Verification of State Machine Models
Nafıseh Kahani, James R. Cordy · 2020
In this work, we propose a bounded verification approach for state machine (SM) models that is independent of any model checking tools. This independence is achieved by encoding the execution semantics of SM models as Satisfiability Modulo Theories (SMT) formulas that reduce the verification of a SM to the satisfiability problem for its corresponding formula. More specifically, our approach takes as input a SM model, a depth bound, and the system properties (as invariants), and then automatically verifies models of systems in a three-phase process: (1) First it generates all possible execution paths of the model to the specified bound, and encodes each of the execution paths as SMT formulas; (2) It then augments the SMT formulas with the negation of the given invariants; and (3) Finally, it uses an SMT solver to check the satisfiability of the instrumented formula. We have applied our approach in the context of UML-RT (the UML profile for modeling real-time embedded systems) and assessed the applicability, performance, and scalability of our approach using several case studies.