| 講演名 | 2013-07-25 異なるスキーマ間に対応するSQL文の整合性のAlloy Analyzerを用いた一検証手法 藤田 悠矢, 岡野 浩三, 楠本 真二, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | ビジネスアプリケーション等において,データベーススキーマが正しく設計・分割できていること,そのスキーマに対応するSQL文が正しく記述できていることが保証されているということは非常に重要である.データベーススキーマは慎重に設計を行った場合においても運営上の不具合が生じることや,長期にわたって使用することによりスキーマの構造が時代遅れのものとなることがある.その際業務に適した形ヘスキーマの改良(スキーマ進化)を行う必要性があり,そのスキーマに対するSQL文も新しいスキーマに適するものに変換する必要がある.一方,ソフトウェアの仕様を形式的に記述できる言語にAlloyがあり,Alloyの制約記述に対してその制約を満たす例(インスタンス),満たさない例(反例)を有界網羅的に検出するAlloyAnalyzerというツールがある.本研究では,スキーマ変更に伴うSQL文の変換が正しく行われていることの確認をAlloyAnalyzerによって行う手法を提案し,その手法の正しさの数学証明を行った.また,ケーススタディとして在庫管理プログラムで用いるデータベーススキーマに対して手法を適用し,その有用性の確認を行った.結果,AlloyAnalyzerにおいてスキーマとSQL文の整合性を確認することができた. |
| 抄録(英) | In software using database, it is very important that database schema is properly designed to assure that and also that SQL statements which correspond to the schema are correctly described. Long-term operation sometimes, however, causes operational defects becuase database shema might not fit to the current deployment despite that it was carefully designed in the past. In such a case, we have to perform improvement of the schema (Schema evolution) to a form suitable for the work, and also we have to convert the SQL statements into a form suitable for new schema. Alloy is a language which can formally describe specification of software. Alloy Analyzer is a tool to find instances that satisfy the constraint described in Alloy or counterexamples that do not satisfy. This report proposes a method that lets Alloy Analyzer verify if the conversion of SQL statements associated with the given schema modification have conformance. It also gives mathematical proof of the correctness of the method. The method is applied to the database schema used in a warehouse management program as a case study to confirm its usefulness. The author consequently can verify the conformance of the SQL statements using Alloy Analyzer. |
| キーワード(和) | Alloy / SQL / スキーマ変換 / 在庫管理問題 |
| キーワード(英) | Alloy / SQL / Schema evolution / Warehouse Management Program |
| 資料番号 | SS2013-14,KBSE2013-14 |
| 発行日 |
| 研究会情報 | |
| 研究会 | KBSE |
|---|---|
| 開催期間 | 2013/7/18(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Knowledge-Based Software Engineering (KBSE) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 異なるスキーマ間に対応するSQL文の整合性のAlloy Analyzerを用いた一検証手法 |
| サブタイトル（和） | |
| タイトル（英） | A Verification Method on Consistency between Different SQL Statements and Schemas using Alloy Analyzer |
| サブタイトル（和） | |
| キーワード(1)（和/英） | Alloy / Alloy |
| キーワード(2)（和/英） | SQL / SQL |
| キーワード(3)（和/英） | スキーマ変換 / Schema evolution |
| キーワード(4)（和/英） | 在庫管理問題 / Warehouse Management Program |
| 第 1 著者 氏名（和/英） | 藤田 悠矢 / Yuya FUJITA |
| 第 1 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Osaka University |
| 第 2 著者 氏名（和/英） | 岡野 浩三 / Kozo OKANO |
| 第 2 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Osaka University |
| 第 3 著者 氏名（和/英） | 楠本 真二 / Shinji KUSUMOTO |
| 第 3 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Osaka University |
| 発表年月日 | 2013-07-25 |
| 資料番号 | SS2013-14,KBSE2013-14 |
| 巻番号（vol） | vol.113 |
| 号番号（no） | 160 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |