xmldtp https://blog.hatena.ne.jp/xmldtp/ ウィリアムのいたずらの、まちあるき、たべあるきーPART2 https://xmldtp.hatenadiary.org/ そのほか 複数プロセスが並行して動いているとき、ある性質(デッドロックしないとか）を満たしているかどうかを確かめる（場合によっては線形時相論理LTLを使って） モデル検査ツールにＳＰＩＮがある。 このＳＰＩＮにおいて、プロセスは、Promela という言語で記述（モデル化）するわけだけど、 実際のプロセスって言うのはＵＭＬなんかで書かれていることが多いわけなので、 Promela に落とすには、どうしたらいいか？ていう話になる。 この落とし方を教わったんだけど、時間がたつと忘れそうなのでメモメモ （ただし、自分が理解した範囲なので、これでいいかどうかは？） ■ステートチャート図からの落とし方 １．mty… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fxmldtp.hatenadiary.org%2Fentry%2F6805d25aeea3988999bfa52970995f45" title="UMLのステートチャート図から、並行動作、線形時相論理の検証をするSPINへの落とし方 - ウィリアムのいたずらの、まちあるき、たべあるきーPART2" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2010-06-30 17:34:47 rich https://xmldtp.hatenadiary.org/entry/6805d25aeea3988999bfa52970995f45 1.0 100%