Verification using counterexample fragment based specification relaxation: case of modular/concurrent linear hybrid automata

Abstract

We present LhaVrf, a symbolic verifier for the safety verification of concurrent LHA (Linear Hybrid Automaton). A concurrent LHA is composed of a set of LHAs that interact through shared variables and/or events. An LHA is first translated to a purely discrete linear transition system that preserves the reachability of discrete states. Its analysis can be conducted in the proposed counterexample fragment based specification relaxation (CEFSR) framework, where an invalid fragment of a counterexample is used to eliminate the entire set of counterexamples sharing the same fragment, by way of specification relaxation (as opposed to the traditional model refinement). For concurrent systems, we propose further enhancement towards scalability as follows. For each spurious counterexample, an unsatisfiable core (unsat-core) that makes the counterexample invalid, is identified and used for specification relaxation, thereby eliminating the entire set of spurious counterexamples sharing the same unsat-core in a single iteration. Our implementation of LhaVrf adopts the above key ideas, with capability of automatically translating the hybrid automata into discrete transition system, composing the concurrent model, and using satisfiability modulo theory solver for validating counterexamples and fast-searching for the unsat-core. The verifier is illustrated via an application to the Fischer mutual exclusion protocol.

Keywords

• formal verification
• relaxation
• finite state machines
• reachability analysis
• computability
• modular linear hybrid automata
• LhaVrf
• symbolic verifier
• safety verification
• LHA
• concurrent linear hybrid automaton
• purely discrete linear transition system
• discrete state reachability
• counterexample fragment based specification relaxation
• CEFSR framework
• unsatisfiable core
• satisfiability modulo theory solver
• Fischer mutual exclusion protocol