本ページでは研究テーマと様々なプロジェクトの概要(企業共同研究も含む)を紹介しています.
「スマートなシステム・スマートなディペンダビリティ保証」をキャッチフレーズとして,ソフトウェア工学分野および自律・スマートシステム分野において幅広い活動を行っています.
先端応用システムも見据え,要求や仕様、設計に関する様々なモデルを活用した検証・推論・最適化・自動テスト生成・自己適応などの技術に取り組んでいます.
現在は特に,形式手法や自動テスト生成の技術を発展させ,サイバーフィジカルシステムや機械学習システムにおけるディペンダビリティ向上・保証を行う技術に焦点をおいて取り組んでいます.
複数組織にまたがる研究グループを形成し,海外機関との連携や,企業との連携も盛んに行っています.
要求や仕様、設計に関する様々なモデルを活用した検証・推論・最適化・自動テスト生成・自己適応などの技術に取り組んでいます。
キーワード:形式手法(形式仕様記述,リファインメント),テスティング(サーチベースドテスティング,モデルベースドテスティング),ゴール指向要求分析,自己適応(Models@run.time),機械学習工学
Webおよび実世界において,柔軟・迅速に機能や情報を実現するための先端システムパラダイムに関する取り組みも盛んに行っています.
キーワード:サービス指向コンピューティング・クラウドコンピューティング(サービス合成,資源最適化),マルチエージェントシステム,IoT: Internet of Things(サービス合成,自己適応),CPS: Cyber-Physical Systems(自動車システム)
このページはあまり高い頻度では更新されていません.
キーワード:機械学習工学,深層ニューラルネットワーク,自動テスト生成,不具合分析,自動デバッグ,自動運転
深層ニューラルネットワークなど複雑な機械学習モデルに対し,自動テスト生成や自動デバッグなどソフトウェア工学の技術を適合させることで,高い安全性・信頼性を示す技術に取り組みます.
資金支援:JST 未来社会創造事業 「機械学習を用いたシステムの高品質化・実用化を加速する"Engineerable AI"技術の開発」
キーワード:Cyber-Physical Systems,ディペンダビリティ,自動テスト生成,不具合分析,自動デバッグ,形式手法,自動運転
物理法則など連続系と,ソフトウェアの離散系の両方を含む複雑なシステムに対し,自動テスト生成や形式手法など様々なアプローチの融合により実用的な検証手法を実現する取り組みです.
資金支援:JST 創造科学技術推進事業(ERATO) 「蓮尾メタ数理システムデザインプロジェクト」
キーワード:ディペンダビリティ,段階的詳細化(リファインメント),形式手法,Event-B,Argument,D-Case
複雑な仕様の効率的な信頼性確保には,概念や要件を徐々に導入する多段階のモデルを構築,検証する段階的詳細化が重要です.しかし,理解や検証の容易性,および様々な整合性を考慮しつつ,適切に導入対象や導入順序を決めることは難しく,現状「職人芸」になっています.これに対し,概念や要件間の依存関係に応じ,どう複雑さが分散されるかといった側面を定式化することにより,段階的詳細化の計画の良し悪しに関する知見,および適切な計画を導く手法を確立します.
資金支援:科学研究費補助金 若手研究(A) 「段階的詳細化における複雑さの分散と整合性の保証に関する研究」
主な発表論文(共著含む)
キーワード:クラウドコンピューティング,モノのインターネット(IoT: Internet of Things),スマートシティー,ディペンダビリティ
モノのネットワークと人のネットワークを,サービスのネットワークを通してつなぐことにより,スマートシティーの実現基盤を構築し,実証する日欧9機関,4都市による取り組みです.
資金支援:Horizon2020/NICT 欧州との連携による公共ビッグデータの利活用基盤に関する研究開発 "BigClouT: Big data meeting Cloud and IoT for empowering the citizen clout in smart cities"
資金支援:FP7/NICT 新世代ネットワークの実現に向けた欧州との連携による共同研究開発 "ClouT: Cloud of Things for empowering the citizen clout in smart cities"
キーワード:モデル発見,形式仕様記述,自動テスト生成,受け入れテスト駆動開発
Javaによるインターフェース記述に対し,部分的に与えた仕様記述やテスト方針記述を基に,考えられる例(テストケース)を生成するツールを提供しています.ソルバーによるモデル発見をより手軽に活用できるようにし,例による実感を持って仕様やテスト方針の記述や妥当性確認を進めることができます.
資金支援:IPA ソフトウェア工学分野の先導的研究支援事業 「形式仕様とテスト生成の部分的・段階的な活用~探索を通したコード中心インクリメンタル型開発の支援」
技術キーワード:Webサービス,クラウドコンピューティング,ビジネスプロセス・コレオグラフィ・オーケストレーション(BPMN,WS-BPEL,WS-CDL),Quality of Service(QoS),Service Leval Agreement(SLA),自己適応
サービスを単位とした迅速,柔軟なアプリケーション構築と,その際の機能・品質の実現・保証に取り組んでいます.
資金支援:科学研究費補助金 若手研究(B)「サービス合成において整合性ある契約管理を実現するフレームワークの研究開発」
資金支援:科学研究費補助金 若手スタートアップ 「サービス合成において契約間の整合性を検証,実現するツールに関する研究」
主な発表論文(共著含む)
キーワード:ゴール指向要求分析,法,法解釈,規約,ガイドライン
組織やシステムが達成すべきゴールの具体化,分析や変更追跡を行う要求工学の考え方を模倣し,法やその解釈のモデル化・分析を行う手法を構築しました.判例などにある既存の法解釈を踏まえ,具体的な要件に関する分析や判断をしたり,新たな判例が現れた際に影響範囲や必要な対応を同定したりすることを支援します.
資金支援:科学研究費補助金 挑戦的萌芽研究 「要求工学の応用による,法とその解釈のモデル化・分析」
主な発表論文(共著含む)
キーワード:マルチエージェントシステム,モバイルエージェント,サービス指向アーキテクチャ,ポリシーベースシステム
複数エージェントが実行時に必要に応じて互いを発見しつつ,交渉と契約を通して協調的にコンテンツ制御や移動を行うためのフレームワークを提供します.
主な発表論文(共著含む)
東大本位田研究室,NII GRACEセンター,連携先の海外大学などと様々な共同研究を行っています.
主なトピック
主な発表論文(共著含む)
産業界の開発者に形式手法をはじめとした,上流における工学的アプローチを伝えるとともに,それらの活用による課題解決,それらの活用のための課題解決に取り組んでいます.
主なトピック
主な発表論文(共著含む)