MODELLING AND VERIFICATION OF KITSAT PACKET COMMUNICATION PROTOCOLS

In this paper, in order to verify KITSAT 1/2 packet communication protocols, we model the AX.25 protocol and PACSAT protocol by using an extended Petri net and then verify the correctness, boundedness, liveness and deadlock freeness of packet protocols by utilizing reachability trees.

Bibliographic Details
Main Authors: Young-Ro Lee, Dan Keun Sung
Format: Article
Language:English
Published: The Korean Space Science Society 1996-06-01
Series:Journal of Astronomy and Space Sciences
Online Access:http://ocean.kisti.re.kr/downfile/volume/kosss/OJOOBS/1996/v13n2/OJOOBS_1996_v13n2_134.pdf
Description
Summary:In this paper, in order to verify KITSAT 1/2 packet communication protocols, we model the AX.25 protocol and PACSAT protocol by using an extended Petri net and then verify the correctness, boundedness, liveness and deadlock freeness of packet protocols by utilizing reachability trees.
ISSN:2093-5587
2093-1409