Toward the Formal Verification of HILECOP: Formalization and Implementation of Synchronously Executed Petri Nets - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier Access content directly
Reports (Research Report) Year : 2020

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

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.
Fichier principal
Vignette du fichier
main.pdf (774.61 Ko) Télécharger le fichier
PNSE20.tar.gz (1.25 Mo) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

lirmm-02611153 , version 1 (18-05-2020)

Identifiers

  • HAL Id : lirmm-02611153 , version 1

Cite

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⟩
211 View
209 Download

Share

Gmail Facebook X LinkedIn More