Automatically Tracking Model Based Testing of Asynchronously Communicated Protocol Implementations

Abstract

Automatic testing of protocol implementations given only a formal protocol specification has long since been achieved for synchronously communicated protocols. However, acquiring similar results under asynchronous communication is not straightforward and has not been practically achievable. This work solves state-space explosions due possible interleaving of events under asynchronous communication through inference optimization from a refined concept of soundness. Additionally, the high concurrent nature of asynchronously communicating systems necessitated a shift from formally specifying protocols using Labeled Transition Systems to formally specifying protocols using Petri Nets. An EDSL for describing protocols in parallel composed structures has been defined that translates to Petri Net structure. These achievements have resulted in a first concrete fundamental foundation to enable practical application of automatic testing theory to asynchronously communicated protocols.