This article introduces a fully automated verification technique that permits to analyze real-time systems described using a continuous notion of time and a mixture of operational (i.e., automata-based) and descriptive (i.e., logic-based) formalisms. The technique relies on the reduction, under reasonable assumptions, of the continuous-time verification problem to its discrete-time counterpart. This reconciles in a viable and effective way the dense discrete and operational descriptive dichotomies that are often encountered in practice when it comes to specifying and analyzing complex critical systems. The article investigates the applicability of the technique through a significant example centered on a communication protocol. More precisely, concurrent runs of the protocol are formalized by parallel instances of a Timed Automaton, while the synchronization rules between these instances are specified through Metric Temporal Logic formulas, thus creating a multi-paradigm model. Verification tests run on this model using a bounded validity checker implementing the technique show consistent results and interesting performances.
@cite_26: In this paper we present a method for modeling asynchronous digital circuits by timed automata. The constructed timed automata serve as “mechanical” and verifiable objects for asynchronous sequential machines in the same sense that (untimed) automata do for synchronous machines. These results, combined with recent results concerning the analysis and synthesis of timed automata provide for the systematic Treatment of a large class of problems that could be treated by conventional simulation methods only in an ad-hoc fashion. The problems that can be solved due to the results presented in this paper include: the reachability analysis of a circuit with uncertainties in gate delays and input arrival times, inferring the necessary timing constraints on input signals that guarantee a proper functioning of a circuit and calculating the delay characteristics of the components required in order to meet some given behavioral specifications.
@cite_11: 
@cite_22: 
@cite_33: 
@cite_8: 
@cite_9: 
@cite_21: 
@cite_3: In this paper, we introduce a parametric semantics for timed controllers called the Almost ASAP (as soon as possible) semantics. This semantics is a relaxation of the usual ASAP semantics (also called the maximal progress semantics) which is a mathematical idealization that cannot be implemented by any physical device no matter how fast it is. On the contrary, any correct Almost ASAP controller can be implemented by a program on a hardware if this hardware is fast enough. We study the properties of this semantics and show how it can be analyzed using the tool HyTech.
@cite_6: 
@cite_24: 
@cite_19: 
@cite_5: 
@cite_34: Timed systems can be considered with two types of semantics – dense time semantics and discrete time semantics. The most typical examples of both of them are real semantics and sampled semantics (i.e., discrete semantics with a fixed time step e). We investigate the relations between real semantics and sampled semantics with respect to different behavioral equivalences. Also, we study decidability of reachability problem for stopwatch automata with sampled semantics. Finally, our main technical contribution is decidability of non-emptiness of a timed automaton ω-language in some sampled semantics (this problem was previously wrongly classified as undecidable). For the proof we employ a novel characterization of reachability relations between configurations of a timed automaton.
@cite_20: 
@cite_25: We study the digitisation of dense-time behaviours of timed processes, and show how this leads to exact verification methods for a large class of dense-time specifications. These specifications are all closed under inverse digitisation, a robustness property first introduced by Henzinger, Manna, and Pnueli (on timed traces), and extended here to timed failures, enabling us to consider liveness issues in addition to safety properties. We discuss a corresponding model checking algorithm and show that, in many cases, automated verification of such dense-time specifications can in fact be directly performed on the model checker FDR (a commercial product of Formal Systems (Europe) Ltd.). We illustrate this with a small case study (the railway level crossing problem). Finally, we show that integral--or digitised--behaviours are fully abstract with respect to specifications closed under inverse digitisation, and relate this to the efficiency of our model checking algorithm.
@cite_12: Real-time systems operate in “real,” continuous time and state changes may occur at any real-numbered time point. Yet many verification methods are based on the assumption that states are observed at integer time points only. What can we conclude if a real-time system has been shown “correct” for integral observations?
@cite_17: 
Another stance at working around the undecidability of dense-time MTL builds upon the fact that the same logic is decidable over discrete time. Hence, a few approaches introduce some notion of discretization, that is partial reduction of the verification problem from dense to discrete time. The present paper goes in this direction by extending previous work on MTL @cite_24 to the case of TA. A different discretization technique, based on the notion of robust satisfiability of MTL specifications, has been introduced in @cite_21 . Other work also deals with notions of robustness in order to guarantee that dense-time TA are implementable with non-ideal architectures @cite_3 . Another well-known notion of discretization is the one based on the concept of @cite_12 ; several authors have applied this quite general notion to the practical verification of descriptive @cite_25 @cite_17 @cite_5 @cite_6 or operational @cite_8 @cite_34 @cite_22 @cite_20 @cite_26 @cite_11 @cite_33 @cite_19 @cite_9 formalisms. See also the related work section of @cite_24 for more references about discretization techniques.