Synchronous Programming with Refinement Types
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866909303885004800 |
|---|---|
| author | Chen, Jiawei de Mendonça, José Luiz Vargas Ayele, Bereket Shimels Bekele, Bereket Ngussie Jalili, Shayan Sharma, Pranjal Wohlfeil, Nicholas Zhang, Yicheng Jeannin, Jean-Baptiste |
| author_facet | Chen, Jiawei de Mendonça, José Luiz Vargas Ayele, Bereket Shimels Bekele, Bereket Ngussie Jalili, Shayan Sharma, Pranjal Wohlfeil, Nicholas Zhang, Yicheng Jeannin, Jean-Baptiste |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_06221 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Synchronous Programming with Refinement Types Chen, Jiawei de Mendonça, José Luiz Vargas Ayele, Bereket Shimels Bekele, Bereket Ngussie Jalili, Shayan Sharma, Pranjal Wohlfeil, Nicholas Zhang, Yicheng Jeannin, Jean-Baptiste Programming Languages 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. |
| title | Synchronous Programming with Refinement Types |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2406.06221 |