PhD Defense TD - Ali Jafari
Student: Ali Jafari
Title: Performance Evaluation and Model Checking of Probabilistic Real-time Actors
Abstract: This dissertation is composed of two parts. In the first part, performance evaluation and verification of safety properties are provided for real-time actors. We use Timed Rebeca, an actor-based modeling language, to model distributed and asynchronous systems with timing constraints and message passing communication. A toolset is developed for automated translation of Timed Rebeca models to Erlang programs. The translated code can be executed using a timed extension of McErlang for model checking and simulation. We also provide statistical model checking of Timed Rebeca models. Using statistical model checking, we are able to verify larger models against safety properties comparing to McErlang model checking.
In the second part of this dissertation, we enhance our modeling ability and cover more properties by performance evaluation and model checking of probabilistic real-time actors. 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 (TMDP). We provide SOS rules for PTRebeca, and develop two approaches and their corresponding toolsets for analyzing PTRebeca models. In each toolset a different backend model checker is used. We use PRISM for the first toolset and IMCA for the second one. Using these toolsets, we are able to analyze PTRebeca models against expected reachability and probabilistic reachability properties