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
_version_ 1797369783195271168
author Young-Ro Lee
Dan Keun Sung
author_facet Young-Ro Lee
Dan Keun Sung
author_sort Young-Ro Lee
collection DOAJ
description 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.
first_indexed 2024-03-08T17:51:53Z
format Article
id doaj.art-28f8debb34224fa1848d448db9fd6268
institution Directory Open Access Journal
issn 2093-5587
2093-1409
language English
last_indexed 2024-03-08T17:51:53Z
publishDate 1996-06-01
publisher The Korean Space Science Society
record_format Article
series Journal of Astronomy and Space Sciences
spelling doaj.art-28f8debb34224fa1848d448db9fd62682024-01-02T07:05:42ZengThe Korean Space Science SocietyJournal of Astronomy and Space Sciences2093-55872093-14091996-06-01132134148MODELLING AND VERIFICATION OF KITSAT PACKET COMMUNICATION PROTOCOLSYoung-Ro Lee0Dan Keun Sung1Department of Computer Science, Chungnam Sanup UniversitySatellite Technology Research Center, KAIST, Taejon 305-701In 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.http://ocean.kisti.re.kr/downfile/volume/kosss/OJOOBS/1996/v13n2/OJOOBS_1996_v13n2_134.pdf
spellingShingle Young-Ro Lee
Dan Keun Sung
MODELLING AND VERIFICATION OF KITSAT PACKET COMMUNICATION PROTOCOLS
Journal of Astronomy and Space Sciences
title MODELLING AND VERIFICATION OF KITSAT PACKET COMMUNICATION PROTOCOLS
title_full MODELLING AND VERIFICATION OF KITSAT PACKET COMMUNICATION PROTOCOLS
title_fullStr MODELLING AND VERIFICATION OF KITSAT PACKET COMMUNICATION PROTOCOLS
title_full_unstemmed MODELLING AND VERIFICATION OF KITSAT PACKET COMMUNICATION PROTOCOLS
title_short MODELLING AND VERIFICATION OF KITSAT PACKET COMMUNICATION PROTOCOLS
title_sort modelling and verification of kitsat packet communication protocols
url http://ocean.kisti.re.kr/downfile/volume/kosss/OJOOBS/1996/v13n2/OJOOBS_1996_v13n2_134.pdf
work_keys_str_mv AT youngrolee modellingandverificationofkitsatpacketcommunicationprotocols
AT dankeunsung modellingandverificationofkitsatpacketcommunicationprotocols