Poster: An Efficient Equivalence Checking Method for Petri Net Based Models of Programs

The initial behavioural specification of any software programs goes through significant optimizing and parallelizing transformations, automated and also human guided, before being mapped to an architecture. Establishing validity of these transformations is crucial to ensure that they preserve the original behaviour. PRES+ model (Petri net based Representation of Embedded Systems) encompassing data processing is used to model parallel behaviours. Being value based with inherent scope of capturing parallelism, PRES+ models depict such data dependencies more directly; accordingly, they are likely to be more convenient as the intermediate representations (IRs) of both the source and the transformed codes for translation validation than strictly sequential variable-based IRs like Finite State Machines with Data path (FSMDs) (which are essentially sequential control flow graphs (CFGs)). In this work, a path based equivalence checking method for PRES+ models is presented.