|
モデル駆動開発(MDD:Model Driven Development)と呼ばれるコンピュータソフトウェア開発手法が注目を浴びている。現在のMDDには幾つもの課題が残っており、その一つがモデル変換の性質検証である。現在のところ、具体的な一つ一つのモデルが妥当なものであるかを検証する「モデルの型検査」は多くのMDD開発環境で実現されているが、あるモデル変換が常に妥当なモデルを生成する、といった、より強い性質を保証する「モデル変換の型検査」を実現したシステムは存在しない。後者は、伝統的なソフトウェア開発プログラミング言語に対する「静的型検査」に相当し、ソフトウェアの問題点の早期発見に非常に役に立つことが知られているが、モデル変換に対しては未だこのような技法が確立されていないのである。本研究では、この問題の、形式論理およびオートマトン理論と呼ばれる数理的な技法を用いた解決を目指している。平成22年度は、我々の提案した双方向モデル変換システムGRoundTramでの変換記述言語として使用されている、グラフ変換言語UnQLおよびそのコア代数UnCALの型検査手法を研究し、単項二階論理(MSO)と呼ばれる論理の真偽判定問題へモデル変換の型検査問題を帰着させる方法を示した。また、MONAという既存のMSO実装系を活用し、高速な実装を行った。
|
