モジュール合成を用いたソフトウェア設計における仕様の充足性検証に関する考察

摘要

現在，大規模なシステムを信頼性が確認されたモジュールを合成することで実現することが多く行われている．その際に，個々のモジュールやモジュールを合成して実現したシステム全体が仕様書を満たしているか否かを検証する必要がある．本論文では，仕様書をモジュールの接続関係と特定のモジュール接続箇所でのデータのドメインを規定したものと考え，各モジュール固有の入出力データのドメインと仕様書に記載されているデータドメインを用いて，合成したシステムがその仕様書を満たしているか否かを検証する手法を提案する．