Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. Model Checking a Networked System Without the Network
 
conference paper

Model Checking a Networked System Without the Network

Guerraoui, Rachid  
•
Yabandeh, Maysam  
2011
Proceedings of the 8th USENIX Symposium on Networked Systems Design and Implementation (NSDI '11)
8th USENIX Symposium on Networked Systems Design and Implementation (NSDI '11)

Current approaches to model checking distributed systems reduce the problem to that of model checking centralized systems: global states involving all nodes and communication links are systematically explored. The frequent changes in the network element of the global states lead however to a rapid state explosion and make it impossible to model check any non-trivial distributed system. We explore in this paper an alternative: a local approach where the network is ignored, a priori: only the local nodes' states are explored and in a separate manner. The set of valid system states is a subset of all combinations of the node local states and checking validity of such a combination is only performed a posteriori, in case of a possible bug. This approach drastically reduces the number of transitions executed by the model checker. It takes for example the classic global approach several minutes to explore the interleaving of messages in the celebrated Paxos distributed protocol even considering only three nodes and a single proposal. Our local approach explores the entire system state in a few seconds. Our local approach does clearly not eliminate the state exponential explosion problem. Yet, it postpones its manifestations till some deeper levels. This is already good enough for online testing tools that restart the model checker periodically from the current live state of a running system. We show for instance how this approach enables us to find two bugs in variants of Paxos.

  • Files
  • Details
  • Metrics
Loading...
Thumbnail Image
Name

Model_checking_a_netw_Guerraoui.pdf

Type

Preprint

cris-layout.advanced-attachment.oaire.version

http://purl.org/coar/version/c_71e4c1898caa6e32

Access type

openaccess

Size

348.92 KB

Format

Adobe PDF

Checksum (MD5)

25971cacbe20c62e9d461ce78e692022

Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés