Continuous time Markov chains (CTMC) are one of the formalisms for building models. This paper discusses OLYMP2 - a system for solving big CTMC models (exceeding $$10^9$$ states), described with a standard programming language - Java. OLYMP2 is primarily aimed at modelling of computer networks, so its formalism comes from networking concepts, like queueing systems. Using Java as a model description allows for greater flexibility in comparison to model-checker specific languages that often do not employ complete features of an object-oriented programming. Using Java also makes the parsing of models relatively fast, due to optimised Java run-time environment. Introducing dedicated compression of transition matrices allows for keeping memory usage at reasonable level even for large models.
原文链接
分享
引用
