The Internet, a huge and open network is rapidly expanding, and distributed
systems there, such as web services, are developing to provide new services.
On the other hand, such a network is still unreliable and insecure.
To overcome this problem, we are doing research on fault tolerance protocols
against two typical types of failures: Byzantine failure and crash failure,
which are designed to work in a huge and open network. In this talk, we first
explain our fault tolerance protocols, and after that, we introduce another
our related work, formal verification methods (model checking) of these
protocols. Here the main issue is model checking of unbounded number of
systems (parameterized systems) against special requirement specifications
of fault tolerance.
|