Efficiently Verifying Safety Properties with Idle Office Computers

Makela, M.

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.

Cite as: Makela, M. (2002). Efficiently Verifying Safety Properties with Idle Office Computers. In Proc. Workshop on Software Engineering and Formal Methods 2002, Adelaide, Australia. CRPIT, 12. Lakos, C., Esser, R., Kristensen, L. M. and Billington, J., Eds. ACS. 11-16.

(from crpit.com) (local if available)