Statistical model checking of Timed Rebeca models
2016 (English)In: Computer languages, systems & structures, ISSN 1477-8424, E-ISSN 1873-6866, Vol. 45, 53-79 p.Article in journal (Refereed) Published
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 statisticalmodel 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 statisticalmodel checking and applicability of our toolset.
Place, publisher, year, edition, pages
2016. Vol. 45, 53-79 p.
IdentifiersURN: urn:nbn:se:mdh:diva-34106DOI: 10.1016/j.cl.2016.01.004ScopusID: 2-s2.0-84961214168OAI: oai:DiVA.org:mdh-34106DiVA: diva2:1056031