Proving a Petri net model-checker implementation - Université d'Évry Access content directly
Reports (Research Report) Year : 2011

Proving a Petri net model-checker implementation

Abstract

Petri nets are a widely used tool in verification through model-checking. In this approach, a Petri Net model of the system of interest is produced and its reachable states are computed, searching for erroneous executions. Compilation of such a Petri net model is one way to accelerate its verification. It consists in generating code to explore the reachable states of the considered Petri net, which avoids the use of a fixed exploration tool involving an "interpretation" of the Petri net structure. In this paper, we show how to compile Petri nets targeting the LLVM language (a high-level assembly language) and formally prove the correct-ness of the produced code. To this aim, we define a structural operational semantics for the fragment of LLVM we use. The acceleration obtained from the presented compilation techniques has been evaluated in [6].
Fichier principal
Vignette du fichier
FP-IBISC-TR-2011.pdf (456.75 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-02315062 , version 1 (14-10-2019)

Identifiers

  • HAL Id : hal-02315062 , version 1

Cite

Lukasz Fronc, Franck Pommereau. Proving a Petri net model-checker implementation. [Research Report] IBISC, university of Evry / Paris-Saclay. 2011. ⟨hal-02315062⟩
43 View
107 Download

Share

Gmail Facebook X LinkedIn More