工学部 研究紹介2018

59/148

研究から広がる未来卒業後の未来像岡野研究室岡野研究室では小形研究室と協力しソフトウェア開発をサポートする諸技術の研究を行っています。ソフトウェアは要求文書に始まり、どのように作るかという設計文書、そしてプログラムコード、テストスイート、表明などからなっています。またこれらの文章は相互に関連付けられています。これの生産物に対して定量測定や、あるいは静的解析を行って、種々の性質を検証したり、工数などを予測することがソフトウェア工学として重要です。これらの技術について研究を行っています。ソフトウェア開発には多くの工学技術が使われています。その中でも我々の研究は高信頼ソフトウェア開発のための技術を研究しています。今後、ソフトウェアの大規模化、社会における重要性の高まりにより、このような技術を持ったソフトウェア技術者の活躍が重要になってくると思われます。半数以上の学生が大学院に進学します。その後は、研究を通して得た技術、経験をもとにソフトウェア開発や組み込みシステムの開発や研究に企業等で活躍することが期待されます。岡野浩三准教授大阪大学大学院基礎工学研究科修了。博士（工学）。2015年より現職。ソフトウェア工学、とりわけ仕様記述と検証技術に関する研究に従事。よりよいソフトウェア作りの研究：「設計書」と「コード」の関係ライントレーシングロボットの安全性検証Spec.(JML)Spec. (Alloy)Alloy Analyzer!?instances仕様の洗練度をAlloy Analyzerを用いて可視化電⼦情報システム⼯学科研究シーズ共同研究・外部資⾦獲得実績社会貢献実績研究キーワードソフトウェア・設計検証・⾼信頼性・障害診断・仕様記述【先生の学問へのきっかけ】ソフトウェア工学の研究者になった理由の1つは、逆説的ですが、ソフトウェア作成が苦手であったことです。自分のような、あわてんぼ（書き間違えが多い）で、理解しているはずのアルゴリズムを実装するときに誤りをいれてしまう（論理的バグの混入）人間でも高信頼ソフトウェアを開発できる方法が「コンピュータを活用することにより」きっとあるはずだという考えで取り組んでいます。子供のころは電子工作に興味を持っていました。その発展として、コンピュータに興味を持ち、当時としてはまだまだ珍しかった「情報工学科」に入学し、今の自分があります。コンピュータについて学んでいく（研究していく）過程で離散数学の素晴らしさや、抽象化・具体化の考え方などに触れる機会を得たと思います。•モデル検査を用いたシステム設計検証•システムの時間的性質のモデル検証•ソフトウェア仕様記述と検証・開発方法•モデルと制約に基づくソフトウェア開発に関する研究2015年度～2018年度基盤研究(C)•三菱電機との共同研究2015年度•モデル検査技術を活用したソフトウェア設計方法に関する研究2009年度～2013年度基盤研究(C)•状態爆発するWEBアプリケーションに対するソフトウェアモデル検査2006年度特定領域研究情報爆発IT基盤•通産省平成11年度IPAソフトウェアシーズ育成整数プレスブルガー文真偽判定ライブラリの作成電子情報通信学会和文論文誌D編集委員会委員情報処理学会論文誌ジャーナル/JIP論文誌編集委員会委員ＩPA製品・制御システム高信頼化部会障害原因診断WG委員CEGARを用いた高速モデル検査時間オートマトンを用いた時間性質のモデル検査57