Abstract
The complexity of digital hardware systems makes it difficult to produce them without the help of computers. The "HILECOP (HIgh LEvel hardware COmponent Programming) methodology" assists the engineers in the design and production of such systems. The context of production is the one of safety-critical digital systems, i.e. systems which failure could result in direct human losses, natural catastrophes, economic disasters, etc. To give an example, the Neurinnov company leverages the HILECOP methodology to produce highly critical medical devices known as neuroprostheses. In HILECOP, engineers rely on a graphical formalism, based on component diagrams and a particular kind of Petri Nets (PNs), to produce a model of a digital system. Then, a computer program turns the model into an intermediary description written in VHDL (Very high speed integrated circuit Hardware Description Language). Finally, an industrial compiler/synthesizer transforms the VHDL description into a concrete physical circuit on an FPGA, or as an ASIC. The use of PNs permits the engineers to describe a formal model of a digital system. The mathematical foundations of PNs enable the use of model-checking techniques. Thus, a proof can be brought that the produced models verify certain soundness properties. However, one transformation step happening in the methodology could alter the behavior of the initial model. The goal of this thesis is to bring the formal proof that the model-to-text transformation from a HILECOP high-level model to a VHDL description is semantic preserving (or behavior preserving); i.e. for all high-level model given as an input to the transformation, the resulting VHDL description behaves similarly. To perform this task, we draw our inspiration from the works pertaining to the formal verification of compilers for programming languages (especially from the certified C compiler CompCert). Specifically, we are interested in proving the property of semantic preservation in the context of deductive verification with proof assistants. In this context, the steps to verify that a transformation is semantic preserving include: (1) the formalization of the execution semantics of thesource representation, (2) of the target representation, (3) the formal description of the transformation, and (4) the proof of a corresponding semantic preservation theorem. In this thesis, these steps have been carried within the framework of the Coq proof assistant. Even though these steps are clearly set, the specificities of the HILECOP model-to-text transformation, compared to compilers for generic programming languages, bring some interesting research challenges. Finally, we have brought the proof on paper that the HILECOP transformation is semantic preserving by demonstrating a related correctness theorem. The full mechanization of the proof using the Coq proof assistant is an ongoing task.