UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

Implementation of a protocol validation and synthesis system Tong, Darren Pong-Choi


VALISYN, an automated system for the validation and synthesis of error-free protocols has been implemented in C language. It assists designers in the detection and prevention of various kinds of potential design errors, such as state deadlocks, non-executable interactions, unspecified receptions and state ambiguities. The technique employed is a stepwise application of a set of production rules which guarantee complete reception capability. These rules are implemented in a tracking algorithm, which prevents the formation of non-executable interactions and unspecified receptions, and which monitors the existence of state deadlocks and state ambiguities. The implementation of VALISYN is discussed and a number of protocol validation and synthesis examples are presented to illustrate its use and features.

Item Media

Item Citations and Data


For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.