how to stop time stopping：如何停止时间停止.pdf

DOI: -006-0010-7 (In press) BCS c°2006 Formal Aspects puting How to Stop Time Stopping Howard Bowman and Rodolfo G′omez puting Laboratory, University of Kent, United Kingdom, {,rsg2}***@ -timelocks constitute a challenge for the formal veri?cation of timed automata: they are di?cult to detect, and the veri?cation of most properties (., safety) is only correct for timelock-free models. Some time ago, Tripakis proposed a syntactic check on the structure of timed automata: If a certain condition (called strong non-zenoness) is met by all the loops in a given automaton, then zeno-timelocks are guaranteed not to occur. Checking for strong non-zenoness is e?cient, positional (if ponents in work of automata are strongly non-zeno, then work is free from zeno-timelocks). Strong non-zenoness, however, is su?cient-only: There exist non-zeno speci?cations which are not strongly non-zeno. A TCTL formula is known that represents a su?cient-and-necessary condition for non-zenoness; unfortunately, this formula requires a demanding model-checking algorithm, and not all model-checkers are able to express it. In addition, this algorithm provides only limited diagnostic information. Here we propose a number of alternative solutions. First, we show that positional application of strong non-zenoness can be weakened: works can be guaranteed to be free from Zeno-timelocks, even if not ponent is strongly non-zeno. Secondly, we present new syntactic, su?cient-only conditions plement strong non-zenoness. Finally, we describe a su?cient-and-necessary condition that only requires a simple form of reachability analysis. Furthermore, our conditions identify the cause of zeno- timelocks directly on the model, in the form of unsafe loops. We ment on a tool that we have developed, which implements the syntactic checks on Uppaal models. The tool is also able to derive, from those unsafe loops in a given automaton (in general, an Uppaal model representing a