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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

20 Years of Actor Model Checking with Rebeca From Dining Philosophers to Micro-services

  • Ehsan Khamespanah,
  • Mohammad Mahdi Jaghoori

摘要

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.