Libdmc とは

LibdmcはLIP6研究所で設計されたライブラリです。その目的は、既存のモデルチェッカーの配布を容易にすることです。また、C ++言語のおかげで、パフォーマンスを犠牲にすることなく最も汎用的なインターフェイスを提供するように設計されています。
モデル検査は、モデル化されたシステムの動作がプロパティを検証することによって正確であることを自動的に証明する方法を提供します。しかし、メモリの集中的な使用によって引き起こされる、いわゆる状態空間爆発の問題がある。この問題を克服するための多くの解決策が提案されているが(例えば、BDDのような意思決定図による記号表現)、これらの方法は、許容できない時間消費に迅速につながる可能性がある。
分散モデル検査は、専用クラスタの集約されたリソースを使用することによって、メモリと時間の両方を克服する方法です。しかし、モデルチェッカー全体を書き直すのは難しい作業なので、libdmcのアプローチはモデルチェッカーを構築するためのフレームワークを与えることです。