Abstract
The LTS of a system can be analyzed manually or using graph algorithms.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Alur, R., & Dill, D. L. (1994). A theory of timed automata. Theoretical Computer Science, 126(2), 183–235. https://doi.org/10.1016/0304-3975(94)90010-8.
Behrmann, G., David, A., & Larsen, K. G. (2006). A Tutorial on Uppaal 4.0. Aalborg, Denmark. url: http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf.
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. https://doi.org/10.1007/s100090050046.
Clarke, E. M., Grumberg, O., & Peled, D. (1999). Model checking. Cambridge, MA: MIT Press. ISBN: 0-262-03270-8.
Hoare, C. A. R. (1978). Communicating sequential processes. Communications of the ACM, 21(8), 666–677. https://doi.org/10.1145/359576.359585.
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. https://doi.org/10.1007/3-540-60218-6_34.
Holzmann, G. J. (1997). The model checker SPIN. IEEE Transactions on Software Engineering, 23(5), 279–295. https://doi.org/10.1109/32.588521.
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. https://doi.org/10.1016/j.entcs.2005.03.032.
May, D. (1983). OCCAM. ACM SIGPLAN Notices, 18(4), 69–79. https://doi.org/10.1145/948176.948183.
Milner, R. (1984). A calculus of communicating systems. Heidelberg: Springer. LNCS vol. 9, https://doi.org/10.1007/3-540-10235-3.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Daszczuk, W.B. (2020). Model Checking of IMDS Specifications in the Dedan Environment. In: Integrated Model of Distributed Systems. Studies in Computational Intelligence, vol 817. Springer, Cham. https://doi.org/10.1007/978-3-030-12835-7_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-12835-7_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-12834-0
Online ISBN: 978-3-030-12835-7
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)