=Paper=
{{Paper
|id=Vol-2651/posterextabs1
|storemode=property
|title=Toward the Formal Verification of HILECOP: Formalization and Implementation of Synchronously Executed Petri Nets
|pdfUrl=https://ceur-ws.org/Vol-2651/posterextabs1.pdf
|volume=Vol-2651
|authors=Vincent Iampietro,David Andreu,David Delahaye
|dblpUrl=https://dblp.org/rec/conf/apn/IampietroAD20
}}
==Toward the Formal Verification of HILECOP: Formalization and Implementation of Synchronously Executed Petri Nets==
https://ceur-ws.org/Vol-2651/posterextabs1.pdf
Toward the Formal Verification of HILECOP:
Formalization and Implementation of
Synchronously Executed Petri Nets?
Vincent Iampietro1 , David Andreu1,2 , and David Delahaye1
1
LIRMM, Univ Montpellier, CNRS, Montpellier, France
2
NEURINNOV, Montpellier, France
Firstname.Lastname@lirmm.fr
While designing critical digital systems, the use of formal models is necessary
as they help us to assess the design soundness with the help of their mathemat-
ical foundations. However, the formal model is then frequently hand-coded by
the engineer, sometimes with automatic generation of a code skeleton to be
completed. While automatic generation facilitates the task and limits the risk
of error, it remains to be proved that the properties highlighted in the design
model are preserved in its implemented version, while considering the impact of
its execution on the target as well.
analysis
feedback
ma ext
n
tio
correction analysis sis /
for o-t
ng &
he n
nt tio
ns l-t
tte ing
sy pila
tra ode
ni
fla mbl
m
m
se
co
Component C1 Component C2
behavior interface interface behavior
VHDL
P1 P1
as
T1 P1−c1 P1−c2 T1
P1 P1
P2 P2
T2−c1 T2−c2
T2 T2
T1 T1
Source
s1 s2−c1 s2−c2 s1
s2 s2
Component C3
interface behavior
P2 P2
Code
P1
P1−c2 T1
T2−c2
P2
T2 T2
T2
s2−c2 s1
s2
Implementation
Abstract model FPGA
model 2 3 implementation
1 4
Fig. 1: Workflow of the HILECOP Methodology
We propose to address the problem within the framework of the HILECOP
(HIgh-LEvel hardware COmponent Programming) methodology. As shown in
Fig. 1, the HILECOP methodology describes a full fledged process to design, an-
alyze, and synthesize critical digital systems. In HILECOP, the models of digital
systems are built leveraging a modular, component-based graphical formalism
(see 1 in Fig. 1). The internal behavior of the model components are described
with a particular kind of Petri nets that we call SITPNs (Synchronously exe-
cuted Interpreted Time Petri Nets with priorities). The SITPN formalism allows
us to analyze the models (see 2 in Fig. 1). Up to that point, the HILECOP
?
Copyright c 2020 for this paper by its authors. Use permitted under Creative Com-
mons License Attribution 4.0 International (CC BY 4.0).
Formalization and Implementation of Synchronously Executed Petri Nets 215
methodology provides a way to design sound models that ensure properties such
as boundedness and liveliness. From Step 2 to Step 3 , the SITPN model is
then transformed into VHDL code. Currently, there is no proof that the struc-
ture and behavior of the implementation model are preserved in the generated
VHDL code. Using theorem proving and the Coq proof assistant [4] in particular,
we propose to formally verify the above statement.
This verification task is somewhat similar to the verification of compilers for
programming languages (see [2], for an example). In this kind of verification, the
steps to establish the proof of behavior preservation are well-known: first, formal-
ize and implement the semantics of the source and the target languages; second,
implement the transformation; finally, prove that for all source program, the gen-
erated program has the same behavior. However, contrary to usual programming
languages, our source formalism is very abstract, and the target language is very
specific, as VHDL describes both the structure and the behavior of hardware
circuits. These particular aspects bring a certain originality to our work.
To complete the verification of HILECOP, the first step consists in formalizing
the semantics of SITPNs, and implementing it in Coq. The SITPN semantics is a
state-transition system. It has been thoroughly formalized in [1,3]. We provided
only minor changes to this semantics, most of them to correct redundancies.
SITPNs combine multiple classes of PNs such as time and interpreted PNs.
However, the singularity of SITPNs resides in the synchronous execution of the
models. The evolution of the overall state of an SITPN depends on the two
events of a clock signal: the falling edge and the rising edge. These two events
label the transitions of the state-transition system. The election of the transitions
to be fired takes place on the falling edge and the update of the marking takes
place on the rising edge. The major impact of synchronous execution is that all
transitions are fired at the same time.
Our first contribution to the verification of HILECOP has been to implement
the SITPN semantics in Coq. To increase our confidence in our implementation
of the SITPN semantics, we have also developed an SITPN token player in Coq
and proved that it is sound and complete with respect to the SITPN semantics.
The full formalization and proof are available to the reader3 .
References
1. H. Leroux. Handling Exceptions in Petri Net-Based Digital Architecture: From For-
malism to Implementation on FPGAs. IEEE Transactions Industrial Informatics,
11(4):897–906, Aug. 2015.
2. X. Leroy. Formal Verification of a Realistic Compiler. Communications of the ACM
(CACM), 52(7):107–115, July 2009.
3. I. Merzoug. Validation formelle des systèmes numériques critiques : génération de
l’espace d’états de réseaux de Petri exécutés en synchrone. PhD thesis, Université
Montpellier, Jan 2018.
4. The Coq Development Team. Coq, version 8.11.0. Inria, Jan. 2020.
http://coq.inria.fr/.
3
https://github.com/viampietro/sitpns