Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

1-2013

Abstract

Real-time system verification must deal with a special notion of ‘fairness’, i.e., clocks must always be able to progress. A system run which prevents clocks from progressing unboundedly is known as Zeno. Zeno runs are infeasible in reality and thus must be pruned during system verification. Though zone abstraction is an effective technique for model checking real-time systems, it is known that zone graphs (e.g., those generated from Timed Automata models) are too abstract to directly infer time progress and hence non-Zenoness. As a result, model checking with non-Zenoness (i.e., existence of a non-Zeno counterexample) based on zone graphs only is infeasible. In our previous work [23], we show that model checking Stateful Timed CSP with non-Zenoness based on zone graphs only is feasible, due to the difference between Stateful Timed CSP and Timed Automata. Nonetheless, the algorithm proposed in [23] requires to associate each time process construct with a unique clock, which could enlarge the state space (compared to model checking without non-Zenoness) significantly. In this paper, we improve our previous work by combining the checking algorithm with a clock-symmetry reduction method. The proposed algorithm has been realized in the PAT model checker for model checking LTL properties with non-Zenoness. The experimental results show that the improved algorithm significantly outperforms the previous work.

Keywords

Model Check, Label Transition System, Symmetry Reduction, Strongly Connected Component, Time Automaton

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 15th International Conference on Formal Engineering Methods, ICFEM 2013, Queenstown, New Zealand, October 29 - November 1

First Page

182

Last Page

198

ISBN

9783642412011

Identifier

10.1007/978-3-642-41202-8_13

Publisher

Springer Link

City or Country

Queenstown, New Zealand

Additional URL

https://doi.org/10.1007/978-3-642-41202-8_13

Download

Share

COinS