2011 Fiscal Year Research-status Report
分散システムの振る舞いモデル自動合成のためのネット理論展開
| Project/Area Number |
23500045
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
宮本 俊幸 大阪大学, 工学(系)研究科(研究院), 准教授 (00294041)
|
|---|
| Project Period (FY) |
2011-04-28 – 2014-03-31
|
| Keywords | ソフトウェア開発効率化・安定化 / ソフトウェア工学 / アルゴリズム / エージェント / 情報システム |
|---|
| Research Abstract |
高信頼ソフトウェアの開発は，安心・安全な社会を実現する上で必要である．本研究では，分散システムにおけるモデルベースのソフトウェア開発を対象として，抽象的な要求仕様（シナリオ）から，分散システムを構成するモジュールの振る舞いモデル（状態機械図）を自動合成するための理論構築およびアルゴリズム開発を目的とする． 平成23年度では，シナリオから状態機械図を自動合成するために，ペトリネットからUMLの階層型状態機械図への変換方法を開発するための理論的考察を行った．ペトリネットの表現能力と状態機械図の表現能力の差により，任意のペトリネットを状態機械図に変換することは困難であった．そこで，平成23年度では，シナリオの数を単一と制限する事によって，ペトリネットから階層型状態機械図に変換可能であることを示した．また，その成果を電子情報通信学会のシステム数理と応用（MSS）研究会にて成果報告した． また，上記の議論を進めるためにUMLの部分集合であるcbUMLを提案した．cbUMLは，クラス，メッセージ，属性，コミュニケーション図，状態機械図から構成され，議論を進めるのに必要かつ十分なUMLの部分集合である．これにより，平成24年度以降に実施を予定しているアルゴリズムの開発およびその実装がスムーズに行えるようになった．cbUMLの定義および操作的意味をMSS研究会にて成果報告した． さらに，合成によって得られた状態機械図の動作検証を行うために，状態機械図をSMTソルバーを使ってモデル検査する方法，およびペトリネットをモジュラーモデル検査する手法を提案し，MSS研究会および国際会議（IEEE IECON 2011）にて成果報告した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
平成23年度では，シナリオから状態機械図を自動合成するために，ペトリネットからUMLの階層型状態機械図への変換方法を開発するための理論的考察を行った．ペトリネットの表現能力と状態機械図の表現能力の差により，任意のペトリネットを状態機械図に変換することは困難であった．そこで，平成23年度では，シナリオの数を単一と制限する事によって，ペトリネットから階層型状態機械図に変換可能であることを示した． 研究計画では，平成23年度においては「シナリオー状態機械図変換のための理論的考察」を行うことになっており，おおむね研究計画通りに進展している．
|
| Strategy for Future Research Activity |
平成23年度の研究が順調に進んだため，当初計画通りに研究を推進していく． すなわち，平成24年度の前半に「シナリオー状態機械図変換アルゴリズム」を開発し，後半からアルゴリズムの実装に移る．平成25年度にかけて開発したアルゴリズムを定量的に評価する． 研究成果は順次国内外学会において成果報告していく．
|
| Expenditure Plans for the Next FY Research Funding |
購入を予定していたソフトウェアを無償のソフトウェアに切り替えたため，平成23年度の研究費に未使用額が生じたが，平成24年度以降の旅費および論文別刷り費として使用する．
|
