|
モデル駆動開発(MDD:Model driven Development)と呼ばれるコンピュータソフトウェア開発手法が注目を浴びている。現在のMDDには幾つもの課題が残っており、その一つがモデル変換の性質検証である。現在のところ、具体的な一つ一つのモデルが妥当なものであるかを検証する「モデルの型検査」は多くのMDD開発環境で実現されているが、あるモデル変換が常に妥当なモデルを生成する、といった、より強い性質を保証する「モデル変換の型検査」を実現したシステムは存在しない。後者は、伝統的なソフトウェア開発プログラミング書語に対する「静的型検査」に相当し、ソフトウェアの問題点の早期発見に非常に役に立つことが知られているが、モデル変換に対しては未だこのような技法が確立されていないのである。本研究では、この問題の、形式理論およびオートマトン理論と呼ばれる数理的な技法を用いた解決を目指していた。初年度には単方向モデル変換に対する型検査の手法を与え、23年度においては、主に双方向モデル変換に対する型検査の手法を検討した。双方向モデル駆動開発においては、モデル変換を適用した後の出力モデルを編集すると、逆方向の変換によって「編集後の出力モデル(ビュー)を与える様な入力グラフ」が自動的に計算される。そのような入力が存在しない編集を行った場合は、逆変換を行おうとした時点でエラーが報告されることになる。ここで必要な「あるモデル変換の出力となり得ない」といった種類の情報はモデル変換の型情報として捉えて、型検査の手法の応用によってこの情報を計算する方法を追求し、模倣に基づくグラフスキーマを利用して、ビュー更新可能性の判定アルゴリズムを提案した。これによって更新不能なビュー更新を静的に排除できるようになった。
|
