本ページでは研究テーマと様々なプロジェクトの概要を紹介しています．

Trustworthy and Smart Software Engineering

賢く頼れる次世代の新しいソフトウェアのあり方を追求するとともに，その開発・運用・進化のための技術に取り組んでいます．

特に仕様，契約，SLA，法律・規約，ポリシーなどの「約束」をモデル化し，人あるいはソフトウェア自身により開発時・実行時に活用することに興味を持っています．

分野としてはソフトウェア工学，特に形式手法分野，サービス指向コンピューティング分野が中心となりますが，分野・コミュニティに閉じずに幅広い活動を行っています．

プロジェクト目次

• MMSD：インテリジェンス協働形式手法
• REFENG：段階的詳細化による整合性保証と複雑さ軽減の定式化を通した支援
• ClouT: スマートシティーを支えるモノのネットワークとクラウドとの融合
• JSTM：例の生成・提示による仕様とテストの洗練
• PerQAS：サービス合成における機能・品質の保証と適応
• LIMT：法とその解釈のモデル化と分析
• Smartive：サービス指向に基づく協調的移動エージェント
• その他共同研究
• 産業界との活動

MMSD：：インテリジェンス協働形式手法

キーワード：Cyber-Physical Systems，ディペンダビリティ，形式検証，テスティング，機械学習，最適化，確率・統計

物理法則など連続系と，ソフトウェアの離散系の両方を含む複雑なシステムに対し，様々なアプローチの融合により実用的な検証手法を実現する取り組みです．

資金支援：JST 創造科学技術推進事業（ERATO） 「蓮尾メタ数理システムデザインプロジェクト」

REFENG：段階的詳細化における整合性保証と複雑さ軽減の定式化を通した支援

キーワード：ディペンダビリティ，段階的詳細化（リファインメント），形式手法，Event-B，Argument，D-Case

複雑な仕様の効率的な信頼性確保には，概念や要件を徐々に導入する多段階のモデルを構築，検証する段階的詳細化が重要です．しかし，理解や検証の容易性，および様々な整合性を考慮しつつ，適切に導入対象や導入順序を決めることは難しく，現状「職人芸」になっています．これに対し，概念や要件間の依存関係に応じ，どう複雑さが分散されるかといった側面を定式化することにより，段階的詳細化の計画の良し悪しに関する知見，および適切な計画を導く手法を確立します．

資金支援：科学研究費補助金 若手研究（Ａ） 「段階的詳細化における複雑さの分散と整合性の保証に関する研究」

主な発表論文（共著含む）

1. Refactoring Refinement Structures of Event-B Machines (FM 2016)
2. Understanding and Planning Event-B Refinement through Primitive Rationales (ABZ 2014)

ClouT/BigClouT：スマートシティーを支えるモノのネットワークとクラウドとの融合・そしてビッグデータ

キーワード：クラウドコンピューティング，モノのインターネット（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"

JSTM：例の生成・提示による仕様とテストの洗練

キーワード：モデル発見，形式仕様記述，自動テスト生成，受け入れテスト駆動開発

Javaによるインターフェース記述に対し，部分的に与えた仕様記述やテスト方針記述を基に，考えられる例（テストケース）を生成するツールを提供しています．ソルバーによるモデル発見をより手軽に活用できるようにし，例による実感を持って仕様やテスト方針の記述や妥当性確認を進めることができます．

資金支援：IPA ソフトウェア工学分野の先導的研究支援事業 「形式仕様とテスト生成の部分的・段階的な活用～探索を通したコード中心インクリメンタル型開発の支援」

PerQAS：サービス合成における機能・品質の保証と適応

技術キーワード：Webサービス，クラウドコンピューティング，ビジネスプロセス・コレオグラフィ・オーケストレーション（BPMN，WS-BPEL，WS-CDL），Quality of Service（QoS），Service Leval Agreement（SLA），自己適応

サービスを単位とした迅速，柔軟なアプリケーション構築と，その際の機能・品質の実現・保証に取り組んでいます．

資金支援：科学研究費補助金 若手研究（B）「サービス合成において整合性ある契約管理を実現するフレームワークの研究開発」

資金支援：科学研究費補助金 若手スタートアップ 「サービス合成において契約間の整合性を検証，実現するツールに関する研究」

主な発表論文（共著含む）

1. Robust Service Compositions with Functional and Location Diversity (IEEE Trans. on Services Computing, 2016)
2. SanGA: A Self-Adaptive Network-Aware Approach to Service Composition (IEEE Trans. on Services Computing, 2014)
3. Towards Robust Service Compositions in the Context of Functionally Diverse Services (WWW 2012)
4. Towards Network-Aware Service Composition in the Cloud (WWW 2012)
5. Service Selection with Combinational Use of Functionally-Equivalent Services (ICWS 2011)
6. QoS-Aware Automatic Service Composition by Applying Functional Clustering (ICWS 2011)
7. Efficient QoS-Aware Service Composition with a Probabilistic Service Selection Policy (ICSOC 2010)
8. Consistent Integration of Selection and Replacement Methods under Different Expectations in Service Composition and Partner Management Life-Cycle (ICSOC 2010)
9. A Probabilistic Approach to Service Selection with Conditional Contracts and Usage Patterns (ICSOC 2009)

LIMT：法とその解釈のモデル化と分析

キーワード：ゴール指向要求分析，法，法解釈，規約，ガイドライン

組織やシステムが達成すべきゴールの具体化，分析や変更追跡を行う要求工学の考え方を模倣し，法やその解釈のモデル化・分析を行う手法を構築しました．判例などにある既存の法解釈を踏まえ，具体的な要件に関する分析や判断をしたり，新たな判例が現れた際に影響範囲や必要な対応を同定したりすることを支援します．

資金支援：科学研究費補助金 挑戦的萌芽研究 「要求工学の応用による，法とその解釈のモデル化・分析」

主な発表論文（共著含む）

1. Modeling and Analyzing Legal Interpretations for/by Requirements Engineering Approaches (JURISIN 2012)
2. Modeling, Analyzing and Weaving Legal Interpretations in Goal-Oriented Requirements Engineering (RELAW Workshop at RE 2009)

Smartive：サービス指向に基づく協調的移動エージェント

キーワード：マルチエージェントシステム，モバイルエージェント，サービス指向アーキテクチャ，ポリシーベースシステム

複数エージェントが実行時に必要に応じて互いを発見しつつ，交渉と契約を通して協調的にコンテンツ制御や移動を行うためのフレームワークを提供します．

主な発表論文（共著含む）

1. サービス指向コンピューティングにおける合意に基づいた協調的な移動性（情報処理学会論文誌・研究会推薦博士論文速報，2008）
2. Formal Model of Mobile BPEL4WS Process (Int'l Journal of Business Process Integration and Management, 2006)
3. A Framework for Synthesis of Web Services and Mobile Agents, (Int'l Journal of Pervasive Computing and Communications, 2005)

その他共同研究

東大本位田研究室，NII GRACEセンター，連携先の海外大学などと様々な共同研究を行っています．

主なトピック

• 科学研究費補助金 基盤研究（A） 「想定外に備えた空間制御ソフトウェアの分析・設計・検証手法」

主な発表論文（共著含む）

1. The Effects of Developer Dynamics on Fitness in an Evolutionary Ecosystem Model of the App Store (IEEE Trans. on Evolutionary Computation)
2. Investigating Country Differences in Mobile App User Behavior and Challenges for Software Engineering (IEEE Trans. on Software Engineering)
3. On Requirements Representation and Reasoning using Answer Set Programming (AIRE 2014)
4. 自己適応ソフトウェアのための自己適応性設計に関する研究動向（コンピュータソフトウェア サーベイ論文，2014）
5. A Normative Approach to Exploring Multi-Agency Privacy and Transparency
6. Using Web 2.0 for Stakeholder Analysis: StakeSource and its Application in Ten Industrial Projects (Book Chapter in Managing Requirements Knowledge, 2013)

産業界との活動

産業界の開発者に形式手法をはじめとした，上流における工学的アプローチを伝えるとともに，それらの活用による課題解決，それらの活用のための課題解決に取り組んでいます．

主なトピック

• トップエスイー（TopSE）やSQiP研究会などにおける，形式手法などの産業界向け教育，および適用研究
• 共同研究（企業）：Webサイト「ディペンダブル・システムのための形式手法の実践ポータル」の構築
• 形式仕様記述の活用
• その他リポジトリマイニング技術など先端技術の活用

主な発表論文（共著含む）

1. Keys and Roles of Formal Methods Education for Industry: 10 Year Experience from Top SE Program (FMSEET 2015)
2. Practices for Formal Models as Documents: Evolution of VDM Application to "Mobile FeliCa" IC Chip Firmware (FM 2015)
3. What Top-Level Software Engineers Tackles after Learning Formal Methods - Experiences from the Top SE Project (TFM 2009)