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.