| 研究概要 |
本研究では,ソフトウェア開発において益々必要性が増す形式手法・形式的検証の大衆化を目指し,ソフトウェア開発工程の全体を一貫して取り扱うことが可能な言語を構築し,研究者ではない一般ソフトウェア開発者にも利用可能な支援ツールを開発することを目的とする.厳密な数学的モデルを持ち形式的検証も可能な代数仕様を中心に,直観的な要求仕様などを記述するUMLなどの図的表現から,プログラミング言語による実装・テストまでを統一して扱うことが可能なシステムを構築する.ソフトウェア開発の流れで生成される中間成果物である要求仕様,設計仕様,実装,テストなどの各種文書の円滑な取り扱いを可能とするため,応募者が提案したモジュラー項書換えシステムの理論を応用し,文書間の変換規則,および仕様と実装が融合した"半仕様・半実装"の操作的意味を与える.
本年度は,主に文書間の変換規則についての研究成果,および実行に適した仕様作成の基礎理論についての研究成果を得た.文書間の変換規則では,等式仕様から書き換え仕様への異なる仕様間の変換規則をまとめ,ツール開発を行い,文献[1]で研究成果を公表した.実行に適した仕様作成の基礎理論では,仕様実行の際に重要となる実行停止性に対し,代数仕様の仕様作成者に理解がしやすい代数モデルに基づく停止性判定手法を提案し,文献[2]で研究成果を公表した.
[1]Min Zhang,Kazuhiro Ogata,Masaki Nakamura:Translation of State Machines from Equational Theories into Rewrite Theories with Tool Support.IEICE Transactions 94-D(5):976-988(2011)
[2]Masaki Nakamura,Kazuhiro Ogata,Kokichi Futatsugi,On Describing Terminating Algebraic Specifications Based on Their Models,Proceedings of the International Multi Conference of Engineers and Computer Scientists 2012,IMECS 2012,pp.269-274,2012.
|
