Affiliations: School of Electrical, Electronic and Computer
Engineering, Merz Court, Newcastle University, Newcastle upon Tyne, NE1 7RU, UK.
danil.sokolov@ncl.ac.uk; ivan.poliakov@ncl.ac.uk; alex.yakovlev@ncl.ac.uk
Note: [] Address for correspondence: School of Electrical, Electronic and
Computer Engineering, Merz Court, Newcastle University, Newcastle upon Tyne,
NE1 7RU, UK
Abstract: A token-based model for asynchronous data path, called static data
flow structures (SDFS), is formally defined. Three token game semantics are
introduced for this model, namely atomic token, spread token and counterflow.
The SDFS semantics are analysed using a simple benchmark example; their
advantages and drawbacks are highlighted. A combination of spread token and
counterflow models, which employs the advantages of both, is presented. A
technique is described for mapping the high-level SDFS token game semantics
into the low level of underlying Petri nets (PNs). The PNs are employed as a
back-end for verification of SDFS models. For analysis and comparison of SDFS
semantics a software tool has been developed, which integrates all SDFS
semantics into a consistent framework, implements their conversion into PNs and
provides an interface to existing model checking tools.
