To Crash or Not to Crash: Efficient Modeling of Fail-Stop Faults
Source: Technische Universitat Darmstadt
A commonly used approach in practical verification is to verify a simplified model of the system rather than the system itself, which would entail infeasible verification complexity. This paper introduces a model for efficient model checking of message-passing systems with crash faults. The key to the achieved efficiency is the intuition that the event of process crash can be omitted in the model as crashed processes can be mimicked by "Slow" ones. The authors formally prove this intuition for a general class of systems and their specifications. They evaluate model checking efficiency using two models, one where crash events are modeled as separate state transitions (explicit model) and another where these events are omitted (implicit model).