Zhang, Miaomiao; Hung, Dang Van; Liu, Zhiming Verification of linear duration invariants by model checking CTL properties. (English) Zbl 1161.68595 Fitzgerald, John S. (ed.) et al., Theoretical aspects of computing – ICTAC 2008. 5th international colloquium, Istanbul, Turkey, September 1–3, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-85761-7/pbk). Lecture Notes in Computer Science 5160, 395-409 (2008). Summary: Linear duration invariants (LDI) are important safety properties of real-time systems. They can be easily formulated in terms of a class of chop-free formulas in the Duration Calculus (DC). Compared to other temporal logics, the specification in DC is simpler, neater and more importantly easier to understand. However, directly model checking them is more difficult than model checking properties formulated in the computation tree logic (CTL). In this paper, we present a technique for the verification of the satisfaction of an LDI \({\mathcal D}\) by a timed automaton \({\mathcal A}\) by model checking a CTL property. For this, we construct an untimed automaton \(G\) from \({\mathcal A}\), and prove that \({\mathcal A}\) satisfies \({\mathcal D}\) iff \({\mathcal D}\) is is satisfied by the set of all paths of \(G\). To verify that all paths of \(G\) satisfy \({\mathcal D}\), we construct a CTL formula \(\psi \) and simply check if \(G\) satisfies \(\psi \). By this, we convert the problem of verification of the LDI to the problem of model checking a CTL formula. As a result, the CTL model checking techniques and tools, such as UPPAAL, can be used for verification of LDI specified in the DC.For the entire collection see [Zbl 1154.68011]. Cited in 2 Documents MSC: 68Q60 Specification and verification (program logics, model checking, etc.) 03B44 Temporal logic 03B70 Logic in computer science Software:Uppaal; Kronos PDFBibTeX XMLCite \textit{M. Zhang} et al., Lect. Notes Comput. Sci. 5160, 395--409 (2008; Zbl 1161.68595) Full Text: DOI References: [1] Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science, 183-235 (1994) · Zbl 0803.68071 [2] Alur, R.; Halbwachs, N.; Peled, D. A., Timed Automata, Computer Aided Verification, 8-22 (1999), Heidelberg: Springer, Heidelberg · Zbl 1046.68574 · doi:10.1007/3-540-48683-6_3 [3] Braberman, V. A.; Van Hung, D., On Checking Timed Automata for Linear Duration Invariants, Proceedings of the 19th Real-Time Systems Symposium RTSS 1998, 264-273 (1998), Los Alamitos: IEEE Computer Society Press, Los Alamitos [4] Clarke, E.; Grumberg, O.; Peled, D., Model Checking (1999), Cambridge: The MIT Press, Cambridge [5] Emerson, E. A.; Halpern, J. Y., “Sometimes“ and “Not Never” Revisited: On Branching versus Linear Time Temporal Logic, Journal of the ACM, 33, 1, 151-178 (1986) · Zbl 0629.68020 · doi:10.1145/4904.4999 [6] Kesten, Y.; Pnueli, A.; Sifakis, J.; Yovine, S.; Grossman, R. L.; Ravn, A. P.; Rischel, H.; Nerode, A., Integration Graphs: A Class of Decidable Hybrid Systems, Hybrid Systems, 179-208 (1993), Heidelberg: Springer, Heidelberg [7] Dong, L. X.; Van Hung, D.; Jaffar, J.; Yap, R. H.C., Checking Linear Duration Invariants by Linear Programming, Concurrency and Parallelism, Programming, Networking, and Security, 321-332 (1996), Heidelberg: Springer, Heidelberg [8] Yong, L.; Van Hung, D., Checking Temporal Duration Properties of Timed Automata, Journal of Computer Science and Technology, 17, 6, 689-698 (2002) · Zbl 1056.68096 · doi:10.1007/BF02960759 [9] Thai, P. H.; Van Hung, D.; Liu, Z.; Araki, K., Verifying Linear Duration Constraints of Timed Automata, Theoretical Aspects of Computing - ICTAC 2004, 295-309 (2005), Heidelberg: Springer, Heidelberg · Zbl 1109.68070 [10] Jianhua, Z.; Van Hung, D., Checking Timed Automata for Some Discretisable Duration Properties, Journal of Computer Science and Technology, 15, 5, 423-429 (2000) · Zbl 0961.68079 · doi:10.1007/BF02950405 [11] Chaochen, Z.; Hoare, C. A.R.; Ravn, A. P., A calculus of durations, Information Processing Letters, 40, 5, 269-276 (1991) · Zbl 0743.68097 · doi:10.1016/0020-0190(91)90122-X [12] Zhou, C.; Langmaack, H.; de Roever, W.-P.; Vytopil, J., Linear Duration Invariants, Formal Techniques in Real-Time and Fault-Tolerant Systems, 86-109 (1994), Heidelberg: Springer, Heidelberg [13] Chaochen, Z.; Hansen, M. R., Duration Calculus. A Formal Approach to Real-Time Systems (2004), Heidelberg: Springer, Heidelberg · Zbl 1071.68062 [14] Yovine, S., KRONOS: A Verification Tool for Real-Time Systems, STTT, 1, 1-2, 123-133 (1997) · Zbl 1060.68606 [15] Behrmann, G.; David, A.; Larsen, K. G.; Bernardo, M.; Corradini, F., A tutorial on Uppaal, Formal Methods for the Design of Real-Time Systems, 200-236 (2004), Heidelberg: Springer, Heidelberg · Zbl 1105.68350 [16] Pandya, P.K.: Interval Duration Logic: Expressiveness and Decidability. ENTCS 65(6) (2002) · Zbl 1270.68175 [17] Meyer, R.; Faber, J.; Rybalchenko, A.; Barkaoui, K.; Cavalcanti, A.; Cerone, A., Model Checking Duration Calculus: A Practical Approach, Theoretical Aspects of Computing - ICTAC 2006, 332-346 (2006), Heidelberg: Springer, Heidelberg · Zbl 1168.68425 · doi:10.1007/11921240_23 [18] Fränzle, M.; Hansen, M. R.; Grumberg, O.; Huth, M., Deciding an Interval Logic with Accumulated Durations, Tools and Algorithms for the Construction and Analysis of Systems, 201-215 (2007), Heidelberg: Springer, Heidelberg · Zbl 1186.03055 · doi:10.1007/978-3-540-71209-1_17 This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.