Pemodelan dan Verifikasi Formal Protokol EE-OLSR dengan UPPAAL CORA
Rachmat Wahid Saleh Insani(1*), Reza Pulungan(2)
(1) 
(2) Jurusan Ilmu Komputer dan Elektronika, FMIPA UGM, Yogyakarta
(*) Corresponding Author
Abstract
Protocol verification process generally be done by simulation and testing. However, these processes unable to verify there are no subtle error or design flaw in protocol. Model Checking is an algorithmic method runs in fully automatic to verify a system. UPPAAL is a model checker tool to model, verify, and simulate a system in Timed Automata.
UPPAAL CORA is model checker tool to verify EE-OLSR protocol modelled in Linearly Priced Timed Automata, if the protocol satisfy the energy efficient property formulated by formal specification language in Weighted Computation Tree Logic syntax. Model Checking Technique to verify the protocols results in the protocol is satisfy the energy efficient property only when the packet transmission traffic happens.
Keywords
Full Text:
PDFReferences
Wibling, O., Parrow, J. dan Pears, A., 2004. Automatized Verification of Ad Hoc Routing Protocols. Formal Techniques for Networked and Distributed Systems, 325, pp.343–358.
Rango, F. De, Fotino, M. dan Marano, S., 2008. EE-OLSR: Energy Efficient OLSR routing protocol for Mobile ad-hoc Networks. MILCOM 2008 - 2008 IEEE Military Communications Conference, pp.1–7.
Jacquet, P. dan Clausen, T., 2001. Optimized link state routing protocol for ad hoc networks. … , 2001. Ieee Inmic …, 2001, pp.62–68. Available at: http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=995315.
Baier, C. dan Katoen, J.-P., 2008. Principles Of Model Checking, The MIT Press. Available at: http://mitpress.mit.edu/books/principles-model-checking.
Berard, B. et al., 2010. System and Software Verification: Model Checking Techniques and Tools, Springer Publishing Company.
Larsen, K.G., Pettersson, P. & Yi, W., 1997. Uppaal in a nutshell. International Journal on Software Tools for Technology Transfer, 1(1-2), pp.134–152.
Brihaye, T., Bruyère, V. dan françois Raskin, J., 2004. Model-Checking for Wei- ghted Timed Automata, in In Proceeding of FORMATS-FTRTFT’04, Lect. Notes Comput. Sci. 3253 , 277–292, Springer, pp. 277–292.
Höfner, P. dan Mciver, A., 2013. Statistical Model Checking of Wireless Mesh Routing Protocols. In NASA Formal Methods. pp. 322–336.
Prakash, R., 2001. A routing algorithm for wireless ad hoc networks with unidirectional links. Wireless Networks, 7(6), pp.617–625.
Fehnker, A., van Glabbeek, R., Hofner, P., McIver, A., Portmann, M., dan Tan, W. L., 2011. Modelling and Analysis of AODV in UPPAAL. In 1st International Workshop on Rigorous Protocol Engineering.
DOI: https://doi.org/10.22146/ijccs.11192
Article Metrics
Abstract views : 2479 | views : 2211Refbacks
- There are currently no refbacks.
Copyright (c) 2016 IJCCS - Indonesian Journal of Computing and Cybernetics Systems
This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.
View My Stats1