Ranch: Rebeca On Chip
摘要
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.