Abstract
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 a LDI \({\cal D}\) by a timed automaton \({\cal A}\) by model checking a CTL property. For this, we construct an untimed automaton G from \({\cal A}\), and prove that \({\cal A}\) satisfies \({\cal D}\) iff \({\cal D}\) is is satisfied by the set of all paths of G. To Verify that all paths of G satisfy \({\cal D}\), we construct a CTL formula ψ and simply check if G satisfies ψ. By this, we convert the problem of verification of the LDI to the problem of model checking 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.
Research supported by the project of National Natural Science Foundation of China (No.60603037) and HTTS project funded by Macau Science and Technology Development Fund.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science, 183–235 (1994)
Alur, R.: Timed Automata. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 8–22. Springer, Heidelberg (1999)
Braberman, V.A., Van Hung, D.: On Checking Timed Automata for Linear Duration Invariants. In: Proceedings of the 19th Real-Time Systems Symposium RTSS 1998, pp. 264–273. IEEE Computer Society Press, Los Alamitos (1998)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)
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)
Kesten, Y., Pnueli, A., Sifakis, J., Yovine, S.: Integration Graphs: A Class of Decidable Hybrid Systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 179–208. Springer, Heidelberg (1993)
Dong, L.X., Van Hung, D.: Checking Linear Duration Invariants by Linear Programming. In: Jaffar, J., Yap, R.H.C. (eds.) ASIAN 1996. LNCS, vol. 1179, pp. 321–332. Springer, Heidelberg (1996)
Yong, L., Van Hung, D.: Checking Temporal Duration Properties of Timed Automata. Journal of Computer Science and Technology 17(6), 689–698 (2002)
Thai, P.H., Van Hung, D.: Verifying Linear Duration Constraints of Timed Automata. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 295–309. Springer, Heidelberg (2005)
Jianhua, Z., Van Hung, D.: Checking Timed Automata for Some Discretisable Duration Properties. Journal of Computer Science and Technology 15(5), 423–429 (2000)
Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters 40(5), 269–276 (1991)
Zhou, C.: Linear Duration Invariants. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 86–109. Springer, Heidelberg (1994)
Chaochen, Z., Hansen, M.R.: Duration Calculus. A Formal Approach to Real-Time Systems. Springer, Heidelberg (2004)
Yovine, S.: KRONOS: A Verification Tool for Real-Time Systems. STTT 1(1-2), 123–133 (1997)
Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)
Pandya, P.K.: Interval Duration Logic: Expressiveness and Decidability. ENTCS 65(6) (2002)
Meyer, R., Faber, J., Rybalchenko, A.: Model Checking Duration Calculus: A Practical Approach. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 332–346. Springer, Heidelberg (2006)
Fränzle, M., Hansen, M.R.: Deciding an Interval Logic with Accumulated Durations. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 201–215. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhang, M., Van Hung, D., Liu, Z. (2008). Verification of Linear Duration Invariants by Model Checking CTL Properties . In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds) Theoretical Aspects of Computing - ICTAC 2008. ICTAC 2008. Lecture Notes in Computer Science, vol 5160. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85762-4_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-85762-4_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85761-7
Online ISBN: 978-3-540-85762-4
eBook Packages: Computer ScienceComputer Science (R0)