Synchronous Programming and Refinement Types in Robotics: From Verification to Implementation
Jiawei Chen

, José Luiz Vargas de Mendonça

, Shayan Jalili

, Bereket Ayele

, Bereket Ngussie Bekele

, Zhemin Qu

, Pranjal Sharma

, Tigist Shiferaw

, Yicheng Zhang

, and Jean-Baptiste Jeannin
(University of Michigan at Ann Arbor, USA; Addis Ababa Institute of Technology, Ethiopia)
Robots and other cyber-physical systems are held to high standards of safety and reliability, and thus one must be confident in the correctness of their software. Formal verification can provide such confidence, but programming languages that lend themselves well to verification often do not produce executable code, and languages that are executable do not typically have precise enough formal semantics. We present MARVeLus, a stream-based approach to combining verification and execution in a synchronous programming language that allows formal guarantees to be made about implementation-level source code. We then demonstrate the end-to-end process of developing a safe robotics application, from modeling and verification to implementation and execution.
@InProceedings{FTSCS22p68,
author = {Jiawei Chen and José Luiz Vargas de Mendonça and Shayan Jalili and Bereket Ayele and Bereket Ngussie Bekele and Zhemin Qu and Pranjal Sharma and Tigist Shiferaw and Yicheng Zhang and Jean-Baptiste Jeannin},
title = {Synchronous Programming and Refinement Types in Robotics: From Verification to Implementation},
booktitle = {Proc.\ FTSCS},
publisher = {ACM},
pages = {68--79},
doi = {10.1145/3563822.3568015},
year = {2022},
}
Publisher's Version