Efficiently verifying safety properties with idle office computers

Reference:

Marko Mäkelä. Efficiently verifying safety properties with idle office computers. In Charles Lakos, Robert Esser, Lars M. Kristensen, and Jonathan Billington, editors, Formal Methods in Software Engineering and Defence Systems 2002, Conferences in Research and Practice in Information Technology, pages 11–16. Australian Computer Society Inc., June 2002.

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

Suggested BibTeX entry:

@inproceedings{MakelaMarko-Makela:safety,
    author = {Marko M{\"a}kel{\"a}},
    booktitle = {Formal Methods in Software Engineering and Defence Systems 2002},
    editor = {Charles Lakos and Robert Esser and Lars M. Kristensen and Jonathan Billington},
    month = {June},
    pages = {11--16},
    publisher = {Australian Computer Society Inc.},
    series = {Conferences in Research and Practice in Information Technology},
    title = {Efficiently verifying safety properties with idle office computers},
    year = {2002},
}