Article: Efficiently verifying safety properties with idle office computers
- Author:
- Marko Mäkelä
- Published in:
- Charles Lakos, Robert Esser, Lars M. Kristensen and Jonathan Billington,
editors, Formal Methods in Software
Engineering and Defence Systems 2002, volume 12 of
Conferences in Research and Practice in
Information Technology
- Pages:
- 11–16
- Abstract:
- Assuring the quality of safety-critical software systems requires
more rigorous methods than testing. Model checking by exhaustive
state space enumeration,
testing all executions,
is an
alternative, but the use of state and memory reduction techniques
makes runtime a major limiting factor. We describe a simple parallel
version of a state space enumeration algorithm that utilises the
unused computing power of office workstations while not congesting
their memories. In an experiment with a complex data link protocol,
our implementation of the algorithm achieves close to linear speedups
on a heterogeneous network of workstations.
- Keywords:
- model checking, distributed algorithm, state space enumeration
- Errata:
- In the bibliography, the entry
Mäkelä,
M. (2002)
should span the page numbers 434–444.
Available in electronic form