モデル規範型形式手法VDMと仕様記述言語VDM++－高信頼性システムの開発に向けて－

摘要

産業界での業務としてのシステム開発においては，開発対象や体制が大規模化，複雑化していく中で，複数人で効率良く品質の高いソフトウェアを開発し，プロジェクトやチームで責任を果たしていく必要がある．このためには，仕様の厳密な記述と検証による，開発の上流工程における成果物の品質確保が鍵となる．厳密な仕様の記述と検証，維持により，開発や運用，保守を正確に行うことができるようになるのである．様々な抽象度の仕様を厳密に記述し，これを検証するための手段として，数多くの形式仕様記述言語や仕様記述支援ツールが提案されており，これらを活用した開発手法の一つとして，モデル規範型の形式手法がある．本稿では，モデル規範型の形式手法と，形式仕様記述言語VDM＋＋，仕様記述支援ツールVDMTooIsについて，主に抽象的な仕様を厳密に記述し，テストするための言語の仕様やツールの機能と，仕様記述の効果，信頼性や安全性の確保に向けた可能性等について解説する．