| 講座・コース | 情報工学部情報システム工学科 |
 |
| 役職 | 准教授 | |
| 生年月 | 非公開 | |
| 自室番号 | 2504 | |
| t-yokoga**cse.oka-pu.ac.jp ※利用の際は,** を @に置き換えてください. |
||
| 学歴 | 大阪大学基礎工学部情報科学科（1999年3月中退・飛び入学のため） 大阪大学大学院基礎工学研究科情報数理系専攻（修）（2001年3月） 大阪大学大学院基礎工学研究科情報数理系専攻（博）（2004年3月） |
|
| 学位 | 博士（工学），大阪大学，2004年3月 Formal Verification for Dependable Systems by Model Checking (モデル検査手法によるディペンダブルシステムの形式的検証に関する研究) |
|
| 着任年月 | 2004年05月 | |
| 職歴 | 大阪大学 大学院情報科学研究科 研究員（2004年4月） | |
| 専門分野 | ディペンダブルシステム，ソフトウェア工学 | |
| 所属学協会 | IEEE Computer Society，Association for Computing Machinery(ACM)，電子情報通信学会，情報処理学会，日本ソフトウェア科学会 | |
| 現在の研究テーマ | UML設計の形式的検証に関する研究，Webアプリケーションのモデル化に関する研究，有界モデル検査を用いた大規模非同期回路の検証 | |
| 主要担当科目 | ||
| 学部 | 論理回路, ソフトウェア演習Ⅱ, 回路デザイン演習, 計算機アーキテクチャ | |
| 研究概要 | 1つめのテーマとして，ソフトウェアシステムの形式的仕様記法であるUML(統一モデル言語)を対象とした，ドキュメント間の整合性検証について研究を行っている．形式記法であるUMLで記述されたドキュメントは曖昧性をもたないが，仕様が設計者の意図した通りであることを保証するものではない．本研究では，与えられたドキュメント同士がそれぞれ矛盾しないことを自動検証手法の一種であるモデル検査を用いて検証する． 2つめのテーマとして，Webアプリケーションのページ遷移関係のモデル化とその解析手法について研究を行っている．現在のWebアプリケーションでは，1つのハイパーリンクやボタンであっても状況に応じてその動作は異なる．本研究ではこのような動的なページ遷移関係を対象として，UMLの状態マシン図を用いてモデル化と解析を行う． 3つめのテーマとして，大規模な非同期回路を対象とした自動検証に関しての研究を行っている．自動検証を行うためには対象となるシステムを状態遷移グラフとして表す必要があるが，非同期回路は時間的な要素を含むためグラフの規模が非常に大きくなる．そこで本研究では，有界モデル検査と呼ばれる，グラフを段階的に探索する手法を用いることで検証コストの削減を行う． |
|
| 社会における活動 | 電子情報通信学会 和文論文誌D 編集委員 電子情報通信学会 システム数理と応用研究会 専門委員 |
|
| 研究業績 | 【論文誌】 [1] 横川智教, 佐藤洋一郎, 有本和民, “検証およびテスト生成の自動化を指向したステートマシン図による Web ナビゲーションのモデル化,” 電気学会論文誌 C, vol. 136, no. 3, pp. 423–433, 2016. [2] 近藤真史, 横川智教, 佐藤洋一郎, 有本和民, “GALS システムの設計最適化を目的とした性能評価ツール,” コンピュータソフトウェア, vol. 32, no. 4, pp. 115–130, Dec. 2015. 【国際会議】 [1] S. Amasaki, K. Kawata, and T. Yokogawa, “Improving Cross-Project Defect Prediction Methods with Data Simplification,” in Proc. of the 41th Euromicro Conference series on Software Engineering and Advanced Applications (SEAA2015), 2015. [2] K. Arimoto, T. Yokogawa, and Y. Sato, “A Battery Operated Normally-off Computing Technique for Energy Efficient Sensor Node Applications,” in Proc. of the 12th Int’l SoC Design Conf. (ISOCC2015), 2015. [3] K. Kawata, S. Amasaki, and T. Yokogawa, “Improving Relevancy Filter Methods for Cross-Project Defect Prediction,” in Proc. of the 3rd Int’l Conf. on Applied Computing & Inf. Tech. (ACIT2015), 2015. [4] T. Yokogawa, S. Amasaki, N. Igawa, Y. Sato, K. Arimoto, and H. Miyazaki, “Consistency Verification of State Machine Diagrams and Sequence Diagrams Using FDR,” in Proc. of the 41th Euromicro Conference series on Software Engineering and Advanced Applications (SEAA2015), 2015. |
|
| 最終更新日 | 2017.09.28 | |