2010 Fiscal Year Annual Research Report
モジュラー書換え理論に基づく代数型ソフトウェア開発言語の構築
| Project/Area Number |
22700027
|
|---|
| Research Institution | Kanazawa University |
|---|
Principal Investigator |
中村 正樹 金沢大学, 電子情報学系, 助教 (40345658)
|
|---|
| Keywords | 代数仕様 / 仕様変換 / 仕様検証 / UML / 形式手法 / 項書き換えシステム / CafeOBJ / Maude |
|---|
| Research Abstract |
本研究では,ソフトウェア開発において益々必要性が増す形式手法・形式的検証の大衆化を目指し,ソフトウェア開発工程の全体を一貫して取り扱うことが可能な言語を構築し,研究者ではない一般ソフトウェア開発者にも利用可能な支援ツールを開発することを目的とする.厳密な数学的モデルを持ち形式的検証も可能な代数仕様を中心に,直観的な要求仕様などを記述するUMLなどの図的表現から,プログラミング言語による実装・テストまでを統一して扱うことが可能なシステムを構築する.ソフトウェア開発の流れで生成される中間成果物である要求仕様,設計仕様,実装,テストなどの各種文書の円滑な取り扱いを可能とするため,応募者が提案したモジュラー項書換えシステムの理論を応用し,文書間の変換規則,および仕様と実装が融合した"半仕様・半実装"の操作的意味を与える.
初年度は,主に異なる仕様間の検証技術の融合の研究を行った.代数仕様言語CafeOBJで記述された観測遷移機械(OTS)仕様(等式仕様)の検証をMaude言語の書き換え仕様に変換することで,Maude言語の全自動網羅探索やモデル検査を,元のOTS仕様の検証に役立てることができる.入力OTS仕様を限定することにより,この変換技術をより実用的なものに発展させ,変換ツールYASTを開発した.この成果は,国際会議ICFEM 2010で発表された(論文:Specification Translation of State Machines from Equational Theories into Rewrite Theories).その他,仕様から実装技術については,代数仕様からのテスト生成技術の並行プログラムへの発展や,仕様実行・検証のためめ代数仕様作成手法の研究などを行った.
|
Research Products
(2 results)
