| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Formal verification of automatically generated C-code from polychronous data-flow equations
Abstract : Synchronous data-flow languages are used as design approaches in developing embedded and critical real-time systems in which synchronous programs are verified by applying formal verification. In a synchronous design approach, transformation and optimization are used to transform synchronous programs and generate general purpose executable code. The incorrectness of the transformations make the guarantees unable to carry over the transformed programs and the executable code. In this work, adopting the translation validation approach, we present an automated verification process to verify the correctness of the synchronous language compiler Signal transformations and code generation on the clock information.
Cited literature [23 references]
https://hal.inria.fr/hal-00763781
Contributor : van Chan Ngo <>
Submitted on : Wednesday, December 12, 2012 - 11:07:54 AM
Last modification on : Friday, January 8, 2021 - 3:40:37 AM
Long-term archiving on: : Sunday, December 18, 2016 - 12:08:58 AM
Contributor : van Chan Ngo <>
Submitted on : Wednesday, December 12, 2012 - 11:07:54 AM
Last modification on : Friday, January 8, 2021 - 3:40:37 AM
Long-term archiving on: : Sunday, December 18, 2016 - 12:08:58 AM
File
report.pdf
Files produced by the author(s)