A calculus for esterel

Spencer P. Florence; Shu Hung You; Jesse Adam Tov; Robert Bruce Findler

doi:10.1145/3290374

A calculus for esterel

Spencer P. Florence, Shu Hung You, Jesse Adam Tov, Robert Bruce Findler

Research output: Contribution to journal › Article › peer-review

4 Scopus citations

Abstract

The language Esterel has found success in many safety-critical applications, such as fly-by-wire systems and nuclear power plant control software. Its imperative style is natural to programmers building such systems and its precise semantics makes it work well for reasoning about programs. Existing semantics of Esterel generally fall into two categories: translation to Boolean circuits, or operational semantics that give a procedure for running a whole program. In contrast, equational theories enable reasoning about program behavior via equational rewrites at the source level. Such theories form the basis for proofs of transformations inside compilers or for program refactorings, and defining program evaluation syntactically. This paper presents the first such equational calculus for Esterel. It also illustrates the calculus's usefulness with a series of example equivalences and discuss how it enabled us to find bugs in Esterel implementations.

Original language	English (US)
Article number	61
Journal	Proceedings of the ACM on Programming Languages
Volume	3
Issue number	POPL
DOIs	https://doi.org/10.1145/3290374
State	Published - Jan 2019

Keywords

Esterel
Semantics
Synchronous Reactive Programming

ASJC Scopus subject areas

Software
Safety, Risk, Reliability and Quality

Access to Document

10.1145/3290374

Cite this

@article{ef28b292f9624f9e91b70449ffd32f88,

title = "A calculus for esterel",

abstract = "The language Esterel has found success in many safety-critical applications, such as fly-by-wire systems and nuclear power plant control software. Its imperative style is natural to programmers building such systems and its precise semantics makes it work well for reasoning about programs. Existing semantics of Esterel generally fall into two categories: translation to Boolean circuits, or operational semantics that give a procedure for running a whole program. In contrast, equational theories enable reasoning about program behavior via equational rewrites at the source level. Such theories form the basis for proofs of transformations inside compilers or for program refactorings, and defining program evaluation syntactically. This paper presents the first such equational calculus for Esterel. It also illustrates the calculus's usefulness with a series of example equivalences and discuss how it enabled us to find bugs in Esterel implementations.",

keywords = "Esterel, Semantics, Synchronous Reactive Programming",

author = "Florence, {Spencer P.} and You, {Shu Hung} and Tov, {Jesse Adam} and Findler, {Robert Bruce}",

note = "Publisher Copyright: {\textcopyright} 2019 Copyright held by the owner/author(s).",

year = "2019",

month = jan,

doi = "10.1145/3290374",

language = "English (US)",

volume = "3",

journal = "Proceedings of the ACM on Programming Languages",

issn = "2475-1421",

publisher = "Association for Computing Machinery (ACM)",

number = "POPL",

}

TY - JOUR

T1 - A calculus for esterel

AU - Florence, Spencer P.

AU - You, Shu Hung

AU - Tov, Jesse Adam

AU - Findler, Robert Bruce

PY - 2019/1

Y1 - 2019/1

N2 - The language Esterel has found success in many safety-critical applications, such as fly-by-wire systems and nuclear power plant control software. Its imperative style is natural to programmers building such systems and its precise semantics makes it work well for reasoning about programs. Existing semantics of Esterel generally fall into two categories: translation to Boolean circuits, or operational semantics that give a procedure for running a whole program. In contrast, equational theories enable reasoning about program behavior via equational rewrites at the source level. Such theories form the basis for proofs of transformations inside compilers or for program refactorings, and defining program evaluation syntactically. This paper presents the first such equational calculus for Esterel. It also illustrates the calculus's usefulness with a series of example equivalences and discuss how it enabled us to find bugs in Esterel implementations.

AB - The language Esterel has found success in many safety-critical applications, such as fly-by-wire systems and nuclear power plant control software. Its imperative style is natural to programmers building such systems and its precise semantics makes it work well for reasoning about programs. Existing semantics of Esterel generally fall into two categories: translation to Boolean circuits, or operational semantics that give a procedure for running a whole program. In contrast, equational theories enable reasoning about program behavior via equational rewrites at the source level. Such theories form the basis for proofs of transformations inside compilers or for program refactorings, and defining program evaluation syntactically. This paper presents the first such equational calculus for Esterel. It also illustrates the calculus's usefulness with a series of example equivalences and discuss how it enabled us to find bugs in Esterel implementations.

KW - Esterel

KW - Semantics

KW - Synchronous Reactive Programming

UR - http://www.scopus.com/inward/record.url?scp=85120130385&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85120130385&partnerID=8YFLogxK

U2 - 10.1145/3290374

DO - 10.1145/3290374

M3 - Article

AN - SCOPUS:85120130385

SN - 2475-1421

VL - 3

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

IS - POPL

M1 - 61

ER -

A calculus for esterel

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this