|
Title
|
|
|
|
PNPEq : verification of scheduled conditional behavior in embedded software using Petri nets
|
|
|
Author
|
|
|
|
|
|
|
Abstract
|
|
|
|
| Software for embedded systems goes through a scheduling phase where it is subjected to optimizing transformations. In such a scenario, validating the preservation of semantics across the transformation is essential. In this paper, we present PNPEq (Petri Net Program Equivalence), an ongoing work on a novel translation validation technique to handle various schedule-time conditional optimizations among others. The method makes use of a reduced size Petri net model integrating SMT solvers for validating arithmetic transformations. The approach is illustrated with a simple program and its translation, and further validated with a preliminary example suite. |
|
|
|
Language
|
|
|
|
English
|
|
|
Source (book)
|
|
|
|
2021 28th Asia-Pacific Software Engineering Conference (APSEC), 06-09 December 2021 , Taipei, Taiwan
|
|
|
Publication
|
|
|
|
2021
|
|
|
ISSN
|
|
|
|
2640-0715
|
|
|
ISBN
|
|
|
|
978-1-6654-3784-4
|
|
|
DOI
|
|
|
|
10.1109/APSEC53868.2021.00059
|
|
|
Volume/pages
|
|
|
|
(2021)
, p. 509-514
|
|
|
ISI
|
|
|
|
000802192700052
|
|
|
Full text (Publisher's DOI)
|
|
|
|
|
|
|
Full text (publisher's version - intranet only)
|
|
|
|
|
|