Abstract
This paper concerns analyzing UML based models of distributed real time systems involving multiple active agents. In order to avoid the timepenalties incurred by distributed execution of synchronous operation calls, it is typically recommended to restrict inter-task communication to event-based communication through unbounded FIFO buffers. This means that such systems potentially have an infinite number of states, making them out of reach for analysis techniques intended for finite-state systems. We present a symbolic analysis technique of such systems, which can be tuned to give a finite, possibly inexact representation of the state-space. The central idea is to eliminate FIFO buffers completely, and represent their contents implicitly, by their effect on the receiving agent. We propose a natural class of protocols which we call mode separated, for which this representation is both finite and exact. This result has impact on both responsiveness and predictability of end-to-end latencies, as well for the protocol verification, enabling automatic verification methods to be applied.
This research was partially supported by DFG USE and the STINT foundation.
On sabbatical leave from Dept. of Computer Science, University of Oldenburg. Oldenburg, FRG
Chapter PDF
References
Euro-Interlocking Requirements, September 2001, see http://www.eurolock.org
W. Damm and J. Klose. Verification of a Radio-based Signaling System Using the Statemate Verification Environment. Formal Methods in System Design, Vol 19(2), 2001.
D. Harel and E. Gery. Executable Object Modelling with Statecharts. IEEE Computer, July 1997, 31–42
D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 2(5):323–342, April 1983.
A.P. Sistla and L.D. Zuck. Automatic temporal verification of buffer systems. in Larsen and Skou, editors, Proc.3rd Int. Conf. on Computer Aided Verification, volume 575 of Lecture Notes in Computer Science, Springer Verlag, 1991.
M.G. Gouda, E.M. Gurari, T.-H. Lai, and L.E. Rosier. On deadlock detection in systems of communicating finite state machines. Computers and Artificial Intelligence, 6(3):209–228, 1987.
J.K. Pachl. Protocol description and analysis based on a state transition model with channel expressions. In Protocol Specification, Testing, and Verification VII, May 1987.
P. A. Abdulla, A. Bouajjani, and B. Jonsson. On-the-fly analysis of systems with unbounded, lossy FIFO channels. In Proc. 10th Int. Conf. on Computer Aided Verification, volume 1427 of Lecture Notes in Computer Science, pages 305–318, 1998.
W. Peng and S. Purushothaman. Dataflow analysis of communicating finite state machines. ACM Trans. on Progr. Languages and Systems 13(3):399–442, July 1991.
B. Boigelot and P. Godefroid. Symbolic verification of communication protocols with infinite statespaces using QDDs. In Alur and Henzinger, editors, Proc. 8th Int. Conf. on Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 1–12. Springer Verlag, 1996.
B. Boigelot, P. Godefroid, B. Willems, and P. Wolper. The power of QDDs. In Proc. 4th Int. Static Analysis Symposium, Lecture Notes in Computer Science. Springer Verlag, 1997.
A. Bouajjani and P. Habermehl. Symbolic reachability analysis of FIFO channel systems with nonregular sets of configurations. in Proc. ICALP 97, volume 1256 of Lecture Notes in Computer Science, 1997.
P.A. Abdulla and B. Jonsson. Channel representations in protocol verification. in Proc. CONCUR 2001, 12th int. Conf. on Concurrency Theory, volume 2154 of Lecture Notes in Computer Science, pages 1–15, 2001.
B. Westphal Exploiting Object Symmetry in Verification of UML-Designs, Diplomarbeit, Carl von Ossietzky Universität, 2001
W. Damm and A. Pnueli. An Active Object Model. Technical Report, OFFIS, Oldenburg, FRG, 2002.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Damm, W., Jonsson, B. (2002). Eliminating Queues from RT UML Model Representations. In: Damm, W., Olderog, E.R. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 2002. Lecture Notes in Computer Science, vol 2469. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45739-9_22
Download citation
DOI: https://doi.org/10.1007/3-540-45739-9_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44165-6
Online ISBN: 978-3-540-45739-8
eBook Packages: Springer Book Archive