2014/11/20 by Ali Jafari, Ehsan Khamespanah, Jafari, Ali +5
Computer Science · #Formal Methods in Verification #Petri Nets in System Modeling #Real-Time Systems Scheduling
paper · doi:10.14279/tuj.eceasst.70.984.963
openalex publication_date 2014/11/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/01
Abstract: Many real-time distributed applications exhibit probabilistic and non-deterministic behaviors. In this paper, we introduce Probabilistic Timed Rebeca (PTRebeca) as an actor-based language for modeling probabilistic distributed real-time systems with asynchronous message passing. We pro-pose the semantics of PTRebeca model in Timed Markov Decision Process (TMDP), the integral semantics of probabilistic timed automaton (PTA) with one digital clock. To analyze PTRebeca models, we develop a tool set to au-tomatically generate a TMDP model from a PTRebeca model in the form of the input language of PRISM model checker. We use PRISM for performance analysis of PTRebeca models against expected reachability and probabilistic reachability properties. We show the applicability of our approach using a few case studies and experimental results.