| 題名 | SMVを用いたUML設計間の整合性違反の自動修正 |
| 著者 | *原田 慎士, 横川 智教 (岡山県立大学大学院情報系工学研究科), 宮崎 仁 (川崎医療福祉大学医療技術学部), 佐藤 洋一郎, 早瀬 道芳 (岡山県立大学大学院情報系工学研究科) |
| Page | p. 378 |
| Keyword | モデル検査, UML, 整合性検証 |
| Abstract | UMLを用いたソフトウェア開発においては，個々の設計には誤りがなくても，それらを組み合わせた際に矛盾や不具合が生じる恐れがある．これまでに我々は，UMLの状態マシン図とシーケンス図を対象に，記号モデル検査ツールSMVを用いて設計間の整合性を検証する手法について開発を行ってきた．本稿では，SMVにより得られた反例を元に設計上の違反箇所を特定し，設計の自動修正を行う手法を提案する．まず，反例として得られた遷移系列を解析し，状態マシン図とシーケンス図で動作が一致しない箇所を特定する．その上で，特定された箇所を互いの動作が一致するよう修正する． |
| 題名 | Alloyを用いたUML設計間の整合性違反の検出および反例生成 |
| 著者 | *仁宮 章恵, 横川 智教 (岡山県立大学大学院情報系工学研究科), 宮崎 仁 (川崎医療福祉大学医療技術学部), 佐藤 洋一郎, 早瀬 道芳 (岡山県立大学大学院情報系工学研究科) |
| Page | p. 379 |
| Keyword | モデル検査, UML, Alloy |
| Abstract | 本稿では，仕様検査ツールAlloyを用いて状態マシン図とコミュニケーション図の整合性を検証し，違反検出時には反例を生成する手法を提案する．本手法では，状態マシン図およびコミュニケーション図の動作を遷移システムとして定義し，Alloy上のモデルとして表現する．また，整合性はモデルの制約として，同様にAlloy上で表現する．これらの条件を満たすモデルをAlloyにより求めることで整合性の検証を実現する．また，条件を満たさないモデルとして反例を得ることが可能である．最後に本手法を例題システムに適用し，整合性違反を正しく検出し，反例が生成されていることを確認した． |
| 題名 | 記号モデル検査ツールSMVを用いた結合フラグメントの形式的検証 |
| 著者 | *川上 由香, 横川 智教 (岡山県立大学大学院情報系工学研究科), 宮崎 仁 (川崎医療福祉大学医療技術学部), 佐藤 洋一郎, 早瀬 道芳 (岡山県立大学大学院情報系工学研究科) |
| Page | p. 380 |
| Keyword | UML, モデル検査, SMV, シーケンス図 |
| Abstract | 結合フラグメントは，シーケンス図で複雑な相互作用を記述するために，UML2.0で新たに導入された記法の1つである．これまでに我々は，記号モデル検査ツールSMVを用いてUMLの状態マシン図とシーケンス図の整合性を検証する手法を開発してきた．この手法では，状態マシン図およびシーケンス図の動作を遷移システムとしてモデル化し，論理式表現することでSMVによる検証を実現している．本稿では，結合フラグメントで記述された動作を同様の枠組みで表現することにより，結合フラグメントを含んだシーケンス図を扱えるよう手法の拡張を行う． |
| 題名 | UPPAALを用いたGALSシステムの形式的検証手法の改良 |
| 著者 | *桐田 和明, 横川 智教 (岡山県立大学 大学院情報系工学研究科), 宮崎 仁 (川崎医療福祉大学 医療技術学部), 佐藤 洋一郎, 早瀬 道芳 (岡山県立大学 大学院情報系工学研究科) |
| Page | p. 381 |
| Keyword | GALSシステム, モデル検査, UPPAAL, STPN, 時間オートマトン |
| Abstract | GALSシステムを設計する上では，設計されたシステムが意図した通りに動作することを保証しなければならない．GALSシステムは実時間システムであるため，その検証には連続時間に基づくモデル化と解析が求められる．これまでに，GALSシステムをSTPNを用いてモデル化し，そのモデルを等価な時間オートマトンへと変換することで，連続時間モデル検査ツールUPPAALを用いた検証を行う手法を開発してきた．現在の変換法では得られた時間オートマトンのサイズが大きく，検証に時間がかかるという問題があるため，変換法を改良することで得られるオートマトンのサイズを縮小する． |
| 題名 | ファイル間関連度を用いたタスク間の共通ファイル発見手法 |
| 著者 | *定免 睦昌, 國島 丈生, 横田 一正 (岡山県立大学大学院情報系工学研究科) |
| Page | pp. 382 - 383 |
| Keyword | ファイル間関連度, クラスタリング, ファイル管理 |
| Abstract | PCでユーザが扱うファイル数は極めて増加しており，フォルダによる分類やデスクトップ検索により高度なデスクトップ関連ファイルの提示機能が求められている． このような動機の下に行われている研究に，デスクトップ操作の履歴からファイル間の関連度を抽出するものがあるが，従来の研究では，ユーザが複数のタスク（作業）を同時並行して行うという状況を想定していなかった． 我々は，複数のタスクが同時並行して行われるという状況を考慮して，ユーザのデスクトップ操作からファイル間の関連度を算出する方法を提案し，階層的クラスタリングによって関連の深いファイル集合としてユーザのタスクを抽出する方法を提案した． 本稿では，複数タスク間で共通して使用されるファイル（を発見する手法について考察する． |
| 題名 | 福山市内道路網におけるリンク旅行時間の解析と推定 |
| 著者 | *森藤 義之 (福山大学大学院/工学研究科), 清水 光 (福山大学/工学部) |
| Page | pp. 384 - 385 |
| Keyword | 動的経路誘導システム, 交通流ダイナミクス, リンク旅行時間 |
| Abstract | 近年，交通量の増加と共に都市地域の幹線道路を中心に交通渋滞や交通事故が日常的に発生している．交通渋滞は，旅行時間や燃料消費，二酸化炭素排出量の増加などの一要因になっている．交通流の円滑化と安全化を図り，交通渋滞を解消，または軽減する対策の一つに動的経路誘導システムがある．動的経路誘導システムでは，運転者に出発地から目的地までの複数の推奨経路を示し，運転者は最も適当と思われる経路を選択して走行する． 本稿では，まず，動的経路誘導システムで基礎的役割を果たす交通流ダイナミクスやリンク旅行時間について解析する．つぎに，広島県福山市内道路網の二つの経路におけるリンク旅行時間について推定する． |