Actor-based languages have attracted much interest in industry and academia. In particular, Rebeca is an actor-based language which offers model checking back-end to ensure absence of any unwanted behavior in the model. After ensuring that a model is correct, an important challenge is the correct implementation of the actor model on the computer. In this work, we present Ranch, a prototype tool that correctly compiles a subset of Rebeca into assembly. In the conducted tests, the target of the translation is ARM Cortex-M3 microcontrollers. With formal verification of this compilation, Ranch guarantees that the Rebeca model and the implementation have the same operational semantics. Our experiments show how Ranch translates some Rebeca models into real hardware and demonstrate the applicability of our approach.

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

Ranch: Rebeca On Chip

  • Meyssam Rostamzadeh,
  • Mahboubeh Samadi,
  • Fatemeh Ghassemi,
  • Hossein Hojjat

摘要

Actor-based languages have attracted much interest in industry and academia. In particular, Rebeca is an actor-based language which offers model checking back-end to ensure absence of any unwanted behavior in the model. After ensuring that a model is correct, an important challenge is the correct implementation of the actor model on the computer. In this work, we present Ranch, a prototype tool that correctly compiles a subset of Rebeca into assembly. In the conducted tests, the target of the translation is ARM Cortex-M3 microcontrollers. With formal verification of this compilation, Ranch guarantees that the Rebeca model and the implementation have the same operational semantics. Our experiments show how Ranch translates some Rebeca models into real hardware and demonstrate the applicability of our approach.