Mechanized semantics and verified compilation for a dataflow synchronous language with reset

Autor: Lélio Brun, Timothy Bourke, Marc Pouzet
Přispěvatelé: Université Paris sciences et lettres (PSL), Département d'informatique - ENS Paris (DI-ENS), Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL), Parallélisme de Kahn Synchrone ( Parkas), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Département d'informatique - ENS Paris (DI-ENS), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS), Sorbonne Université (SU), Bpifrance Invest for the Future Program ('Programme d’Investissements d’Avenir') in the ES3CAP project, ES3CAP, École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria), Département d'informatique de l'École normale supérieure (DI-ENS), École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS Paris)
Jazyk: angličtina
Rok vydání: 2020
Předmět:
CCS Concepts: • Software and its engineering → Formal language definitions
Interactive theorem proving
Computer science
Dataflow
Stateflow
02 engineering and technology
computer.software_genre
• Computer systems organization → Embedded software Additional Key Words and Phrases: stream languages
Software verification
0202 electrical engineering
electronic engineering
information engineering
Verified compilation
Safety
Risk
Reliability and Quality
computer.programming_language
Finite-state machine
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
Assembly language
Programming language
Lustre (programming language)
Proof assistant
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
020207 software engineering
computer.file_format
020202 computer hardware & architecture
Compilers
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
[INFO.INFO-ES]Computer Science [cs]/Embedded Systems
Compiler
Executable
computer
Software
Zdroj: Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2020, 4 (POPL), pp.1-29. ⟨10.1145/3371112⟩
Proceedings of the ACM on Programming Languages, 2020, 4 (POPL), pp.1-29. ⟨10.1145/3371112⟩
ISSN: 2475-1421
Popis: Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications. Tools like SCADE Suite and Simulink/Stateflow are equipped with compilers that translate such specifications into executable code. They provide programming languages for composing functions over streams as typified by Dataflow Synchronous Languages like Lustre. Recent work builds on CompCert to specify and verify a compiler for the core of Lustre in the Coq Interactive Theorem Prover. It formally links the stream-based semantics of the source language to the sequential memory manipulations of generated assembly code. We extend this work to treat a primitive for resetting subsystems. Our contributions include new semantic rules that are suitable for mechanized reasoning, a novel intermediate language for generating optimized code, and proofs of correctness for the associated compilation passes.
Databáze: OpenAIRE
Externí odkaz: