マルチスレッドプログラミングにおける単体テスト

URLメモ プログラミング

研究用に開発しているグラフシミュレータは、各ノードがマルチスレッドで動作します（だから、機能シミュレーションしかできず、時間を正確に扱う必要があるシミュレーションはできない。サイクルアキュレートモデルみたいなもの）。で、現在マルチスレッドにおいて、どうすれば容易にテスト（主に単体テスト）が行えるか考えています。
以下、URLメモです。

  • Multithreaded Tests with JUnit

http://today.java.net/pub/a/today/2003/08/06/multithreadedTests.html

  • Thread Debugger

http://www.borland.co.jp/optimizeit/opt4.2/thread_debug.html

  • GrobUtils

http://groboutils.sourceforge.net/codecoverage/index.html

  • Jlint

http://artho.com/jlint/download.shtml

http://www.willowriver.net/products/download_jlint.php
私が行いたいテストは、二つのスレッドが１つのリソースにアクセスするとき、スレッドがいかなる動きをしても、リソースはある定められた状態にあるというものです。二つのスレッドで安全性を証明できれば、あとは数学的帰納法を用いて、複数のスレッドでも安全であると証明できると考えています。ですから、時相論理を用いた形式的検証を行うことができれば一番いいのですのが、そこまで手の込んだことはしたくないんですよね。