Melola Discovery

← Melola Discovery

Open access Jurnal SINTA 2

Verifikasi Dua Varian Protokol Ad hoc On demand Distance Vector dengan UPPAAL

IJCCS (Indonesian Journal of Computing and Cybernetics Systems) · Vol. 9 No. 1 (2015) · pp. 13–22

DOI
10.22146/ijccs.6636
ISSN
2460-7258, 1978-1520
Published
2015-01-31
Publisher
IndoCEISS in colaboration with Universitas Gadjah Mada, Indonesia.
Language
eng
License
creativecommons.org/licenses/by-sa/4.0

Abstract

AbstrakMobile Ad-hoc Network (MANET) adalah sekumpulan wireless mobile yang terhubung satu sama lain tanpa infrastruktur yang tetap sehingga perubahan topologi dapat terjadi setiap saat. Protokol routing MANET memiliki dua model yaitu protokol routing reaktif yang membentuk tabel routing hanya saat dibutuhkan dan protokol routing proaktif yang melakukan pemeliharaan tabel routing secara berkala. Properti umum yang harus dipenuhi oleh protokol jaringan ad-hoc adalah route discovery, packet delivery dan loop fredom. AODV merupakan protokol reaktif MANET yang memiliki standar waktu berapa lama sebuah rute dapat digunakan (route validity), sehingga properti route discovery dan packet delivery harus dapat dipenuhi dalam waktu tersebut. Proses verifikasi protokol dilakukan dengan memodelkan spesifikasi protokol menggunakan teknik, tool, dan bahasa matematis. Pada penelitian ini bahasa pemodelan yang digunakan adalah timed automata, yaitu bahasa pemodelan untuk memodelkan sistem yang memiliki ketergantungan terhadap waktu tertentu pada setiap prosesnya. Verifikasi protokol dilakukan secara otomatis dengan mengggunakan tool model checker UPPAAL.Protokol yang diverifikasi adalah protokol AODV Break Avoidance milik Ali Khosrozadeh dkk dan protokol AODV Reliable Delivery dari Liu-Jian dan Fang-Min. Hasil verifikasi protokol membuktikan bahwa protokol AODV Break Avoidance mampu memenuhi properti route discovery dan protokol AODV Reliable Delivery mampu memenuhi properti packet delivery dalam waktu sesuai dengan spesifikasi. Kata kunci —Verifikasi Protokol, Timed Automata, AODV, UPPAAL Abstract MANET is a group of wireless mobile that connected one to each other without fixed infrastructure so topology could change at anytime. MANET routing protocol has two models which are reactive routing protocol that built routing table only when needed and proactive routing protocol that maintain routing table periodically. General property which had to be satisfied by ad-hoc network protocol are route discovery, packet delivery and loop freedom. AODV is a reactive protocol in MANET that has time standard to determine how long a route is valid to be used (route validity) so route discovery and packet delivery property should be satisfied in a specifically certain time. Protocol verification process done by modeling protocol specification using technique, tool and mathematic language.In this research protocol modeled using timed automata which is a modeling language that could be used to model a time dependent system in each process. Verification using timed automata can automatically done by UPPAAL tool model checker.Protocol which will be verified are AODV Break Avoidance by Ali Khosrozadeh et al. and AODV Reliable Delivery by Liu Jian and Fang-Min. Result of this protocol verification prove that AODV BA could satisfied route discovery property and AODV Reliable Delivery could satisfied packet delivery property within their specification time. Keywords—Protocol Verification, Timed Automata, AODV, UPPAAL

Collaboration network of the authors

17 authors · 24 co-authorship links · 4 across different organisations

Hover or tap a name to highlight its co-authors. Double-click to open the author's page.

  • Universitas Gadjah Mada
  • Udayana University
  • Universitas Halu Oleo
  • Affiliation unknown
  • Different organisations
  • Same organisation
  • Affiliation unknown
  • Thicker line = more joint articles · bigger circle = more articles
Show as table
Co-authorOrganisationJoint articles
Gede Saindra SantyadiAffiliation unknown1
Anindita SuryarasmiUniversitas Gadjah Mada1
La SurimiUniversitas Halu Oleo1
Agus HalidUniversitas Gadjah Mada1
Yoga Dwitya PramuditaUniversitas Gadjah Mada1
I Nym Saputra Wahyu WijayaAffiliation unknown1
Rachmat Wahid Saleh InsaniUniversitas Gadjah Mada1
Afiahayati AfiahayatiUniversitas Gadjah Mada1
Muhammad IhsanAffiliation unknown1
Muhammad Asghar NazalUniversitas Gadjah Mada1
Mardhani RiasetiawanUniversitas Gadjah Mada1
Ni Made Ary Esta Dewi WirastutiUdayana University1
I Dewa Made Bayu Atmaja DarmawanUdayana University1
LinawatiAffiliation unknown1
Gede SukadarmikaUdayana University1

Affiliations come from OpenAlex; journal OAI-PMH metadata carries none. Authors without an OpenAlex ID are matched by name, which can merge or split people.

Metadata source: OAI-PMH (metadata jurnal) https://journal.ugm.ac.id/ijccs/oai, first harvested 26 Okt 2026, last seen 26 Okt 2026.
Original metadata (oai_dc) 
<oai_dc:dc xmlns="http://www.openarchives.org/OAI/2.0/" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:oai_dc="http://www.openarchives.org/OAI/2.0/oai_dc/" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://www.openarchives.org/OAI/2.0/oai_dc/  http://www.openarchives.org/OAI/2.0/oai_dc.xsd">
	<dc:title xml:lang="en-US">Verifikasi Dua Varian Protokol Ad hoc On demand Distance Vector dengan UPPAAL</dc:title>
	<dc:creator>Suzanti, Ika Oktavia</dc:creator>
	<dc:creator>Pulungan, Reza</dc:creator>
	<dc:description xml:lang="en-US">AbstrakMobile Ad-hoc Network (MANET) adalah sekumpulan wireless mobile yang terhubung satu sama lain tanpa infrastruktur yang tetap sehingga perubahan topologi dapat terjadi setiap saat. Protokol routing MANET memiliki dua model yaitu protokol routing reaktif yang membentuk tabel routing hanya saat dibutuhkan dan protokol routing proaktif yang melakukan pemeliharaan tabel routing secara berkala. Properti umum yang harus dipenuhi oleh protokol jaringan ad-hoc adalah route discovery, packet delivery dan loop fredom. AODV merupakan protokol reaktif MANET yang memiliki standar waktu berapa lama sebuah rute dapat digunakan (route validity), sehingga properti route discovery dan packet delivery harus dapat dipenuhi dalam waktu tersebut. Proses verifikasi protokol dilakukan dengan memodelkan spesifikasi protokol menggunakan teknik, tool, dan bahasa matematis. Pada penelitian ini bahasa pemodelan  yang digunakan adalah timed automata, yaitu bahasa pemodelan untuk memodelkan sistem yang memiliki ketergantungan terhadap waktu tertentu pada setiap prosesnya. Verifikasi protokol dilakukan secara otomatis dengan mengggunakan tool model checker UPPAAL.Protokol yang diverifikasi adalah protokol AODV Break Avoidance milik Ali Khosrozadeh dkk dan protokol AODV Reliable Delivery dari Liu-Jian dan Fang-Min. Hasil verifikasi protokol membuktikan bahwa protokol AODV Break Avoidance mampu memenuhi properti route discovery dan protokol AODV Reliable Delivery mampu memenuhi properti packet delivery dalam waktu sesuai dengan spesifikasi. Kata kunci —Verifikasi Protokol, Timed Automata,  AODV, UPPAAL Abstract MANET is a group of wireless mobile that connected one to each other without fixed infrastructure so topology could change at anytime. MANET routing protocol has two models which are reactive routing protocol that built routing table only when needed and proactive routing protocol that maintain routing table periodically. General property which had to be satisfied by ad-hoc network protocol are route discovery, packet delivery and loop freedom. AODV is a reactive protocol in MANET that has time standard to determine how long a route is valid to be used (route validity) so route discovery and packet delivery property should be satisfied in a specifically certain time. Protocol verification process done by modeling protocol specification using technique, tool and mathematic language.In this research protocol modeled using timed automata which is a modeling language that could be used to model a time dependent system in each process. Verification using timed automata can automatically done by UPPAAL tool model checker.Protocol which will be verified are AODV Break Avoidance by Ali Khosrozadeh et al. and AODV Reliable Delivery by Liu Jian and Fang-Min. Result of this protocol verification prove that AODV BA could satisfied route discovery property and AODV Reliable Delivery could satisfied packet delivery property within their specification time. Keywords—Protocol Verification, Timed Automata, AODV, UPPAAL</dc:description>
	<dc:publisher xml:lang="en-US">IndoCEISS in colaboration with Universitas Gadjah Mada, Indonesia.</dc:publisher>
	<dc:contributor xml:lang="en-US">IndoCEISS</dc:contributor>
	<dc:date>2015-01-31</dc:date>
	<dc:type>info:eu-repo/semantics/article</dc:type>
	<dc:type>info:eu-repo/semantics/publishedVersion</dc:type>
	<dc:type xml:lang="en-US"></dc:type>
	<dc:format>application/pdf</dc:format>
	<dc:identifier>https://journal.ugm.ac.id/ijccs/article/view/6636</dc:identifier>
	<dc:identifier>10.22146/ijccs.6636</dc:identifier>
	<dc:source xml:lang="en-US">IJCCS (Indonesian Journal of Computing and Cybernetics Systems); Vol 9, No 1 (2015): January; 13-22</dc:source>
	<dc:source>2460-7258</dc:source>
	<dc:source>1978-1520</dc:source>
	<dc:language>eng</dc:language>
	<dc:relation>https://journal.ugm.ac.id/ijccs/article/view/6636/5184</dc:relation>
	<dc:rights xml:lang="en-US">Copyright (c) 2015 IJCCS - Indonesian Journal of Computing and Cybernetics Systems</dc:rights>
	<dc:rights xml:lang="en-US">http://creativecommons.org/licenses/by-sa/4.0</dc:rights>
</oai_dc:dc>