Skip to content

研究テーマ

省電力インテリジェント組込みシステム

本研究室では，知能化 (Intelligent) された組込みシステムの省電力化に関する研究開発を行っています．

組込みシステムは，携帯電話や家電，また自動車，製造ロボットといった機器に組み込まれたコンピュータシステムで，ある特定の用途に特化したシステムとして実現されています． 従来の組込みシステムでは，特定の機器の特定の機能に特化した開発を行うことで，開発コストを抑えつつ高性能なコンピュータシステムを実現することに成功してきました． そして，近年の組込みオペレーティングシステムの進化や組込みボードの処理能力の強化といった組込みシステムの性能向上により，知能化された組込みシステムが実現可能となってきています．

機械学習に基づく AI 技術の進歩により，スマート家電や自動運転技術などといった組込みシステムの応用分野に対しても AI による高性能化が進んでいます． しかしながら，AI を搭載したソフトウェアを組込みシステム上で動作させるとなると，消費される電力量も大きくなり，十分な速度性能を実現するためには高価なハードウェア資源が必要となります． こうした課題の解決を目指して，本研究室ではノーマリーオフ技術と需給エネルギーマッチング技術を導入することで，組込み AI システムの消費電力を軽減するための技術について研究を行っています．

また，組込み AI 技術の応用分野として，小型ドローンに搭載した AI を用いての農作物の生育モニタリングや，車載バイタルモニタに AI を組み込むことでのドライバの病変予測についても研究開発を行っています． さらに，省電力化技術の応用として，再生エネルギーを用いたローカル 5G 基地局の消費電力量削減についても研究を進めています．

進行中のプロジェクト

  • ドライバの生体情報を用いた運転支援
    • T. Kubo, T. Yokogawa, K. Arimoto, M. Hokari and I. Kayano, "Enhancing the Generalization Performance of Drowsiness Estimation AI in Drivers using Time-Series Data from FAU with Limited Datasets," in 14th International Conference on Smart Computing and Artificial Intelligence (SCAI 2023-Winter), Dec. 2023.
  • ドローン搭載超小型 AI を用いた農作物の生育モニタリング
  • ナノ触覚センサと組込み AI 技術の融合による触覚定量化

形式手法を用いたQA/QCプロセスの効率化

本研究室では，ソフトウェアおよびハードウェアの品質保証（Quality Assurance，QA）と品質管理（Quality Control，QC）に形式手法の諸技術を応用するための研究開発を行っています．

QA/QCはソフトウェアやハードウェアの開発において最も多くの工数を要するプロセスであり，QA/QCをいかに効率的に行うかが開発コストに大きく関わってきます． 形式手法 (Formal Method) は，ソフトウェアやハードウェアの仕様記述〜設計〜検証の各開発プロセスに数学や論理学の知見を利用することでその信頼性・頑健性を向上するための様々な技術です． 形式手法は，「形式的仕様記述」と「形式的検証」の2つに大きく分類されており，形式的仕様記述ではソフトウェアやハードウェアの仕様を集合と論理に基づいて数学的に記述することで，仕様の曖昧さを排除することや，仕様間の不整合を検出することが可能です． 一方で，形式的検証は定理証明（Theorem Proving）とモデル検査（Model Checking）の2つにさらに分類され，定理証明では公理と推論規則に従ったプログラムの演繹的証明を，モデル検査では状態遷移グラフとしてモデル化されたシステムの網羅的探索による自動検証を実現しています．

形式手法の導入を支援するためのツールや環境は数多くのものが公開されていますが，それらを実際にQA/QCに用いるためには解決すべき課題が数多く残されています． 例えば，形式的仕様記述を行うためのツールであるBやAlloyにおける集合と論理を用いた仕様記述は，開発現場で慣れ親しんだ自然言語による仕様書の書き方と全く違っていますし，モデル検査ツールのSMVやSALで用いる専用のモデル化言語は，C言語のような手続き型のプログラミング言語とは考え方が大きく異なっています． そのため，現場の技術者がこれらのツールを活用するには教育のための準備期間が必要となります． こうした問題を解決するため，本学では構文解析やテンプレートマッチングを用いて仕様書からの形式仕様の作成を支援する技術や，ビジュアルプログラミングを用いて直感的にモデル作成を行うための技術について研究を行っています．

また，モデル検査は従来のテストでは見つけづらいバグでも網羅的探索によって容易に検出できる利点がありますが，一方で状態遷移グラフの規模が大きくなりやすく，大規模なプログラムの検証には利用しづらいという問題があります． この問題を解決すべく，検証したい性質に合わせてグラフを抽象化して検証を高速化する手法についても研究を行っています．

進行中のプロジェクト