PTRebeca: Modeling and analysis of distributed and asynchronous systems

• We presented the SOS rules of PTRebeca, which is an actor-based modeling language.
• The parallel composition approach was introduced for analysis of PTRebeca models.
• The conversion of the TMDP semantics to one Markov automaton (MA) was proposed.
• We mathematically proved that expectation properties are preserved by conversion.
• IMCA tool was used to evaluate a PTRebeca model via analyzing its corresponding MA.

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.