Model Checking in Rebeca

摘要

Rebeca is a recently introduced actor-based language, for modeling concurrent and distributed systems. In this paper, we present our work on model checking Rebeca code. Rebeca is a high level language, comparing to the most of languages used for modeling, in the existing model checker tools. So, we need specific ion techniques for model checking Rebeca code. Here, we show some of these ion techniques used and some case studies. Concurrency, actor model, model checking, ion, Rebeca.