Skip to main navigation Skip to search Skip to main content

PNPEq: Verification of Scheduled Conditional Behavior in Embedded Software using Petri Nets

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

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.

Original languageEnglish
Title of host publicationProceedings - 2021 28th Asia-Pacific Software Engineering Conference, APSEC 2021
PublisherIEEE Computer Society
Pages509-514
Number of pages6
ISBN (Electronic)9781665437844
DOIs
Publication statusPublished - 1 Jan 2021
Event28th Asia-Pacific Software Engineering Conference, APSEC 2021 - Virtual, Online, Taiwan, Province of China
Duration: 6 Dec 20219 Dec 2021

Publication series

NameProceedings - Asia-Pacific Software Engineering Conference, APSEC
Volume2021-December
ISSN (Print)1530-1362

Conference

Conference28th Asia-Pacific Software Engineering Conference, APSEC 2021
Country/TerritoryTaiwan, Province of China
CityVirtual, Online
Period6/12/219/12/21

Keywords

  • Conditional optimization
  • Path-based analysis
  • Petri net
  • Program equivalence
  • Translation validation

Fingerprint

Dive into the research topics of 'PNPEq: Verification of Scheduled Conditional Behavior in Embedded Software using Petri Nets'. Together they form a unique fingerprint.

Cite this