Modelling CTMC with a standard programming language and using conventions from computer networking

• Autorzy: Rataj A. , Nowak M. , Pecka P.

Warianty tytułu

PL

Modelowanie łańcuchów Markowa z czasem ciągłym przy użyciu standardowego języka programowania i z zastosowaniem konwencji z dziedziny sieci komputerowych

• Języki publikacji: EN

Abstrakty

EN

Continuous time Markov chains (CTMC) are one of the formalisms for building models. This paper discusses expressing these models in a standard programming language – Java. Using such a language as a model description allows for a partially common implementation of the production software and of the description of the model, for a greater flexibility in comparison to model-checker specific languages that often do not employ features of an object-oriented programming. Using Java also makes the parsing of models relatively fast, using optimised Java runtime environment. Our approach aims at using typical mechanisms of the Java language when implementing the model, and at the same time, following closely the concepts from computer networking and from formalisms based on it, like the queueing systems. These assumption result in techniques like plain object fields constituting the state vector, or negotiation between nodes to decide if an event happens.

PL

Łańcuchy Markowa czasu rzeczywistego są jednym z formalizmów używanych do budowy modeli. Artykuł ten omawia wyrażanie takich modeli w standardowym języku programowania - Javie. Użycie takiego języka umożliwia częściowo wspólną implementację oprogramowania użytkowego i opisu modelu, większą elastyczność w porównaniu do często nie używających obiektowych konwencji programistycznych języków stosowanych przez oprogramowanie weryfikujące, oraz szybką budowę modelu z użyciem zoptymalizowanego środowiska czasu wykonania Javy. Nasze podejście miało na celu wykorzystanie typowych mechanizmów języka Java przy opisie modelu i jednoczesnie trzymanie się konwencji z dziedziny sieci komputerowych i pokrewnych formalizmóm typu systemy kolejkowe. Dlatego używamy technik takich jak zastosowanie pól obiektów jako elementów wektora stanu czy negocjacja pomiędzy węzłami, czy dane zdarzenie ma mieć miejsce.

Słowa kluczowe

EN

Markov chain; continuous time; model checking; Java

• Wydawca: Instytut Informatyki Teoretycznej i Stosowanej Polskiej Akademii Nauk
• Czasopismo: Theoretical and Applied Informatics
• Rocznik: 2011
• Tom: Vol. 23, No. 3-4
• Strony: 229--243
• Opis fizyczny: Bibliogr. 13 poz., rys.

Twórcy

autor

Rataj A.

autor

Nowak M.

autor

Pecka P.

• Institute of Theoretical and Applied Informatics of the Polish Academy of Sciences

Bibliografia

• [1] R. Alur and T. Henzinger: Reactive modules. Formal Methods in System Design,15(1):7–48, 1999.
• [2] G.J. Holzmann: The SPIN Model Checker: Primer and Reference Manual. AddisonWesley, 2004. ISBN ISBN 0-321-22862-6.
• [3] Kogent Solution Inc. Java 6 Programm ing Black Book. Dreamtech Press, 2007. ISBN 9788177227369.
• [4] S. Khurshid, W. Visser, and C.S. Pasareanu: Test input generation with Java Path Finder.In Proceedings of the ACM/SIGSOFT International Symposiumon Software Testing and Analysis. ACM Press, 2004. ISBN ISBN 1-58113-820-2.
• [5] M. Kwiatkowska, G. Norman, and D. Parker: Probabilistic symbolic model checking with Prism: A hybrid approach. International Journalon Software Tools for Technology Transfer, pages 52–66, 2002.
• [6] M. Kwiatkowska, G. Norman, and D. Parker: Quantitative analysis with the probabilistic model checker PRISM. Electronic Notesin Theoretical Computer Science, 153(2):5–31, 2005.
• [7] M. Kwiatkowska, G. Norman, and D. Parker: Prism: Probabilistic model checking for performance and reliability analysis. ACM SIGMETRICS Performance Evaluation Review, 36(4):40–45, 2009.
• [8] E. Parzen: Stochastic processes. Classics in applied mathematics. Society for Industrial and Applied Mathematics, 1999. ISBN ISBN 9780898714418.
• [9] P. Pecka: Obiektowo zorientowany wielowatkowy system do modelowania stanow nieustalonych w sieciach komputerowych za pomoca lancuchow Markowa, PhD thesis, IITiS PAN, Gliwice, 2002.
• [10] A. Rataj: More flexible models using a new version of the translator of Java sources to times automatons J2TADD. Theoretical and Applied Informatics, 21(2):107–114, 2009.243
• [11] A. Rataj, B. Wozna, and A. Zbrzezny: A translator of Java programs to TADDs. In Concurrency, Specifcation and Programming (CS & P2008), pages 524–535, Gross Vaeternear Berlin, Germany, 2008.
• [12] B. Wozna and A. Zbrzezny: Towards verification of Java programs in VerICS.FundamentaInformaticae, 85(1-4):533–548, 2008.
• [13] F. Yellin and T. Lindholm: Java Virtual Machine Specifcation. Prentice Hall, 1999. ISBN ISBN 978-0201432947.