Cプログラムの検証をモデル検査でNECや松下が相次ぎ技術開発: LSI設計の検証技術を応用

摘要

NECおよび松下電器産業は，「モ デル検査（model checking）」と呼ぶ 技術を応用して，メモリ・リークなど C言語プログラムの実行時エラーを検 出する技術を，それぞれ開発した。 一般にメモリ・リークなどの実行時 エラーは，プログラムを実際に実行す るテスト，特に開発工程後半のシステ ム・テスト時に検出することが多いが， 今回の技術は一種の静的検証ツール として利用できるため，ソース・コード が出来上がった直後など，開発工程 のより早い段階でこれらの不具合を 検出しやすくなる利点がある。