Specification and Verification Method of Parallel Hierarchical Timed Automata by Predicate Abstraction and Refinement

Embedded systems have three major features: real-time, parallel and hierarchical. Therefore, we specified an embedded system as a hierarchically structured timed automata operating in parallel. The reduction technique of the state space for verifying embedded systems is crucial. On the other hand, Counterexample-Guided Abstraction Refinement (CEGAR) is a very hopeful verification method. In this study, we propose an effective CEGAR for a parallel hierarchical timed automaton. First, the algorithm performs abstraction of the hierarchical structures and timing constraints. Next, it performs a reachability analysis and divided counterexample analysis on the individual automaton. Based on the results of the analysis, the algorithm performs refinement corresponding to each abstraction. In the refinement, we devised it such that an overapproximation is maintained even if two abstractions are paired. In addition, the abstraction of timing constraints is performed after the abstraction of hierarchical structures; however the algorithm refines only the attention part, and the refinement of the hierarchical structure applies to an individual automaton. Finally, we implemented the proposed method as a prototype in Mathematica. The proposed CEGAR effectively reduced the state space.