Abstract
The article shows how untimed process algebraic methods can be used in verifying a category of dense time properties from a restricted class of timed automata. The work is based on the known results that if we restrict ourselves to a certain class of timed automata, then most of the interesting dense time properties are verifiable using discrete time methods. Those results are refined here in order to fit the process algebraic context, and furthermore, reduction strategies based on behavior equivalences, compositionality and abstraction are indicated. The usability of the method is evaluated with two case studies.
Chapter PDF
Similar content being viewed by others
References
Alur, R. and Dill, D. (1994). A Theory of Timed Automata. Theoretical Computer Science, 126:183–235.
Bošnački, D. (1999). Digitization of Timed Automata. In Fourth International Workshop on Formal Methods for Industrial Critical Systems.
Bošnačlki, D. and Damms, D. (1998). Integrating Real-Time in Spin: a Prototype Implementation. In Proceedings of IFIP Joint Conference on Formal Description Techniques and Protocol Specification, Testing and Verification, pages 423–439. Kluwer Academic Publishers.
D’Argenio, P., Katoen, J.-P., Ruys, T., and Tretmans, J. (1997). The Bounded Retransmission Protocol Must Be in Time. In Third International Workshop of Tools and Algorithms for the Construction and Analysis of Systems, number 1217 in Lecture Notes in Computer Science, pages 416–431. Springer-Verlag.
Daws, C., Olivero, A., Tripakis, S., and Yovine, S. (1996). The Tool KRONOS. In Hybrid Systems III, number 1066 in Lecture Notes in Computer Science, pages 208–219. Springer-Verlag.
Daws, C. and Tripakis, S. (1998). Model Checking of Timed Reachability Properties Using Abstraction. In Fourth International Workshop of Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science. Springer-Verlag.
Henzinger, T., Manna, Z., and Pnueli, A. (1992). What Good are Digital Clocks? In Proceedings of the 20th International Conference on Automata, Languages and Programming, number 623 in Lecture Notes in Computer Science, pages 545–558. Springer-Verlag.
Kaivola, R. (1996). Equivalences, Preorders and Compositional Verification for Linear Time Temporal Logic and Concurrent Systems. Report A-1996-1. PhD Thesis, University of Helsinki, Department of Computer Science.
Larsen, K. G., Pettersson, P., and Yi, W. (1995). Model-Checking for Real-Time Systems. In Proc. of Fundamentals of Computation Theory, number 965 in Lecture Notes in Computer Science, pages 62–88.
M. Luukkainen (2001). Verification of dense time properties using theories of untimed process algebra. www.cs.helsinki.fi/u/mluukkai/full.ps.
Tripakis, S. and Courcoubetis, C. (1996). Extending Promela and Spin with Real Time. In Second International Workshop of Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science. Springer-Verlag.
Valmari, A., Kemppainen, J., Clegg, M., and Levanto, M. (1993). Putting Advanced Reachability Analysis Techniques Together: the “ARA” Tool. In Proceedings of Formal Methods Europe, number 670 in Lecture Notes in Computer Science, pages 597–616. Springer-Verlag.
Valmari, A. and Tienari, M. (1995). Compositional Failure-Based Semantic Models for Basic LOTOS. Formal Aspects of Computing, 7:440–468.
Wolper, P. (1986). Expressing Interesting Properties of Programs in Propositional Temporal Logic. In Proceedings of the 13th ACM Symposium on Principles of Programming Languages, pages 184–193.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 IFIP International Federation for Information Processing
About this paper
Cite this paper
Luukkainen, M. (2001). Verification of Dense Time Properties Using Theories of Untimed Process Algebra. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds) Formal Techniques for Networked and Distributed Systems. FORTE 2001. IFIP International Federation for Information Processing, vol 69. Springer, Boston, MA. https://doi.org/10.1007/0-306-47003-9_22
Download citation
DOI: https://doi.org/10.1007/0-306-47003-9_22
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-7923-7470-1
Online ISBN: 978-0-306-47003-5
eBook Packages: Springer Book Archive