Towards a Coq-verified Chain of Esterel Semantics
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2019
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929661014966272 |
|---|---|
| author | Berry, Gérard Rieg, Lionel |
| author_facet | Berry, Gérard Rieg, Lionel |
| contents | This paper focuses on formally specifying and verifying the chain of formal semantics of the Esterel synchronous programming language using the Coq proof assistant. In particular, in addition to the standard logical (LBS) semantics, constructive semantics (CBS) and constructive state semantics (CSS), we introduce a novel microstep semantics that gets rid of the Must/Can potential function pair of the constructive semantics and can be viewed as an abstract version of Esterel's circuit semantics used by compilers to generate software code and hardware designs. Excluding the loop construct from Esterel, the paper also provides formal proofs in Coq of the equivalence between the CBS and CSS semantics and of the refinement of the CSS by the microstep semantics. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_1909_12582 |
| institution | arXiv |
| publishDate | 2019 |
| record_format | arxiv |
| spellingShingle | Towards a Coq-verified Chain of Esterel Semantics Berry, Gérard Rieg, Lionel Formal Languages and Automata Theory Logic in Computer Science Programming Languages This paper focuses on formally specifying and verifying the chain of formal semantics of the Esterel synchronous programming language using the Coq proof assistant. In particular, in addition to the standard logical (LBS) semantics, constructive semantics (CBS) and constructive state semantics (CSS), we introduce a novel microstep semantics that gets rid of the Must/Can potential function pair of the constructive semantics and can be viewed as an abstract version of Esterel's circuit semantics used by compilers to generate software code and hardware designs. Excluding the loop construct from Esterel, the paper also provides formal proofs in Coq of the equivalence between the CBS and CSS semantics and of the refinement of the CSS by the microstep semantics. |
| title | Towards a Coq-verified Chain of Esterel Semantics |
| topic | Formal Languages and Automata Theory Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/1909.12582 |