Check and simulate: A case for incorporating model checking in network simulation

Ahmed Sobeih, Mahesh Viswanathan, Jennifer C. Hou

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Existing network simulators perform reasonably well in evaluating the performance of network protocols, but lack the capability of verifying and validating the correctness of network protocols. In this paper, we have extended J-Sim - an open-source, component-based compositional network simulation environment - with the model checking capability to explore the state space created by a network protocol until either the entire state space is explored (if the state space is finite) or an error (e.g., a violation of a user-defined safety assertion) is discovered. We also exploit protocol-specific properties in the process of exploring the state space, to reduce the size of the state space and to guide the (best-first) search towards paths that can potentially locate errors in less time. As a proof of concept, we have demonstrated use of the J-Sim model checker in locating errors in an automatic repeat request (ARQ) protocol. As compared to the Maude LTL model checker, the J-Sim model checker can locate errors in a more timely manner and with shorter error traces.

Original languageEnglish (US)
Title of host publicationProceedings - 2nd ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'04
Pages27-36
Number of pages10
StatePublished - Dec 1 2004
EventProceedings - 2nd ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'04 - San Diego, CA, United States
Duration: Jun 23 2004Jun 25 2004

Publication series

NameProceedings - 2nd ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'04

Other

OtherProceedings - 2nd ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'04
CountryUnited States
CitySan Diego, CA
Period6/23/046/25/04

    Fingerprint

ASJC Scopus subject areas

  • Engineering(all)

Cite this

Sobeih, A., Viswanathan, M., & Hou, J. C. (2004). Check and simulate: A case for incorporating model checking in network simulation. In Proceedings - 2nd ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'04 (pp. 27-36). (Proceedings - 2nd ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'04).