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.
Main Authors: | , |
---|---|
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 |