Abstract
In this paper, an algebra of timed processes with real-valued clocks is presented, which serves as a formal description language for real-time communicating systems. We show that requirements such as “a process will never reach an undesired state” can be verified by solving a simple class of constraint systems on the clock-variables. A complete method for reachability analysis associated with the language is developed, and implemented as an automatic verification tool based on constraint-solving techniques. Finally as examples, we study and verify the safety-properties of Fischer’s mutual exclusion protocol and a railway crossing controller.
This research is supported in part by the Swedish Board for Technical Development (NUTEK), project No. 93-3244.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Rajeev Alur, Costas Courcoubetis, and David Dill. Model—checking for real—time systems. In Proceedings of the Fifth IEEE Symposium on Logic in Computer Science, 1990.
R. Alur, C Courcoubetis, N. Halbwachs, D. Dill, H. Wong-Toi. Minimization of Timed Transition Systems. CONCUR92, LNCS 630, 1992.
Rajeev Alur and David Dill. Automata for modelling real—time systems. In Automata, Languages and Programming: Proceedings of the 17th ICALP, LNCS 443. Springer-Verlag, 1990.
Martin Abadi and Leslie Lamport. An Old-Fashioned Recipe for Real Time. Lecture Notes in Computer Science, volume 600, Springer-Verlag, 1993.
J.C.M. Baeten and J.A. Bergstra. Real time process algebra. Technical Report P8916, University of Amsterdam, 1989.
B. Berhomieu and M. Diaz. Modeling and Verification of Time Dependent Systems Using Time Petri Nets. In IEEE trans. on Software Engineering, pages 259–273, Vol 17, March 1991.
Karlis Cerans, Jens Chr. Godskesen and Kim G. Larsen. Time Modal Specification — Theory and Tools. Proceedings of the 5th Int. Conf. on Computer Aided Verification, 1993.
M. Diaz. Modeling and analysis of communication and cooperation protocols using Petri net based models. Computer Networks, Dec. 1982.
Jim Davis and Steve Schneider. An introduction to timed CSP. Technical Report PRG-75, Oxford University Computing Laboratory, 1989.
Willem Jan Fokkink and Steven Klusener. Real time algebra with prefixed integration. Technical report, CWI, Amsterdam, 1991.
Jens Chr. Godskesen and Kim G. Larsen. Real-time calculi and expansion theorems. In Twelfth Conference on the FST and TCS, Lecture Notes in Computer Science. Springer-Verlag, December 1992.
Nicolas Halbwachs. Delay Analysis in Synchronous Programs. In the Proceedings of CAV’93, volume 697 of Lecture Notes in Computer Science. Springer-Verlag, 1991.
Uno Holmer, Kim Larsen, and Yi Wang. Deciding properties of regular timed processes. In Kim G. Larsen and Arne Skou, editors, Proceedings of the Third Workshop on Computer Aided Verification„ volume 575 of Lecture Notes in Computer Science. Springer-Verlag, 1991.
T. Henzinger, X. Nicollin, J. Sifakis, and J. Yovine. Symbolic Model Checking for Real-Time Systems. Proceedings of the 7th IEEE Symposium on Logic in Computer Science, 1992.
Matthew Hennessy and Tim Regan. A process algebra for timed systems. Technical Report 5/91, University of Sussex, 1991.
P.C. Kanellakis and S.A. Smolka, CCS Expressions, finite state processes, and three problems of equivalence. Information and Control Vol 86, 1990.
Kim G. Larsen and Wang Yi, Time Abstracted Bisimulation: Implicit Specification and Decidability. In the proceedings of MFPS93, New Oleans, USA, 1993. Lecture Notes in Computer Science No. 802, 1994.
Leslie Lamport. A fast mutual exclusion algorithm. ACM Trans. on Computer System, pages 1–11, volume 5 (1), February 1987.
Robin Milner. Communication and Concurrency. Series in Computer Science. Prentice-Hall International, 1989.
Faron Moller and Chris Tofts. A temporal calculus of communicating systems. In CONCUR’90, volume 458 of Lecture Notes in Computer Science. Springer-Verlag, 1990.
Martin Nilsson. Piecewise Linear Constraints and Entailment Technical report, Swedish Institute of Computer Science, August 1993.
X. Nicollin, J.-L. Richier, Joseph Sifakis, and J. Yovine. ATP: an algebra for timed processes. In Proceedings of the IFIP TC 2 Working Conference on Programming Concepts and Methods, Sea of Gallilee, Israel, April 1990.
Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. From ATP to timed graphs and hybrid systems. In Real-Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science. Springer-Verlag, 1991.
Kārlis Čerāns. Decidability of bisimulation equivalences for processes with parallel timers. In the Proceedings of CAV’92, 1992.
N. Shankar. Verification of Real-Time Systems Using PVS. Proceedings of the 5th Int. Conf. on Computer Aided Verification, 1993.
Frits Vaandrager and Nancy Lynch. Action Transducers and Timed Automata. In CONCUR ‘82, volume 630 of Lecture Notes in Computer Science. Springer-Verlag, 1992.
Yi Wang. Real-time behaviour of asynchronous agents. In CONCUR ‘80, volume 458 of Lecture Notes in Computer Science. Springer-Verlag, 1990.
Yi Wang. A Calculus of Real Time Systems. PhD thesis, Chalmers University of Technology, Göteborg, Sweden, 1991.
Yi Wang. CCS + time = an interleaving model for real time systems. In ICALP ‘81, LNCS 510. Springer-Verlag, 1991.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1995 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Yi, W., Pettersson, P., Daniels, M. (1995). Automatic Verification of Real-Time Communicating Systems by Constraint-Solving. In: Hogrefe, D., Leue, S. (eds) Formal Description Techniques VII. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-34878-0_18
Download citation
DOI: https://doi.org/10.1007/978-0-387-34878-0_18
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2881-0
Online ISBN: 978-0-387-34878-0
eBook Packages: Springer Book Archive