九州工業大学
情報工学部 知能情報工学科
知能情報工学特別講義
（鵜林研究室の紹介）
知能情報アーキテクチャ講座
鵜林 尚靖
1
内容
研究室の概要
研究紹介
配属希望の皆さんへ
2
１．研究室の概要
ＰＯＳＬ
（Principles of Software Languages）
3
研究分野
言語の視点に立ったソフトウェア構成原理
に関する研究
ＰＯＳＬ（Principles of Software Languages）
プログラミング言語
モデリング言語
形式仕様記述言語
ドメイン特化言語
先進的なプログラミング言語機構に関する研究（特
にアスペクト指向プログラミング）
モデル駆動型開発手法に関する研究
形式手法に関する研究
4
研究室の公開ホームページ
http://posl.minnie.ai.kyutech.ac.jp/
5
共同研究マップ
生産性と安全性向上のためのアスペクト指向ソフトウェア
開発に関する研究
大学
東京大学
玉井研究室
東大、東工大、ＮＩＩ、京大
企業
九州工業大学
鵜林研究室
電機メーカ
カーエレメーカ
国立研究機関
国立情報学研究所（ＮＩＩ）
アーキテクチャ科学系
組込みソフトウェアの分析、
設計法に関する研究
自主研究
形式手法を用いたソフトウェア・プロダク
トラインの研究
科研基盤研究（Ｃ）
検証可能なモデルコンパイラに関する研究
6
最近の主な研究
目標は世界レベルの研究！
(ACM, IEEE で論文発表)
Tetsuo Tamai, Naoyasu Ubayashi, and Ryoichi Ichiyama:
An Adaptive Object Model with Dynamic Role Binding,
27th IEEE/ACM International Conference on Software Engineering (ICSE 2005)
[acceptance rate: 44 of 313 (14%)]
Naoyasu Ubayashi, Genki Moriyama, Hidehiko Masuhara, and Tetsuo Tamai:
A Parameterized Interpreter for Modeling Different AOP Mechanisms,
20th IEEE/ACM International Conference on Automated Software Engineering (ASE 2005)
[acceptance rate: 28 of 291 (10%)]
Naoyasu Ubayashi, Akihiro Sakai, and Tetsuo Tamai:
An Aspect-oriented Weaving Mechanism Based on Component and Connector Architecture ,
22nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2007)
[acceptance rate: 37 of 312 (12%)]
7
研究室メンバ（２００８年度）
Ｄ２ １名
Ｍ２ ２名
Ｍ１ １名
Ｂ４ ５名
グループ構成
① Webモデリンググループ
（Ｄ２：１名，Ｂ４：３名）
② Aspectモデリンググループ
（Ｍ２：２名）
③ Concernモデリンググループ （Ｍ１：１名，Ｂ４：２名）
8
ゼミの進め方
勉強会（週１回）:
専門書の輪読を行う
２００８年度（参考）
ＳＰＩＮモデル検査 (中島 震）
研究進捗報告会（週１回×３グループ）：
学生が持ち回りで、自分の研究内容の紹介、進捗報告を行う
研究に関連する（英語の）論文の紹介
実質的な研究指導の場
プレゼン能力習得の場
9
卒研の進め方
研究活動の一環としてプログラムを開発する（新しい
言語やツールなど）
基礎理論を構築する
最終的な研究成果は、学会で発表する（全国大会や
研究会などで）
10
２．研究紹介
11
研究マップ
表現
形式手法（組込みソフトウェア開発への応用）
外部環境分析、プロダクトライン
モデル駆動型開発
AspectM: UMLベースAOモデリング言語
AspectVDM： VDMベースAOモデリング言語
アスペクト指向プログラミング
X-ASB: AOメカニズムのモデル化
ｃｃＪａｖａ： ＡＯインタフェースの導入
AOWP: Webアプリケーション向けＡＯＰ
検証
形式仕様記述言語
Lightweight Formal Methodsの適用
モデリング言語
AspectM: モデルコンパイラの検証
AspectVDM： 証明課題
プログラミング言語
COW: 契約による織り込み検証
契約によるリファクタリング検証
ｃｃＪａｖａ： 型システム
12
アスペクト指向プログラミング
現在、アスペクト指向はプログラミング研究においてホットな
話題の一つ
当研究室では、アスペクト指向計算モデル、アスペクト指向
プログラムの論理検証、クラスベースのアスペクト指向言語
等の研究開発に取り組んでいる
プログラミング言語機構に関するアイデアをツールとして実
現するだけでなく、そのための基礎理論を構築することも重
要な研究の一つ
13
アスペクト指向の概要
AspectJ
横断的関心事のモジュール化
（ロギングなど）
AOPはAspectJだけ？
⇒ X-ASB
AOPの織り込みで不具合は発生しない？
⇒ COW or WbC
AOPにはインタフェース概念は無いのか？
⇒ ccJava 織り込みインタフェース
Display updating
pointcut
after (FigureElement fe):
(call(void set*(..)) && target(fe) {
fe.display.update(fe); }
advice
14
ccJava
(Class-based Crosscutting Language for Java)
Component & Connector Architecture
public w_interface wPoint {
pointcut change():
execution(void setX(int)) ||
execution(void setY(int)) ||
execution(void moveBy(int, int));
import before(), after() returning, around() : change();
}
インタフェース
public w_interface wLine {
pointcut change():
execution(void setP1(Point)) ||
execution(void setP2(Point)) ||
execution(void moveBy(int, int));
import before(), after() returning, around() : change();
}
public w_interface wDisplay {
pointcut redraw(): execution(void update());
import before(), after() returning : redraw();
export redraw();
}
言語レベルで
reasoning が可能
weave {
class Point implements wPoint;
class Line implements wLine;
class Display implements wDisplay;
connect(port1:wDisplay.redraw, port2:{wPoint || wLine}.change){
after() returning : port2 { port1.proceed(); }
}
}
15
モデル駆動型開発
産業界では、ＵＭＬを用いたモデルベースのソフトウェア開発
が主流
当研究室では、拡張可能なアスペクト指向モデリング言語に
関する研究を行っている
拡張可能なモデルエディタ、コンパイラを開発
16
AspectM －拡張可能な
アスペクト指向モデリング言語
AspectM metamodel
protocols
reify
meta level
(MOF L2)
extension
point
MMAP
Edit-time
reflection
base level
(MOF L1)
AspectM model
reflect
new model
element
モデルエディタ
17
Invoke the Meta Editor
Overview of Reflective Model Editor
Demonstration
Base Editor
Meta Editor
Extension Procedure
1.
2.
3.
4.
Execute extension operations
Assign a graphic notation to
a new model element
Regenerate the metamodel
Restart the base editor
Base Editor
19
Show an extension point
Rebuild the Base Editor
Create a new metaclass
Execute extension operations
(add attribute, association, …)
Assign a graphic notation
Add a constraint using OCL
A class can have at most one UniqueId.
self.owner.feature
->select(oclIsTypeOf(UniqueId))->size() <= 1
Meta Editor
20
This violates the constraint
A class can have at most one UniqueId.
self.owner.feature
->select(oclIsTypeOf(UniqueId))->size() <= 1
Base Editor can detectNew
this
error
model
elements are added to the pallet
Base Editor
21
形式手法に関する研究
形式手法(Formal Methods)とは、ソフトウェアの仕様記述や
設計を数学的な考え方に基づいて行うための手法
ソフトウェアの品質や信頼性向上の手段として最も注目され
ている技術の一つ（特に組込みソフトウェアの分野で注目さ
れている）
当研究室では、形式手法を組込みソフトウェア開発、ソフト
ウェアプロダクトライン（ＳＰＬ）に適用する研究を行っている
22
形式手法のタイプ
モデル規範型（ＶＤＭ、Ｚ、Ｂ等）
性質規範型（代数仕様）
モデル検査（ＳＰＩＮ、ＳＭＶ、ＵＰＰＡＡＬ、ＬＴＳＡ等）
通信プロセスモデル（ＣＳＰ、ＣＣＳ等）
論理学（命題論理、一階述語論理、時相論理など）の
知識が必要
23
時相論理による仕様記述の例
安全性の記述
安全性とはシステムが正常な動作を継続することを
表すもので、「良い性質が常に満たされること」を
求める
Ｓ → □Ｓ’
デッドロックの回避は？
Ｐ∧Ｑ ＰかつＱ
Ｐ∨Ｑ ＰまたはＱ
Ｐ→Ｑ
ＰならばＱ
￢Ｐ Ｐでない
□Ｐ これからずっとＰが成り立つ
◇Ｐ これからいずれＰが成り立つ
○Ｐ 次にＰが成り立つ
24
Pettersonの排他制御アルゴリズムの例
UPPAAL
プロセス Ｐ１
req1=1;
turn=2;
while(turn!=1 && req2!=0);
//critical section
job1();
req1=0;
プロセス Ｐ２
req2=1;
turn=1;
while(turn!=2 && req1!=0);
//critical section
job2();
req2=0;
• リアルタイムシステムの妥当性検査と検証を行なうツール
• 時間オートマトンを用いてシステムをモデル化
• 到達可能性がチェック可能（これはモデル検査と呼ばれ、基本的に
システムの全ての起こりうる動的な振る舞いを網羅的に調査）
25
安全性の検査
同時に
critical section
に到達しない
検査結果
26
組込みシステム開発の特徴
：システム外の環境から影響を受け、不具合を出すケースが多い
→外部環境を分析する手法を提案
外部環境を分析することで組込みシステム開発における信頼性を
向上させる
上流工程
分
析
下流工程
外
部
環
境
分
析
不具合発覚！
設
計
ドキュメント
実
装
テ
ス
ト
外部環境を考慮したモノ
外部環境に起因するものは
存在しない
→信頼性向上
不具合
27
形式手法の導入方法
・外部環境分析手法 UMLプロファイルを作成
・プロファイルは形式手法への導入を意識して作成している
Ｕ
Ｍ
Ｌ
プ
ロ
フ
ァ
イ
ル
外部環境分析手法
クラス図
形 VDM
式
type
手
・・・
法
operations
・・・
厳密な仕様記述
の探索
状態遷移図
SPIN
active proctype ・・・(){
do
:: ・・・
od
}
システムと外部環境
の振舞いを検証
28
研究室の学生が表彰
第９回組込みシステム技術に
関するサマーワークショップ
（ＳＷＥＳＴ９）
29
３．配属希望の皆さんへ
30
配属希望の方へ
向いている人
言語に関する理論に興味ある人
新しい言語を作りたい人
研究室で重視していること
アイデアを形にし、それを著名な国際会議の場で発信
していく
研究に対する志を持っている方を歓迎
研究の進め方、論文の書き方についてきめ細かく指導
31
一流のエンジニアになるためには
数学
集合論
グラフ理論
論理数学
代数
オートマトン
等々
実際のソフトウエア開発
仕様記述
デザイン
プログラミング
テスト
ブリッジ
安心・安全なシステム構築には必須
抽象化・モデル検査・定理証明
32
Computational Thinking,
Abstraction
物事の本質を掴む、その本質を記述する
抽象化 （数学が重要）
Jeannette M. Wing
(Communications of the ACM
2006.3)
Jeff Kramer
(Communications of the ACM
2007.4)
Daniel Jackson
(The MIT Press)
33
最後に
奥の深そうな着想を見つけて、長期間研究する
研究の成果に対して明確な目的意識をもって研究する
理論的研究は、現実問題に有用であることを、その価値基準とする
力のありそうな人となるべく多くの議論をする
学生は、できるだけ早くかつ多く欧米に行かせ、発表・議論させてくる
理論を研究する学生にも、必ず実装をきちんとさせる
システム実装が得意な学生には、自分の実装の特徴を概念化・明示化す
る訓練をさせ、かつ実装の重要性を自覚させる
各学生には、その人生に１つでよいから、他人が考えたことのない、概念・
アイデア・プロダクトを、確立あるいは作成するという使命感をもたせる
米澤 明憲 「私のソフトウェア研究」より
コンピュータソフトウェア, Vol.21，No.5(2004)
34
© Copyright 2024 ExpyDoc
