↓上位設計%&'()*⽣成系研究キーワード⾼信頼ソフトウェア ・ 設計検証技術 ・ 並列分散システム ・ モデル検査 ・ 形式⼿法94最近の研究トピックス↑OcamlベースHWコンパイラ系HiPSツール:階層型ペトリネットを設計・解析・シミュレーショ ン実⾏する統合環境 並列分散システムのモデル化http://sourceforge.net/projects/hips-tools/ SPINモデル検査ツール統合環境iSPINによる検証とランダムウォーク・シミュレーショ ン実⾏の様⼦（通信プロトコル設計の検証中）私の学問へのきっかけ⾼校⽣の時、 世間ではパソコンが発売され始めていて、⼀⽇中プログラミングができる仕事に就きたいと考え、情報⼯学分野への進学を決めました。 私が学問の道を志すきっかけとなったのは、 所属研究室の指導教授から、情報システムと数学との深い繋がり、 そして研究活動の成果は特定の製品に留まらず、 幅広い応⽤に活かされることを学んだからです。 ⼤学で学んだ知識や経験は、今の研究の全てに繋がっています。 学問の煌きを、皆さんも⼤学で体験して下さい。教授 和﨑 克⼰⻑ 野 ⾼ 専 助 ⼿、 信 州 ⼤ 学⼯ 学 部 情 報 ⼯ 学 科 助 ⼿ 、助 教 授、 ⼤ 学 院 ⼯ 学 系 研究 科 准 教 授 を 経 て、 2009年 よ り 現 職 。 研 究 分 野 は、並 列 分 散 シ ス テ ム の モ デル 化 と 解 析、 ⾮ 同 期 回 路の 数 学 モ デ ル と 形 式 検 証 、モデル検査系、など。ソフトウェアは⽬に⾒えず重さも無く、「情報（ ビット）」という形で格納される、 不思議な⼯業製品です。ソフトウェアの設計を検証することで、正しく動く信頼性の⾼い製品やサービスを提供することができます。⾼い信頼性を持つ情報システムの設計・開発や組み込みシステムに活かされます。通信ネットワーク、 ソフトウェア開発、システム設計エンジニア、クラウドサービス企業などに卒業⽣を輩出。⾃律的な論理的思考ができる技術者・ 研究者の育成のため、 ⽇頃から研究の議論・ ゼミ活動を中⼼とした指導を⾏っています。研究の成果は国内外の学会や論⽂で発表しています。情報システムの「信頼性」に関して、ネットワークQoS・暗号化通信に代表される「安全性(Safety)」とともに、 システムの堅牢性(Reliability) を確保することが⼤変重要です。⾼い信頼性が要求される情報システムのため、可能な限り誤り（バグ）を排除した設計に仕上げていくことが重要な課題です。 和﨑研究室では、「100%バグフリー設計」 を⽬指し、ソフトウェア分野で( 1)特に並列システムを対象とした、設計の全網羅的な検査システムと検証ツールの開発と(2)上流⼯程からの⼀貫設計検証環境、などを研究しています。研究シーズn ペトリネット援⽤ツール HiPS（各種解析器、モデル検査器、ライブラリ）n ⾼⽔準ペトリネット援⽤ツール HiPS2（各種解析器、制御システムモデル）n UMLステートマシン図＋構成図からSPINモデル検査器コードの⾃動⽣成系n UMLアクティビティ図からJava Servletコード⾃動⽣成系、⾼速プロトタイピングn VDM++仕様記述とインタープリタ実⾏系、VDMJWeb分散モデル実⾏サービスn 上位ハードウェアコンパイラ Melasy+ : HDLコード⾃動⽣成系共同研究・外部資⾦獲得実績l ⼤規模⾼速な形式検証を実現するメタスケーラブル定理証明器と並列モデル検査器の融合（科研費代表）l グリッド環境の定理証明器とモデル検査器をハードウェアコンパイラ融合した形式検証系（科研費代表）l 関数型⾔語系とグリッド環境上のプルーフチェッカを融合した超並列演算器の設計検証法（科研費代表）l 信州⼤学インターネット⼤学院におけるマルチメディア利⽤CAIシステムの⾼度化研究（科研費分担）l 複合センサを⽤いた地域型独居⾼齢者⽣活サポ－トシステムの研究開発（総務省SCOPE分担）★★設設計計をを検検証証すするるっってて、、ととっっててもも重重要要★★「「110000％％ババググフフリリーー設設計計」」をを⽬⽬指指ししてて!!!!研究から広がる未来卒業後の未来像
元のページ ../index.html#95