Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Synchronous Programming with Refinement Types

Jiawei Chen, José Luiz Vargas de Mendonça, Bereket Shimels Ayele, Bereket Ngussie Bekele, Shayan Jalili, Pranjal Sharma, Nicholas Wohlfeil, Yicheng Zhang, Jean-Baptiste Jeannin

TL;DR

The paper tackles the challenge of ensuring safety in cyber-physical systems by introducing MARVeLus, a synchronous language augmented with refinement types that enable verification directly in the executable source. It develops a formal metatheory including a time-aware type system with LTL-like predicates, plus a proof of type safety via progress and preservation adapted to streaming semantics. The approach is demonstrated on a robotics collision-avoidance scenario, implemented as an extension to the Zélus compiler and verified with an SMT-based verifier, achieving both simulation and real-world execution within moments. This work bridges verification and deployment for CPS, reducing translation errors and enabling end-to-end confidence in safety-critical behavior.

Abstract

Cyber-Physical Systems (CPS) consist of software interacting with the physical world, such as robots, vehicles, and industrial processes. CPS are frequently responsible for the safety of lives, property, or the environment, and so software correctness must be determined with a high degree of certainty. To that end, simply testing a CPS is insufficient, as its interactions with the physical world may be difficult to predict, and unsafe conditions may not be immediately obvious. Formal verification can provide stronger safety guarantees but relies on the accuracy of the verified system in representing the real system. Bringing together verification and implementation can be challenging, as languages that are typically used to implement CPS are not easy to formally verify, and languages that lend themselves well to verification often abstract away low-level implementation details. Translation between verification and implementation languages is possible, but requires additional assurances in the translation process and increases software complexity; having both in a single language is desirable. This paper presents a formalization of MARVeLus, a CPS language which combines verification and implementation. We develop a metatheory for its synchronous refinement type system and demonstrate verified synchronous programs executing on real systems.

Synchronous Programming with Refinement Types

TL;DR

The paper tackles the challenge of ensuring safety in cyber-physical systems by introducing MARVeLus, a synchronous language augmented with refinement types that enable verification directly in the executable source. It develops a formal metatheory including a time-aware type system with LTL-like predicates, plus a proof of type safety via progress and preservation adapted to streaming semantics. The approach is demonstrated on a robotics collision-avoidance scenario, implemented as an extension to the Zélus compiler and verified with an SMT-based verifier, achieving both simulation and real-world execution within moments. This work bridges verification and deployment for CPS, reducing translation errors and enabling end-to-end confidence in safety-critical behavior.

Abstract

Cyber-Physical Systems (CPS) consist of software interacting with the physical world, such as robots, vehicles, and industrial processes. CPS are frequently responsible for the safety of lives, property, or the environment, and so software correctness must be determined with a high degree of certainty. To that end, simply testing a CPS is insufficient, as its interactions with the physical world may be difficult to predict, and unsafe conditions may not be immediately obvious. Formal verification can provide stronger safety guarantees but relies on the accuracy of the verified system in representing the real system. Bringing together verification and implementation can be challenging, as languages that are typically used to implement CPS are not easy to formally verify, and languages that lend themselves well to verification often abstract away low-level implementation details. Translation between verification and implementation languages is possible, but requires additional assurances in the translation process and increases software complexity; having both in a single language is desirable. This paper presents a formalization of MARVeLus, a CPS language which combines verification and implementation. We develop a metatheory for its synchronous refinement type system and demonstrate verified synchronous programs executing on real systems.
Paper Structure (39 sections, 5 theorems, 12 equations, 15 figures, 1 table)

This paper contains 39 sections, 5 theorems, 12 equations, 15 figures, 1 table.

Table of Contents

  1. Introduction
  2. Overview
  3. A Simple Industrial Controller
  4. Preliminaries
  5. Synchronous Programming
  6. Refinement Types
  7. Verification Via Typing
  8. Syntax
  9. Specification Syntax
  10. Stream Semantics
  11. Summary of Stream Behaviors
  12. Predicate Semantics
  13. State Predicates
  14. Trace Predicates
  15. The MARVeLus Type System
  16. ...and 24 more sections

Key Result

Lemma 1

For any stream $\sigma=(\sigma_0,\ \sigma_1,\ldots)$, if $\sigma \vDash \psi$, then for any other stream $\tau=(\tau_0,\ \tau_1, \ldots)$, $(\sigma_0,\ \tau_1,\ \tau_2...\tau_n...)\vDash{\sf hd}(\psi)$

Figures (15)

  • Figure 1: The industrial controller code with added refinements and external interfaces
  • Figure 2: MARVeLus Syntax
  • Figure 3: Refinement Type Syntax, where we note that $e_1,e_2$ are terms within the logic of quantifier-free equality, uninterpreted functions, and arithmetic (QF-EUFA)
  • Figure 4: Definitions for function environment $S$, term environment $\sigma$, and the histories $h$ of variables bound in $\sigma$
  • Figure 6: MARVeLus Stream Semantics, inspired from existing semantics of Lustre and Esterel ratel1992definitionparissis1996testcolaco2006mixingcaspi_co-iterative_1998
  • ...and 10 more figures

Theorems & Definitions (7)

  • Lemma 1: Correctness of hd
  • Definition 1: Function Environment Correspondence
  • Definition 2: Stream Environment Correspondence
  • Theorem 1: Type Safety
  • Lemma 2: Progress
  • Lemma 3: Temporal Predicate Expansion
  • Lemma 4: Type Preservation