1. Toward the Formal Verification of HILECOP: Formalization and Implementation of Synchronously Executed Petri Nets
- Author
-
Iampietro, Vincent, Andreu, David, Delahaye, David, Contrôle Artificiel de Mouvements et de Neuroprothèses Intuitives (CAMIN), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier (LIRMM), Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM), NEURINNOV, Models And Reuse Engineering, Languages (MAREL), Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM)-Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM), and LIRMM, Université de Montpellier
- Subjects
Critical Digital Systems ,[INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] ,HILECOP Methodology ,Petri Nets ,[SPI.NANO]Engineering Sciences [physics]/Micro and nanotechnologies/Microelectronics ,Coq Proof Assistant ,Formal Verification - Abstract
The HILECOP methodology is a process for the design of critical digital systems. In HILECOP, Petri Net (PN) models are used as a high-level formalism to specify the behavior of the designed systems. VHDL (VHSIC Hardware Description Language) code is then automatically generated from PN models to implement the digital system on Field Programmable Gate Array (FPGA) circuits. The goal of this work is to formally verify that through this model-to-text transformation, the behavior described by a PN model is preserved in the produced VHDL code, knowing that the transformed PN models are synchronously executed on the target. As a first step toward the achievement of this goal, we present our implementation of HILECOP's PN structure and semantics , which has been formalized using the Coq proof assistant. We also describe a token player program for these PNs, which has been proved sound and complete with respect to HILECOP's PN semantics.
- Published
- 2020