Model Checking of IMDS Specifications in the Dedan Environment

  • Wiktor B. DaszczukEmail author
Part of the Studies in Computational Intelligence book series (SCI, volume 817)


The LTS of a system can be analyzed manually or using graph algorithms.


  1. Alur, R., & Dill, D. L. (1994). A theory of timed automata. Theoretical Computer Science, 126(2), 183–235. Scholar
  2. Behrmann, G., David, A., & Larsen, K. G. (2006). A Tutorial on Uppaal 4.0. Aalborg, Denmark. url:
  3. Cimatti, A., Clarke, E., … Roveri, M. (2000). NUSMV: A new symbolic model checker. International Journal on Software Tools for Technology Transfer, 2(4), 410–425.
  4. Clarke, E. M., Grumberg, O., & Peled, D. (1999). Model checking. Cambridge, MA: MIT Press. ISBN: 0-262-03270-8.Google Scholar
  5. Hoare, C. A. R. (1978). Communicating sequential processes. Communications of the ACM, 21(8), 666–677. Scholar
  6. Holzmann, G. J. (1995). Tutorial: Proving properties of concurrent systems with SPIN. In 6th International Conference on Concurrency Theory, CONCUR’95, Philadelphia, PA, 21–24 Aug. 1995 (pp. 453–455). Heidelberg: Springer.
  7. Holzmann, G. J. (1997). The model checker SPIN. IEEE Transactions on Software Engineering, 23(5), 279–295. Scholar
  8. Lanese, I., & Montanari, U. (2006). Hoare vs Milner: Comparing synchronizations in a graphical framework with mobility. Electronic Notes in Theoretical Computer Science, 154(2), 55–72. Scholar
  9. May, D. (1983). OCCAM. ACM SIGPLAN Notices, 18(4), 69–79. Scholar
  10. Milner, R. (1984). A calculus of communicating systems. Heidelberg: Springer. LNCS vol. 9, Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.Institute of Computer ScienceWarsaw University of TechnologyWarsawPoland

Personalised recommendations