工学部 研究紹介2018

57/148

和﨑研究室研究から広がる未来卒業後の未来像情報システムの「信頼性(Dependability)」に関して、ネットワークのQoS・暗号化通信に代表される「安全性(Safety)」とともに、システムの堅牢性(Reliability)を確保することが大変重要です。高い信頼性が要求される情報システムのために、可能な限り誤り（バグ）を排除した設計に仕上げていくことが重要な課題です。和﨑研究室では、「100%バグフリー設計」を目指し、ソフトウェア分野で(1)特に並列システムを対象とした、設計の全網羅的な検査システムと検証ツールの開発と(2)上流工程からの一貫設計検証環境、などを研究しています。ソフトウェアは目に見えず重さも無く、「情報（ビット）」という形で格納される、不思議な工業製品です。ソフトウェアの設計を検証することで、正しく動く信頼性の高い製品やサービスを提供することができます。和﨑研究室では、並列システムモデルそのモデル化手法（ネット指向設計、プロセス代数仕様設計等）ならびにその形式検証系（定理証明系、モデル検査系）を基盤理論として、ソフトウェアの上流設計や、上位ハードウェアコンパイラ、ペトリネット設計・検証ツールといった応用に取り組んでいます。通信ネットワーク、ソフトウェア開発、システム設計エンジニア、クラウドサービス企業などに卒業生を輩出。自律的な論理的思考ができる技術者・研究者の育成のため、日頃から研究の議論・ゼミ活動を中心とした指導を行っています。研究の成果は国内外の学会や論文で発表しています。和﨑克己教授長野高専助手、信州大学工学部情報工学科助手、助教授、大学院工学系研究科准教授を経て、2009年より現職。研究分野は、並列分散システムのモデル化と解析、非同期回路の数学モデルと形式検証、モデル検査系、など。電⼦情報システム⼯学科研究シーズ共同研究・外部資⾦獲得実績社会貢献実績研究キーワード⾼信頼ソフトウェア・設計検証技術・並列分散システム・モデル検査・形式⼿法【先生の学問へのきっかけ】子供の頃から、機械いじりや電子工作が大好きでした。高校生の時、世間ではパソコンが発売され始めていて、一日中コンピュータを使っていられる仕事に就きたいと考え、情報工学分野への進学を決めました。私が学問の道を志すきっかけとなったのは、所属研究室の指導教授から、情報システムと数学との深い繋がり、そして研究活動の成果は特定の製品に留まらず、幅広い応用に活かされることを学んだからです。学部・大学院で学んだ知識や経験は、私の「システム検証」研究の全ての基盤となっています。学問の煌きを、皆さんも大学で体験して下さい。•ペトリネット援用ツールHiPS（各種解析器、モデル検査器、ライブラリ）•高水準ペトリネット援用ツールHiPS2（各種解析器、制御システムモデル）•UMLステートマシン図＋構成図からSPINモデル検査器コードの自動生成系•UMLアクティビティ図からJava Servletコード自動生成系、高速プロトタイピング•VDM++仕様記述とインタープリタ実行系、VDMJWeb分散モデル実行サービス•上位ハードウェアコンパイラMelasy+ : HDLコード自動生成系•グリッド環境の定理証明器とモデル検査器をハードウェアコンパイラ融合した形式検証系（科研費代表）•MIZAR数学ライブラリの構築と大学数学向け高度遠隔教育用コンテンツ開発（科研費分担）•関数型言語系とグリッド環境上のプルーフチェッカを融合した超並列演算器の設計検証法（科研費代表）•信州大学インターネット大学院におけるマルチメディア利用CAIシステムの高度化研究（科研費分担）•複合センサを用いた地域型独居高齢者生活サポ－トシステムの研究開発（総務省SCOPE分担）•GHz帯長距離漏洩同軸ケーブルを用いた高速防災無線情報システムの研究開発（総務省消防庁分担）長野市個人情報保護審査会審査委員（2014〜）独立行政法人新エネルギー・産業技術総合開発機構（NEDO）研究評価委員（2008）長野県組込システムコンソーシアム運営委員・研究会員（2003〜2007）電子情報通信学会会誌編集委員WG・A（2013〜2015）電子情報通信学会信越支部委員・学生会顧問（2011〜2013）★設計を検証するって、とっても重要★「100％バグフリー設計」を⽬指して!!HiPSツール:階層型ペトリネットを設計・解析・シミュレーション実行する統合環境http://sourceforge.net/projects/hips-tools/SPINモデル検査ツール統合環境iSPINによる検証とランダムウォーク・シミュレーション実行の様子（通信プロトコル設計の検証中）55