Automatic abstraction refinement for timed automata

摘要: We present a fully automatic approach for counterexample guided abstraction refinement of real-time systems modelled in subset timed automata. Our is implemented the MOBY/RT tool environment, which CASE embedded system specifications. Verification done by constructing abstractions semantics terms automata are fed into model checker UPPAAL. Since over-approximations, absence abstract counter examples implies valid result full model. new deals with situation an example found The generated used to construct either concrete or identify slightly refined spurious cannot occur anymore. Hence, allows loop starting from coarsest towards verification found. Nontrivial case studies demonstrate that this computes small fast without any user interaction.