An efficient path based equivalence checking for Petri net based models of programs

A user written program goes through significant optimizing and parallelizing transformations, both (compiler) automated and human guided, before being mapped to an architecture. Formally verifying these transformations is crucial to ensure that they preserve the original behavioural specification. The PRES+ model (Petri net based Representation of Embedded Systems) encompassing data processing is used to model parallel behaviours more succinctly. Being value based with a natural capability of capturing parallelism, PRES+ models depict such data dependencies more vividly; accordingly, they are likely to be more convenient as the intermediate representations (IRs) of both source and transformed codes for translation validation than strictly sequential, variable-based IRs such as Finite State Machines with Data path (FSMDs) which are essentially sequential control and data flow graphs (CDFGs). This paper presents a scheme for verifying equivalence between two given PRES+ models for translation validation of optimizing and parallelizing code transformations; one of the two models represents the source code and the other represents its optimized and (or) parallelized version.