複数のスレッドが共有リソースにアクセスしたとき、
デッドロックが発生しない設計になっていることを示す
設計資料の作り方に困っています。

ひとまず、共有リソースの種類と、各スレッドがどういう処理の中でリード/ライトアクセスするか
の洗い出しまでは終わりました。

リソースのロック状態、処理イベントで状態遷移図をつくってみたのですが、
他のスレッドが共有リソースをロックしていたら、
・ロック取得に失敗してリトライする（ノンブロッキングの場合）
・またはロックが開放されるまで待ち続ける（ブロッキングの場合）
という当たり前を記載しているだけで
デッドロックが発生しない説明になってないと思えてきました。

一般的には、どのような種類の設計書（タイミングチャート？シーケンス図？その他？）を作成してデッドロックが発生しない設計かを検証するのか教えていただけないでしょうか？

特に具体的な資料が表示してるURLを教えていただければ、大変助かります。