Synchronous Programming with Refinement Types

TL;DR

This paper introduces MARVeLus, a formal language for cyber-physical systems that integrates verification and implementation through a synchronous refinement type system, enabling verified programs to run on real hardware.

Contribution

It presents a formalization and metatheory for MARVeLus, a unified language combining verification and implementation for CPS.

Findings

Verified synchronous programs can execute on real systems.

The type system ensures safety properties in CPS.

Formalization bridges verification and implementation in a single language.

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.