20 Years of Actor Model Checking with Rebeca From Dining Philosophers to Micro-services
摘要
Micro-service architecture, combined with message-passing tools such as Kafka, is nowadays widely used in software systems. However, this leads to highly concurrent behavior, making it susceptible to subtle design flaws. In this paper, we survey the two decades of research and development in the actor-based modeling language Rebeca and its model checking toolset, and explore how it can be leveraged to ensure the correctness of software with these modern designs.