お問い合わせ 交通・キャンパス案内 信州大学HOME
信州大学工学部 電子情報システム工学科

和﨑 克己

★設計を検証するって、とっても重要★ 「100%バグフリー設計」を目指して!!

HiPSツール:階層型ペトリネットを設計・解析・シミュレーション実行する統合環境 http://sourceforge.net/projects/hips-tools/

HiPSツール:階層型ペトリネットを設計・解析・シミュレーション実行する統合環境 http://sourceforge.net/projects/hips-tools/

SPINモデル検査ツール統合環境iSPINによる検証とランダムウォーク・シミュレーション実行の様子(通信プロトコル設計の検証中)

SPINモデル検査ツール統合環境iSPINによる検証とランダムウォーク・シミュレーション実行の様子(通信プロトコル設計の検証中)

情報システムの「信頼性(Dependability)」に関して、ネットワークのQoS・暗号化通信に代表される「安全性(Safety)」とともに、システムの堅牢性(Reliability)を確保することが大変重要です。高い信頼性が要求される情報システムのために、可能な限り誤り(バグ)を排除した設計に仕上げていくことが重要な課題です。和﨑研究室では、「100%バグフリー設計」を目指し、ソフトウェア分野で(1)特に並列システムを対象とした、設計の全網羅的な検査システムと検証ツールの開発と(2)上流工程からの一貫設計検証環境、などを研究しています。

研究から広がる未来

ソフトウェアは目に見えず重さも無く、「情報(ビット)」という形で格納される、不思議な工業製品です。ソフトウェアの設計を検証することで、正しく動く信頼性の高い製品やサービスを提供することができます。和﨑研究室では、並列システムモデルそのモデル化手法(ネット指向設計、プロセス代数仕様設計等)ならびにその形式検証系(定理証明系、モデル検査系)を基盤理論として、ソフトウェアの上流設計や、上位ハードウェアコンパイラ、ペトリネット設計・検証ツールといった応用に取り組んでいます。

卒業後の未来像

通信ネットワーク、ソフトウェア開発、システム設計エンジニア、クラウドサービス企業などに卒業生を輩出。自律的な論理的思考ができる技術者・研究者の育成のため、日頃から研究の議論・ゼミ活動を中心とした指導を行っています。研究の成果は国内外の学会や論文で発表しています。

プロフィール

長野高専助手、信州大学工学部情報工学科助手、助教授、大学院工学系研究科准教授を経て、2009年より現職。研究分野は、並列分散システムのモデル化と解析、非同期回路の数学モデルと形式検証、モデル検査系、など。

電子メールアドレス
研究者総覧(SOAR) 詳細を見る
個人サイト http://www.researchgate.net/profile/Katsumi_Wasaki
オフィスアワー 部屋:5F 506室

原則として授業期間内の、水曜日と木曜日の、16:30から18:00をオフィスアワーとします。但し、不在の場合もありますのでメールで確認してください。