Eliminating Queues from RT UML Model Representations

  • Werner Damm
  • Bengt Jonsson
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2469)


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.


Real-time distributed systems RT UML protocol verification verification of infinite state systems 


  1. 1.
    Euro-Interlocking Requirements, September 2001, see
  2. 2.
    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.Google Scholar
  3. 3.
    D. Harel and E. Gery. Executable Object Modelling with Statecharts. IEEE Computer, July 1997, 31–42Google Scholar
  4. 4.
    D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 2(5):323–342, April 1983.Google Scholar
  5. 5.
    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.Google Scholar
  6. 6.
    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.zbMATHGoogle Scholar
  7. 7.
    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.Google Scholar
  8. 8.
    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.CrossRefGoogle Scholar
  9. 9.
    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.Google Scholar
  10. 10.
    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.Google Scholar
  11. 11.
    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.Google Scholar
  12. 12.
    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.Google Scholar
  13. 13.
    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.CrossRefGoogle Scholar
  14. 14.
    B. Westphal Exploiting Object Symmetry in Verification of UML-Designs, Diplomarbeit, Carl von Ossietzky Universität, 2001Google Scholar
  15. 15.
    W. Damm and A. Pnueli. An Active Object Model. Technical Report, OFFIS, Oldenburg, FRG, 2002.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Werner Damm
    • 1
  • Bengt Jonsson
    • 1
  1. 1.Dept. of Computer SystemsUppsala UniversityUppsala

Personalised recommendations