異なるスキーマ間に対応するSQL文の整合性のAlloy Analyzerを用いた一検証手法

摘要

ビジネスアプリケーション等において，データベーススキーマが正しく設計·分割できていること，そのスキーマに対応するSQL文が正しく記述できていることが保証されているということは非常に重要である．データベーススキーマは慎重に設計を行った場合においても運営上の不具合が生じることや，長期にわたって使用することによりスキーマの構造が時代遅れのものとなることがある．その際，業務に適した形へスキーマの改良（スキーマ進化）を行う必要性があり，そのスキーマに対するSQL文も新しいスキーマに適するものに変換する必要がある．一方，ソフトウェアの仕様を形式的に記述できる言語にAlloyがあり，Alloyの制約記述に対してその制約を満たす例（インスタンス），満たさない例（反例）を有界網羅的に検出するAlloy Analyzerというツールがある．本研究では，スキーマ変更に伴うSQL文の変換が正しく行われていることの確認をAlloy Analyzerによって行う手法を提案し，その手法の正しさの数学証明を行った．また，ケーススタディとして在庫管理プログラムで用いるデータベーススキーマに対して手法を適用し，その有用性の確認を行った．結果，Alloy AnalyzerにおいてスキーマとSQL文の整合性を確認することができた．