https://www.mdu.se/

Distributed systems exhibit probabilistic and non-deterministic behaviors and may have time constraints. Probabilistic Timed Rebeca (PTRebeca) is introduced as a timed and probabilistic actor-based language for modeling distributed real-time systems with asynchronous message passing. The semantics of PTRebeca is a Timed Markov Decision Process. In this paper, we provide SOS rules for PTRebeca, introduce a new tool-set and describe the corresponding mappings. The tool-set automatically generates a Markov Automaton from a PTRebeca model in the form of the input language of the Interactive Markov Chain Analyzer (IMCA). The IMCA can be used as a back-end model checker for performance analysis of PTRebeca models against expected reachability and probabilistic reachability properties. Comparing to the existing tool-set, proposed in the conference paper, we now have the ability of analyzing significantly larger models, and we also can add different rewards to the model. We show the applicability of our approach and efficiency of our tool by analyzing a Network on Chip architecture as a real-world case study. (C) 2016 Elsevier B.V. All rights reserved.