Destructive testing of software systems by model checking

Recently, software verification using model checkers has achieved widespread success. It can locate hard-to-find bugs in software by exhaustively searching executing paths. In this paper, we propose a new software design method that enables the evaluation of the fault tolerance of software behavior at the specification level: we can check software behavior, not only when the hardware and network are in good order, but also when they are out of order; we can then improve fault tolerance of the target software using the model checker. We can test software under environments in which we destroy hardware and/or networks intentionally, not in situ, but in silico (in computer simulation).