Open AccessVerification of parallelising transformations of KPN models
Author(s) -
Karfa Chandan,
Sarkar Dipankar,
Mandal Chittaranjan
Publication year - 2019
Publication title -
iet cyber‐physical systems: theory and applications
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.308
H-Index - 7
ISSN - 2398-3396
DOI - 10.1049/iet-cps.2018.5008
Subject(s) - correctness , computer science , programming language , executable , transformation (genetics) , theoretical computer science , model checking , equivalence (formal languages) , formal verification , usability , algorithm , mathematics , operating system , discrete mathematics , biochemistry , chemistry , gene
Parallelising transformations of Kahn process networks (KPNs) are important mechanisms for achieving speedup for deployment on heterogeneous multiprocessor systems particularly in the domain of signal processing applications. Correctness of such parallelising transformations is crucial for their reliable applications. In this study, verification frameworks for checking correctness of sequential to KPN behavioural transformation and KPN level transformations are presented. To the best of the authors’ knowledge, these are the first such approaches for verification problems. The sequential behaviour and the KPN behaviours are both modelled as array data dependence graphs (ADDGs) and the verification problem is posed as the problem of checking of equivalence between the two ADDGs. The key aspect of the proposed scheme is to model a KPN behaviour as an ADDG. Correctness of KPN to ADDG construction method is proved. Experimental results supporting usability of this scheme are also provided.