Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6871020 | Computer Languages, Systems & Structures | 2016 | 33 Pages |
Abstract
The actor-based language, Timed Rebeca, was introduced to model distributed and asynchronous systems with timing constraints and message passing communication. A toolset was developed for automated translation of Timed Rebeca models to Erlang. The translated code can be executed using a timed extension of McErlang for model checking and simulation. In this work, we added a new toolset that provides statistical model checking of Timed Rebeca models. Using statistical model checking, we are now able to verify larger models against safety properties compared to McErlang model checking. We examine the typical case studies of elevators and ticket service to show the efficiency of statistical model checking and applicability of our toolset.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Ali Jafari, Ehsan Khamespanah, Haukur Kristinsson, Marjan Sirjani, Brynjar Magnusson,