情報処理学会 第79回全国大会講演要旨

プレース/トランジションネットは，並行処理を含むソフトウェアの振舞いを形式的に記述することに適した表記法のひとつである．本研究では，より複雑な振舞いを表現できるように拡張されたプレース/トランジションネットに基づいて，形式的仕様記述言語VDM++によって記述されたVDM仕様を構築する手法を提案する．まず，拡張プレース/トランジションネットについて定義し，これとVDM仕様との対応関係を明らかにする．そして，ソフトウェアの仕様の動的検証やテストケースの設計，評価などにこのVDM仕様を応用する方法について考察する．