Volume 12 Number 4 (Apr. 2017)
Home > Archive > 2017 > Volume 12 Number 4 (Apr. 2017) >
JSW 2017 Vol.12(4): 253-264 ISSN: 1796-217X
doi: 10.17706/jsw.12.4.253-264

Verification of an Ad-hoc Serial Communication Protocol through Model-checking: A Case Study with Echo Sounder

Shakaiba Majeed1, Kashif Saghar2, Kashif Hameed2, Minsoo Ryu3*
1Department of Computer and Software, Hanyang University, Seoul, South Korea
2CESAT, 44000, Islamabad, Pakistan
3Department of Computer Science and Engineering, Hanyang University, Seoul, South Korea

Abstract—Serial data transmission accounts for a considerable share of the overall communication involved in real-time embedded systems. Although there are some standard serial protocols, many systems still use ad-hoc serial protocols for communication between a control computer and a serial peripheral device. Such protocols may have flaws in them which cannot be revealed by computer simulations or testing only. To complement testing, formal methods are now widely used and have proved effective in the verification of various communication protocols. However, for serial communication specifically, most of the previous research is focused on applying formal methods for the verification of standard serial interfaces. In the current work instead, we use formal methods to verify an ad-hoc serial communication protocol between a control computer and an echo sounder. Through our case study, we show how we integrated formal modeling and model-checking methods in an existing system and as a result, we were able to discover a fault in the protocol design, which could have gone unnoticed without formal software verification.

Index Terms—Formal-modeling, model-checking, fault-injection, serial data transmission.


Cite: Shakaiba Majeed, Kashif Saghar, Kashif Hameed, Minsoo Ryu, "Verification of an Ad-hoc Serial Communication Protocol through Model-checking: A Case Study with Echo Sounder," Journal of Software vol. 12, no. 4, pp. 253-264, 2017.

General Information

ISSN: 1796-217X
Frequency: Monthly
Editor-in-Chief: Prof. Antanas Verikas
Executive Editor: Ms. Yoyo Y. Zhou
Abstracting/ Indexing: DBLP, EBSCO, DOAJ, ProQuest, INSPEC, ULRICH's Periodicals Directory, WorldCat, CNKI,etc
E-mail: jsw@iap.org
  • Aug 02, 2017 News!

    Papers published in JSW Vol. 12, No. 1- Vol. 12, No. 8 have been indexed by DBLP.    [Click]

  • Jan 05, 2017 News!

    [CFP] 2017 the annual meeting of JSW Editorial Board, ICSTE 2017, will be held in Hong Kong, October 27-29, 2017.   [Click]

  • Sep 27, 2017 News!

    Vol.12, No.5 has been indexed by EI (Inspec).   [Click]

  • Oct 30, 2017 News!

    Vol 12, No. 11 has been published with online version 8 original aritcles from 4 countries are published in this issue.      [Click]

  • Oct 30, 2017 News!

    The papers published in Vol.12, No. 11 have all received dois from Crossref.