Skip to Main content Skip to Navigation
Reports

Toward the Formal Verification of HILECOP: Formalization and Implementation of Synchronously Executed Petri Nets

Vincent Iampietro 1 David Andreu 2, 3 David Delahaye 4
1 CAMIN - Control of Artificial Movement and Intuitive Neuroprosthesis
LIRMM - Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier, CRISAM - Inria Sophia Antipolis - Méditerranée
4 MAREL - Models And Reuse Engineering, Languages
LIRMM - Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier
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.
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download

https://hal-lirmm.ccsd.cnrs.fr/lirmm-02611153
Contributor : Vincent Iampietro <>
Submitted on : Monday, May 18, 2020 - 10:59:30 AM
Last modification on : Thursday, May 21, 2020 - 1:41:03 AM

Identifiers

  • HAL Id : lirmm-02611153, version 1

Collections

Citation

Vincent Iampietro, David Andreu, David Delahaye. Toward the Formal Verification of HILECOP: Formalization and Implementation of Synchronously Executed Petri Nets. [Research Report] LIRMM, Université de Montpellier. 2020. ⟨lirmm-02611153⟩

Share

Metrics

Record views

41

Files downloads

73