Comments
Description
Transcript
資料2 e‐Society基盤ソフトウェアの総合開発 中間成果
誰もが安心して参加できるＩＴ社会を構築する
『e-Society 基盤ソフトウェアの総合開発』
中間成果報告会
主催：文部科学省
２００５年６月３０日（木） １0：００～１5：0０
ホテルフロラシオン青山
目次
○高信頼組込みソフトウェア構築技術
○プログラム自動解析に基づく高信頼ソフトウェアシステムの構築技術
○安全なシステム記述言語および高信頼 OS
○データ収集に基づくソフトウェア開発支援システム
○高信頼構造化文書変換技術
○高信頼 WebWare の生成技術
○インターネット上の知識集約を可能にするプラットフォーム構築技術
○先進的なストレージ技術および Web 解析技術
○ユーザ負担のない話者・環境適応性を実現する自然な音声対話処理技術
e-Society 基盤ソフトウェアの総合開発中間成果報告会プログラム
10:00～10:10
開会の挨拶
星野 利彦
文部科学省研究振興局情報課企画官
土居 範久
10:10～14:55
中央大学理工学部情報工学科教授
プロジェクト中間成果報告
10:10～10:35
○高信頼組込みソフトウェア構築技術
片山 卓也 北陸先端科学技術大学院大学教授
10:35～11:00
○プログラム自動解析に基づく高信頼ソフトウェ
アシステムの構築技術
東北大学教授
大堀 淳
11:00～11:25
○安全なシステム記述言語および高信頼 OS
米澤 明憲 東京大学教授
11:25～11:50
○データ収集に基づくソフトウェア開発支援シス
テム
鳥居 宏次 奈良先端科学技術大学院大学特任教授
11:50～12:15
○高信頼構造化文書変換技術
武市 正人 東京大学教授
(12:15～13:15
昼食休憩）
13:15～13:40
○高信頼 WebWare の生成技術
阿草 清滋 名古屋大学教授
13:40～14:05
○インターネット上の知識集約を可能にするプラ
ットフォーム構築技術
村岡 洋一 早稲田大学教授
14:05～14:30
○先進的なストレージ技術および Web 解析技術
喜連川 優 東京大学生産技術研究所教授
14:30～14:55
○ユーザ負担のない話者・環境適応性を実現する
自然な音声対話処理技術
鹿野 清宏 奈良先端科学技術大学院大学教授
14:55～15:00
閉会の挨拶
星野 利彦
文部科学省研究振興局情報課企画官
高信頼性組込みソフトウェア構築技術
片山卓也
北陸先端科学技術大学院大学
背景
組込みソフトウェアの品質が社会的問題に
• 携帯電話回収、自動車リコール等。メーカ負担も大
• 今後の産業の競争力を左右するキーファクタ
組込みソフトウェア開発は変革期に
• 開発量の増大と短納期化で、従来の徒弟的開発は限界
• IT人材の大量シフトにより、経験に頼った従来手法は破綻
新しい信頼性の枠組みが必要
• 産業の大半を占める民需組込み領域で高信頼性技術の必要性
• 熟練者のノウハウに頼った手法から、科学的な手法へ
2
達成目標 (1/2)
組込みシステム特有の計算資源・実時間処理といった制約を考慮しつつ、ソフト
ウェアの信頼性を高めるために必要となる、分析・設計環境、組込みコンポーネ
ント技術、実時間Java技術を開発する
3
達成目標(2/3)
バグの少ない組込み
ソフトウェアをモデル
ベースで開発
実時間・メモリ制約に
関する機能を提供し、
間違いの少ない
ソフトウェア開発を支援
見逃されたバグによる
システムクラッシュに
備える
4
達成目標 (3/3)
最終年度までに、全体を統合し
「モデル駆動での高信頼性ソフトウェア開発環境」として体系化
UML
設計検証機能
コード生成機能
Javaコード
組込み用ミドルウェア
バグの少ない組込み
ソフトウェアをモデル
ベースで開発
実時間・メモリ制約に
関する機能を提供し、
間違いの少ない
ソフトウェア開発を支援
実時間Java
高信頼実行環境
高信頼OS
見逃されたバグによる
システムクラッシュに
備える
5
分析設計環境(1/3)
目標
• 組込みソフトウェア特有の問題を踏まえながら、UMLを利用して組込みソフトウェ
アを設計し、その正しさを確認・検証（主にモデル検査）することを可能とする分析・
設計環境を実現する
モデル検査を利用したUMLモデル検証の流れ
UMLによる設計
検証モデル作成
検証にかかわる側面の
Promelaによる記述
検証したい性質の
LTL式による記述
UML上で結果の確認
SPINで自動検証
6
分析設計環境(2/3)
現在までの成果
• 組込みソフトウェア検証方法論に関する基本的検討
• 分析・設計環境評価版の構築と実事例（NECエレクトロニクス社製ソフト
ウェア）による設計検証評価
• 派生開発への応用に関する基本的検討
• 実時間制約の解決のための性能解析のための基本的検討
研究項目の追加
• 設計からのコード生成に関する研究の追加
• 事例研究を通じ、設計とコードの関係を明確にすることが実適用上重要である
ことが明らかになったため
7
分析設計環境(3/3)
独創性と優位性
• 一般のソフトウェア技術者を対象とした実用レベルのUML設計検証ツール
は非常に少ない。実際の利用形態に即した機能の提供等
• 組込みソフトウェアに多い、製品系列開発における形式的手法を体系的に
取り扱っている点は他に例がない。これにより本来高コストな検証技術を
妥当なコストで適用できる
• 検証しやすい設計モデルを構築するためにアスペクト指向モデリング技術
を適用している点は新規。これにより分かりやすく、拡張性・再利用性に優
れたモデルが構築できる
8
組込みコンポーネント技術(1/3)
目標
• ソフトウェアをコンポーネントに分割し、分割したソフトウェアを時間的、空
間的に隔離することにより、コンポーネントの障害を隔離し、コンポーネント
を高信頼に実行する環境を実現する
9
組込みコンポーネント技術(2/3)
現在までの成果
• コンポーネントの空間的隔離に関する要求を明確にするために必要なアプ
リケーションの開発
• コンポーネントの時間的隔離に必要な、Linuxカーネル内アカウンティング
システムの開発
• 将来の携帯端末用ミドルウェア・アプリケーション開発のための端末システ
ムプロトタイプ開発
研究項目の追加
• 基盤オペレーティングシステムに関する研究
• 高信頼コンポーネントフレームワークの実現に必要不可欠であることが明らか
になったため
• 企業との共同研究により基盤オペレーティングシステムレベルでのサポートが
より重要であることが明らかになったため
10
組込みコンポーネント技術(3/3)
独創性と優位性
•
•
組込みシステムを対象とした技術
•
大規模システム向けに時間的、空間的隔離を実現する本研究と類似の
システムが存在する。しかし、実用的なレベルで組込みシステムに適
したシステムは存在しない
•
本研究はサーバで一般的なIntelのプロセッサだけではなく、組み込み
で使用されるＡＲＭなどのプロセッサにも対応している
高いリアルタイム性の実現
•
•
従来のシステムは10ms単位の管理しかできなかったが、我々のシステ
ムは100μsの単位で管理できる
システム全体の回復性能の向上
•
アプリケーションに障害が生じた場合でも、その一部のみを回復する
ことでシステム全体の安定化が可能となる
•
従来の手法ではアプリケーションレベルで粗粒度の回復しかできない
11
実時間Java技術(1/3)
目標
• Javaで記述される組込み実時間アプリケーションの開発を効率化するため
の諸技術の開発を目的として、ごみ集めによる停止時間とメモリ制約を解
決する実行基盤の開発、実証実験、要求仕様検証技術との統合を行う
12
実時間Java技術(2/3)
現在までの成果
•
リターンバリアー方式実時間ごみ集めアルゴリズムのオムロン社JeRTy
VM、およびKaffe VMへの実装と評価、優位性の確認
•
複数フリーリストによるメモリー静的最適化方式
研究項目の追加
•
組込み用ミドルウェアの研究
•
実時間ごみ集め処理技術の組込み用としての実用性を検証するため
•
Java処理系に組込みアプリケーション開発のためのミドルウェアを追加
13
実時間Java技術(3/3)
独創性と優位性
• 処理の細分化による実時間ごみ集めの実現
• ごみ集めの処理を細分化し、アプリケーションの停止時間を小さく抑える
• 従来のごみ集め技術は、ごみ集め中にアプリケーションが長時間停止
• 様々なレベルの実時間要求に対応可能
• ごみ集め処理の細分化の程度を変更することで、実時間性のレベルを調整で
きる
• 組込みシステムに適したごみ集め処理
• 本研究の手法は、アプリケーションの実行中に長時間の動作停止を発生させ
ない。組込みシステムのように常に安定した動作が求められるシステムに適し
ている
• 実時間ごみ集め手法は他にも存在するが、いつかはアプリケーションを長時
間停止する処理(major GC)を実行する必要がある
14
研究の実施体制
どのサブプロジェクトも、具体的な問題を抱える企業との共同研究が主体
普及のために関連するコンソーシアム等と連携
各サブプロジェクトは統合に向け定期的打ち合わせ
平成1６年度より具体的活動を開始
全体検討会・ワークショップ等
全体統合調整会議
リーダ：片山卓也
メンバ：各グループの研究者
リーダ：片山卓也
メンバ：各グループの研究者
プロジェクト全体の調整・確認
サブグループ間の相互技術理解
全体統合に関する技術検討
全体統合
分析設計環境
グループ
北陸先端大学
国立情報学研究所
NEC
NECエレクトロニクス
組込みコンポーネント技術
グループ
実時間Java技術
グループ
早稲田大学
筑波大学
松下電器産業
ノキアジャパン
京都大学
オムロン
オムロンソフトウェア
15
企業とのシナジー効果
連携先企業
NEC
連携内容とその効果
UMLモデル検証ツールの研究・開発
企業が持つソフトウェア開発手法やツール開発・適用に関する経験やノウハウを生かして研究・開発を
共同で進めることができた
NECエレクトロニクス
開発事例の提供を受け、検証ツールの適用手法を検討
実プロジェクトにつながる事例についても適用の検討がスタートした
松下電器産業
コンポーネントフレームワーク・ミドルウェア構築技術のプロトタイプシステム評価を依頼
実製品へのツール適用において重要となる点が明確化した
モンタビスタジャパン
コンポーネントフレームワーク・ミドルウェア構築技術の基盤にモンタビスタLinuxを採用
我々の成果がより組込みの実製品に適した技術として実現可能になった
ノキアジャパン
10年後の次世代携帯端末のプロトタイプ作成を依頼
携帯電話メーカーが持つノウハウをベースに、次世代組込みシステムに求められる新しい要求や基盤ソ
フトウェアがサポートすべき機能について有効な指針が得られた
オムロン
組込み用実時間Java技術を、同社が販売する組込みシステムプラットフォームに適用
同社プラットフォームの性能が大幅に向上し、ソフトウェア開発コストが削減できた
16
経済的効果
17
研究成果普及への取り組み
研究成果の内容、産業界での活用のされ方を踏まえ、適切な施策を進めている
• 標準化への取り組み
• 日本エンベデッドリナックスコンソーシアム リソースマネジメントWGにおいてアカウンティ
ングシステムAPIの標準化
• 特許等
• 分析設計環境に関する特許（企業側で現在準備中）
• 製品化
• オムロン社のJavaで記述された実時間組込みアプリケーション製品すべてに、我々の実
時間ごみ集め技術を実装した処理系が利用される予定
• 無償提供
• 分析設計環境を、評価目的での試用を希望する大学や企業に無償貸与
• アカウンティングシステムをオープンソースで公開
– https://sourceforge.jp/projects/cabi
• Kaffe VMに対する実時間ごみ集め処理技術の実装をフリーソフトウェアとして公開予定
• その他
• マイクロカーネルに基づく仮想化技術をWebで公開中
– 本技術のソースコードをベースに事業化を検討している企業あり
18
人材育成の状況
現在までの育成状況
• 修士課程15名、博士課程9名、ポスドク4名を育成
組織
修士課程
博士課程
ポスドク
北陸先端大
10
5
1
早稲田大学
5
1
1
京都大学
0
3
2
合計
15
9
4
効果
• ツールだけでなくそれを利用できる人材の育成が不可欠。既に就職先で検証事例
を成功させた例も出ている
• 組み込みOSの知識を持つ人材は、今後企業でアーキテクチャ開発をリードできる。
既にコンサルタントを実施し、評価を受けている
• 社会人育成のためにJAIST田町キャンパスで検証技術等の人材育成を進めている
19
論文・発表
学術活動の成果
ジャーナル
11
国際会議
23
研究発表・講演など
14
合計
48
社会への情報発信活動状況
メディアへの情報発信・新聞報道など
1
ウェブサイトなどでの情報公開
2
その他の広報活動(講演・デモなど)
22
合計
25
20
参考資料
分析設計技術グループ
UML設計検証ツール
検証項目の例：
・外部からどんな入力がどんな順序や組合
せで来ても正しく動作するか
・どんな状況でもデッドロックが起こらないか
・危険な状態に絶対に入らないか
①UMLをみながら設計・検証指示
③問題があればUML上で結果を解析可能
ステート図
クラス図
シーケンス図
検証したい
UML設計
上の項目
②ツールが内部的に形式手法を適用
検証の初期状態の指定
状態再現機能・構成管理機能 必要な情報の関連
22
プロダクトライン開発への適用
組込みシステムの多くは製品系列開発
再利用可能な検証モデルを再利用資産として体系化
• フィーチャモデル、設計モデル、検証モデル間にトレーサビリティ定義
設計モデルだけでなく対応する検証モデルを効率的に作成
再利用による設計モデル構築
Agent
フィーチャモデルを利用して
製品への要求を定義
PROCESS
Download
<<CONTEXT>>
CONTEXT
SENSOR
Safer
Agent
Server
OPTIONAL
Wireless
LAN
Available
Server
Install
Safe Guard
Safety
<<CONTEXT>>
Connection
<<CONTEXT>>
Safety
Panel
Operation
Operation
OPTIONAL
PDC
Parking
Brake
^stop
<<environment>>
Gear
Position
Agent
Operation
Safer Agent
Safety
OPTIONAL
<stop condition>
OPTIONAL
対応する検証モデルの
再利用による構築
stop
^install
^skip
S1
INSTALLING
^to unsafe
SAFE
UNSAFE
^to safe
to unsafe
[] ((Operation@INSTALLING && <stop condition>) -> <> (Agent@STOP))
23
オブジェクト指向設計モデルの
データフロー解析法
オブジェクト指向設計モデルにおけるデータの流れをモデル検査ツールＳＰＩＮ
で解析。
Producer
Consumer
変換
データフローに注目し
た振る舞い記述
オブジェクト指向設計モデル
aho
foo
bar
データフロー
proctype Producer(...){
....
}
proctype Consumer(...){
...
}
変換
SPIN
( bar ⇒ ◊ foo )
¬ ( afo ∧ ◊ bar )
データフローを
表現するＬＴＬ式
24
並列処理モデルへの変換による、
オブジェクト指向システムの実時間解析
オブジェクトの振る舞いモデルを処理列中心のモデルへ変換
• オブジェクト指向組み込みソフトウェアの実時間性解析のための論理的基礎
Obj1
Obj2
Obj3
Obj1の処理
Obj4の処理
Obj3の処理
Obj2の処理
Obj4
Obj4の処理
Obj3の処理
25
参考資料
組込みコンポーネント技術グループ
QOSサポートの概要
リアルタイム
プロセス
タイムシェアリング
プロセス
20%
階層型スケジューラ
30%
アカウンティング
システム
27
QOSサポートシステム
アカウンティングシステム
• アカウンティングオブジェクト： 周期と実行時間
• 複数のプロセスを1つのアカウンティングオブジェクトにバインド可能
• 新しいプロセスと生成する場合は、親プロセスのアカウンティングオブジェクト
をバインドする
階層型スケジューラ
• プロポーショナルフェアスケジューラ
• タイムシェアリングスケジューラを最大限優先可能な割合を指定可能
• アプリケーションプログラムの変更が不要
28
アプリケーション隔離の概要
Protected Domain
Application
Application
Application
ITRON Kernel
Protected Domain
Protected Domain
Application
Application
Application
Application
…
Application
Application
ITRON Kernel
Linux Kernel
Protected Domain
Application
Application
Application
Linux Kernel
TL4 Microkernel
29
アプリケーション隔離システム
TL4マイクロカーネル
• ドイツカールスルーエ大学が開発したL4 μ-kernelをベース
• 以下の機能を提供する
• スレッド, プロテクションドメイン, メモリページ, IPC
• オリジナルからの拡張
• スケジューリング, リソース管理, セキュリティ
OSパーソナリティ
• Linux： Linuxの実行セマンティクスも保存することによりリアルタイムアプ
リケーションの移植性も保証
• μITRON： 高速な応答性を保証することにより, 既存のITRONアプリ
ケーションを利用可能
• デバイス共有フレームワーク
30
次世代携帯端末
Camera
Compass
RFID
GPS
antenna Reader
Microphone
Full color LED
Speaker
Rear Camera
Barometer
Pulse sensor
Grip Sensor
GPS
ノキアジャパンとの
共同開発
Skin resistance
sensor
Micro Joystick
Air temp.
Relative Humidity
sensor
3D Linear
accelerometer
LCD & Touch Panel
31
参考資料
実時間Java技術グループ
JeRTyVMにおける
リターンバリア方式実時間ごみ集めの実装
Java実行環境には、不用なメモリを回収するごみ集め（Garbage
Collection，GC）が存在
一般的に，GCは一括でごみ集めを行うため実時間処理には適し
ていない
実時間処理に適した方法として，湯淺（京大）らが，スナップショッ
トＧＣとその改良版であるリターンバリア方式を開発した
これらの方式を，オムロン社が組込みJavaアプリケーションの実
行環境として開発してきたJeRTyVMに実装し、評価した
33
JeRTyVM
オムロン（株）が開発した組込みシステム用実時間Javaアプリ
ケーション実行環境
実時間OS(ITRON）上で動作
商用の組込みシステムに利用されてきた
実時間処理
• on-the-fly方式による中断・再開可能なGC
• 周期タスクとして動作するGC
• コンパクションでのコピー処理
• 実時間処理用拡張APIの実装
34
スナップショット方式
マーク・アンド・スイープ方式を基礎とした実時間ＧＣのアルゴリズム
プログラム実行用とＧＣ実行用の２つのプロセッサを並行に動作させることで、
ＧＣの中断・再開を実現
ライトバリア（write barrier）が必要：オブジェクトの参照を代入する際に，その
場所から参照されていたオブジェクトがまだマークされていなければマークする．
これをマーク
スタックなどのルートにはバリアが不要⇒実行性能向上
スタック全体を同時に走査する必要あり
35
リターンバリア
スナップショット方式のスタック走査を分割
• ⇒実時間性の向上
リターンバリアを越えてリターンするときに一定個のフレームを走査
• ⇒走査済みのフレームのみが参照されることを保証
scan
return
current
frame
stack
stack
stack
36
性能評価（プログラム実行時間）
30%程度速度向上
JVM命令でのライトバリアの変更が大きな要因
ＧＣの高優先度の時間が短くなったのも理由の１つ
100
80
%
100
100
100
73.5
72
64.9
60
40
20
0
マ ージ ソート
D IV
従来版
FFT
リターン バ リア 版
37
プログラム自動解析に基づく
高信頼ソフトウエアシステムの構築技術
東北大学 電気通信研究所
大堀 淳
２００５年６月３０日 中間成果報告・自己点検評価
背景：ソフトウエア生産の現状
現在のソフトウエア生産はあまりに脆弱
整合性検証がされていない膨大なコード
実行時の型エラーによるシステム障害
バッファオーバフローによる危険なコードの実行
システム間の結合における潜在的な不整合
JAVAとWebシステム間の文字列によるアドホックで脆弱
な結合
データベースなどとの インピーダンスミスマッチ
⇒ 「信頼性ボトルネック」： 高信頼性確保が，社会の生
産性を低下させる大きなコスト要因．
背景：高信頼言語の現状
型理論（プログラム自働解析）に基づく高信頼言語ML
すべての型エラーの自働検出と除去による高い信頼性
高水準記述による高生産性
しかし，ソフト生産に生かされていない．
静的型システムの柔軟性の欠如
SQL，JAVA等との相互運用性の欠如
プログラミングツール，開発環境の欠如．
⇒「次世代de facto standard」： 理論を生かした実用的な
高信頼技術の確立が次世代ソフトウエア生産における重
要で支配的な技術となりうる．
研究開発の目的
「世界最先端の理論と技術」＋「現実に即した実用化」に
より
（１） 次世代高信頼言語：SML#
より柔軟で強力な静的型システム
データベース，Java, Cなどとの高い相互運用性
（２） プログラム開発ツール
Javaコンポーネントの整合性解析ツール
SML#を含む多言語環境のプログラミングツール
の２つを開発・統合し，世界最先端の高信頼プログラ
ム開発環境を実現．
型の柔軟性の欠如
ツールの欠如
SML#
相互運用高信頼言語
相互運用性の欠如
Java
SQL
インターフェイスの不整合
C
スクリプト言語，CGI
型エラー
SQL
Java
C, アセンブラ
型理論を基礎とする
•コンポーネント整合性検証
•プログラミング自動化ツール
高信頼ソフトウエア構築環境
高機構高信頼ソフトの効率よい開発
高信頼言語
「世界最先端の理論と技術」
以下を含む世界的にも最先端理論・技術を基礎とする．
多相型レコード計算（Ohori, ACM TOPLAS（１）, 1995）
より柔軟で実用的な型システム
世界で最も読まれているMLプログラミングの教科書などで取り
上げられ，次世代言語のプロジェクトプロポーザルなどでもこ
れを超える技術の理論・技術の実現が目指された先端技術．
データベースとの連携（Buneman, Ohori, ACM TODS（２）,1996）
高信頼言語とデータベースとのシームレスな統合の基礎．
この技術に関する先駆けであり，世界的に知られた基礎理論．
しかし，これら技術を実用化した言語はまだ存在しない．
（注１） ACM TOPLAS:プログラミング言語分野最高の雑誌．過去１０年間累計の日本の論文は５件程．
（注２） ACM TODS:データベース分野最高の雑誌．過去１０年間累計の日本の論文は２件程．
「現実に即した実用化」
大学と企業の連携により，先端理論を実用システムへと
完成させる．
必要性を反映した実用化（沖電気，算譜工房と連携）
大規模Webシステム開発事例の分析を通じたツール仕様
現実のシステムへの適用を通じた言語やツール評価
実用プログラミングツールの開発
実装技術，アルゴリズムの開発（東北大・北陸先端大）
相互運用可能GC
Javaコード解析技術
Javaコンポーネントの整合性解析の型理論
実施体制
東北大・北陸先端大 大堀研究室
ＳＭＬ＃言語，プログラム開発環境の設計・開発全般
沖電気工業（株）金融ソリューション開発本部
JAVA 開発環境の実例調査，詳細設計・開発，
さらに，プロジェクトの後半では，実際の大規模開発業務に適
用した検証
算譜工房（有）
ＳＭＬ＃言語開発
東京工業大学 渡部研究室
プログラム開発環境の基礎理論・基本方式の設計，開発
目標とした具体的成果
中間目標（３年目，平成１７年度末）
ＳＭＬ＃ 言語
バイトコードコンパイラ，バイトコード処理系
プログラム開発ツール
インターフェイス整合性チェックツールのプロトタイプ
SML#のための種々の開発支援ツール
最終
ＳＭＬ＃ 言語
ネイティブコードコンパイラ，実行時ライブラリを含む言語システム
プログラム開発ツール
インターフェイス整合性チェックツール
ＳＭＬ＃のための種々の開発支援ツール
以上を統合した，高信頼プログラム開発環境．
年次計画：ＳＭＬ＃
平成１５年度
コンパイラフロントエンド（パーザ，型推論，パターンマッチング），
バイトコード処理系（ごみ集め処理，抽象器械）
平成１６年度
コンパイラバックエンド（多相型レコードコンパイル，A-正規変換， コー
ド生成， クロージャ変換）
平成１７年度
バイトコードコンパイラ，バイトコード処理系完成
平成１８年度
ネイティブコードコンパイラ
プログラム環境との統合
平成１９年度
製品化および評価
年次計画：プログラム開発ツール
平成１５年度
コンポーネント解析ツールの実現方式
平成１６年度
Javaコンポーネント整合性解析ツールプロトタイプ.
平成１７年度
Javaコンポーネント解析ツール完成.
平成１８年度
SML#と統合した開発環境の構築
平成１９年度
製品化および評価
計画と進捗状況
開発項目
H15年 H16年 H17年 H18年 H19年
バイトコード処
理系
SML#言語
ネイティブコード
処理系
SML開発ツール
相互運用実行
時ライブラリ
プログラム Javaインタフェイ
開発ツール ス解析ツール
相互運用プログ
ラム開発環境
相互運用高信頼プログラ
ム開発環境
研究の効率化と目標の拡大
ML系言語自動プログラミングツール
SML#コンパイラの効率的開発のため，以下の自動プログラム
ツールをプロジェクト内部で開発
ドキュメント自働生成システム SMLDOC
MLソースコードからドキュメントを自働生成
プリンター自働生成システム SMLPPG
種々のデータ型のプリンタを，型情報によって自働生成
これらは，我々のプログラム開発の必要性から生まれた実用
性の高いツール．SML#と共に１７年度末リリース予定．
関数システム設計論（Functional Development）
システム開発で得られたノウハウをオブジェクト指向設計に代
わりうる設計論としてテキストにまとめ，公表・出版を計画．
プロジェクト計画の修正
相互運用処理系
理論，方式，アルゴリズム，システム開発を同時に行
う先端技術開発の効率的な実現のため，
実行時ヒープエミュレータの開発を追加
これにより，相互運用実行時ライブラリの種々の方式のプ
ロトタイプ構築とテストが可能となった．
相互運用実行時ライブラリ開発時期の延期
エミュレータによるテスト済みプロトタイプの実装になるた
め効率よく実装可能で，システム全体としては遅れはない．
プログラム開発環境の基礎理論（渡部研究室担当）
米澤グループとの成果の統一のための基礎理論研究．
米澤，大堀グループの独立に伴い，e-Societyの枠か
ら独立した共同研究としての実施へ変更．
成果概要：SML#言語
SML#バイトコードコンパイラ
コーディング終了．現在系統的なテストを実施中
テスト数
成功数（６月１5日現在）
成功割合
2899
2837
97.9%
テストケースは，仕様（型推論規則）から系統的に設計作成したもの．
すべてのテストケースを毎日深夜自動実行．
SML系言語用自動プログラムツール
SMLDOC
ツール，マニュアル（ドラフト）完成
SMLPPG
ツール，マニュアル（ドラフト）完成
成果概要：プログラム開発ツール
Javaコンポーネント解析ツール
事例調査： ２８K，１３４Kの開発事例分析，調査
脆弱性要因分析
２分類，４種類，１４項目の脆弱性要因を特定．
基本方式，アルゴリズム
多相型理論を基礎とするチェック方式完成
プロトタイプ開発
典型的な５パターンについてシステムを実装．
ツール仕様策定
検証対称６１パターンを特定．
研究成果のリリース予定
SML#バイトコードコンパイラ（予定通り）
研究者向け：２００５年１０月
一般向け：２００６年２月
ML系言語用自働プログラムツール（追加項目）
研究者向け：２００５年１０月
一般向け：２００６年２月
Java整合性解析ツール（予定通り）
一般向け：２００６年２月
主な学術的貢献
T. Higuchi and A. Ohori, A Static Type System
for JVM Access Control. To be accepted
subject to minor revisions to ACM TOPLAS．
（本論文の正確な情報：TOPLAS編集長からの２００５年５月４日付けの通知（抜粋）：
論文のステイタス: minor revisions required.
担当エディタのコメント：
Dear authors, The reviewers rather liked your paper, so I am going to
accept it with minor revisions, that is, provided you revise the paper
following the Reviewers suggestions.
Best regards,）
（注）ACM TOPLAS：プログラミング言語で最も権威とインパクトの
ある雑誌．日本の研究機関からの採録は過去１０年間の累計で
４件のみ（他に海外と日本の共著２件） ．４件のうち１件は我々
のSML#の基礎理論の論文．
主な学術的貢献
A. Ohori: Register Allocation by Proof Transformation,
Journal of Science of Computer Programming, 50(1-3):161 187, 2004. (下記同名論文が雑誌に投稿を招待され，投稿，採
録されたもの．)
T. Higuchi and A. Ohori, A Static Type System for JVM
Access Control, Proc. ACM International Conference on
Functional Programming (ICFP), 227 - 237, 2003.
A. Ohori， Register Allocation by Proof Transformation, Proc
European Symposium on Programming (ESOP), 399-413,
2003.
Kanghoon Choi and A. Ohori, A Type Theory for KrivineStyle Evaluation and Compilation, Proc. Asian Symposium on
Programming Languages and Systems, Springer LNCS 3302,
213-228, 2004.
国際会議での情報発信
A. Ohori. Type-Directed Garbage Collection with
Explicit Layout Bitmaps for a Polymorphic Language.
International Lisp Conference, New York, 2003.
(Invited talk).
A Ohori, A Logical Approach to Compilation and
Machine Code Analysis, The Second Asian Workshop
on Foundations of Software, Nanjing, China, 2003.
(Keynote Speech).
世界への成果の発信にむけて
成果は世界への発信を目指す．その準備として，以下の
研究者からなる国際評価委員会を設置
Simon Peyton Jones (Microsoft，関数型言語)
Zhong Shao (Yale U．，MLコンパイラ)
Peter Buneman (Edinburgh U．，データベース言語)
加藤和彦 （筑波大，OS言語統合フレームワーク）
いずれも，それぞれの分野の第一人者．
（すでにすべてのメンバーより承諾を得ている．）
SML#リリース後，第１回の評価を依頼予定．
人材養成の方針と成果
修士課程
高信頼言語による開発技術者
平成１５年度： ５名
平成１６年度： ６名
博士課程
先端システムの設計開発ができる研究開発技術者
平成１５年度： ５名
平成１６年度： ０名
ポストドクタ
世界レベルの研究者．世界の研究機関から登用
平成１６年度： １名（韓国KAISTから）
他プロジェクトとの連携
加藤和彦氏のCREST「自律連合型基盤システムの構築」
と本e-Societyの両プロジェクトの最終成果を発展統合し，
オープンかつ理論的整合性を検証可能なプログラミン
グレイア
を共同で構築．システム・OSと言語の相補的な２つの中
核先端技術を統合する大きなシナジー効果が期待できる．
実施計画（プロジェクト最終年から３∼５年程度を想定）
コンポーネントを一般化した計算の単位の合成や移動のた
めの型理論的基礎の確立
高信頼言語を中核とする自律連合プログラミングモデルの構
築
システムの実現
産業界との連携，成果の普及
設計，開発段階
沖電気工業（株）金融ソルーション開発本部にて，現実に行ったソフトウエ
アプロジェクトの分析を通じ，ソフトウエア開発環境に必要な機能を分析．
⇒ 産業界にて実際に有用なツールと開発環境の構築を目指す．
製品の利用，普及
沖電気工業（ 株） 金融ソルーション開発本部にて， 高信頼web アプリ
ケーションソフトウエア構築に利用予定．
⇒ 高信頼性，短納期が要求されるこれら先端ソフト生産分野での生産性
および競争力の強化
ハードウエアや金融システムなど高信頼性が要求される分野への応用．
算譜工房（有）にて特化したソフトウエア開発，さらに，これら特化したベン
チャー等の設立・育成．
企業グループ等のコンソーシアム等を通じて使用／流通の努力．
今後の方針
当初の予定通り研究開発を進める．
SML#言語
ネイティブコードコンパイラ（１８年度）
多言語相互運用ライブラリを含む実行時ライブラリ（１８年
度）
プログラム開発環境への統合のための実行時モジュール
（１９年度）
プログラム開発ツール
SML#と統合した開発環境の構築（１８年度）
大規模な評価と製品化（１９年度）
上記の高信頼開発環境への統合（１９年度）
成果の詳細
以降にこれまでに得られた以下の成果の詳細を記す．
SML#言語
SMLDOC
SMLPPG
Javaインターフェイス整合性解析ツールプロトタイプ
成果の詳細：ＳＭＬ＃
ＳＭＬ＃コンパイラの構成と完成部分
バイトコードコンパイラ（ほぼ完成）
1.
2.
3.
4.
5.
6.
7.
8.
字句解析，構文解析(15年度構築）
ランク１，レコードを含む型推論(15年度構築）
パターンマッチングコンパイル(15年度構築）
多相型レコード演算のコンパイル（１５，１６年実施）
A-Normal 変換（１６年実施）
クロージャ変換（１６年実施）
ビットマップパッシング変換（１６年，１７年実施）
コード生成（１６年，１７年実施）
バイトコード処理系（ほぼ完成）
1.
2.
抽象機械
相互運用ヒープーのためのビットマップトレーシングＧＣ
ＳＭＬ＃の開発済新機能（１）
ランク１多相型
->fun f x y = (x,y);
val f = fn : ['a.'a -> ['b.'b -> 'a * 'b]]
->f 1;
val it = fn : ['a.'a -> int * 'a]
val it 2;
val it = (1, 2) : int * int
レコード多相型
->fun name x = #name x;
val name = fn : ['a#{name:'b},'b.'a -> 'b]
->name {name = "joe", age = 21};
val it = "joe" : string
ＳＭＬ＃の開発済新機能（２）
高効率な型推論アルゴリズム
以下のようなコードの型推論は，従来のコンパイラは指数関数時
間を要するが，本コパイラでは一瞬で終了する．
let
val a= (fn x=>x, fn y=>y)
val a= (a, a)
...
val a= (a, a)
in
#1 (#1 (#1 ... (#1 a) ... )))1
end
ＳＭＬ＃の開発済新機能（３）
相互運用可能なヒープ
従来のＭＬ系言語：実行時オブジェクトは他の言語と互換性なし
ＳＭＬ＃：ＣやＪＡＶＡと同一のメモリーモデルを持ち相互運用可能．
以下の先端理論の実装により実現
ビットマップトレーシングＧＣ
型主導ビットマップパッシングコンパイル
コンパイラ実装：エミュレータで動作確認済み．
ＳＭＬ＃の開発済新機能（４）
高速バイトコード処理系
従来のスタックアーキテクチャに代えて
３アドレス抽象機械命令セット
証明論に基づくレジスタ割付方式
の組み合わせによる新規な抽象機械を設計・実装
エミュレータによるシュミレーションの結果，従来の処理
系（例ＯＣＡＭＬ）を凌ぐ速度が得られる可能性を確認．
１７年度に，最適化，性能評価実
成果の詳細：ＳＭＬＤＯＣ
ソースコード群からシステムのドキュメント自動生成
ソースコードを解析し以下の構造を自動認識
モジュール，シグニチャー
関数，変数定義
型，datatype定義
例外定義
豊富なドキュメントコメントを認識
@author, @version, etc
@params, @return, @exception, etc
ソースコードのブラウズ機能
ＳＭＬＤＯＣの例
成果の詳細：ＳＭＬＰＰG
型宣言からその型のプリンターを自動生成
基底型 ⇒ 清書関数
型構成子 ⇒ 清書関数生成関数
豊富なフォーマットコメントを認識
自動字下げ，字下げのスコープ，
演算子の結合力
ガード
大規模実用システムに耐える機能
ＳＭＬ＃コンパイラのメッセージは本ツールで自動生
成
ＳＭＬＰＰG使用例（１）
ＳＭＬＰＰGのソース
(*% *)
datatype exp
= (*%
* @format(const * loc) {const}
*)
EXPCONSTANT of constant * loc
¦ (*%
* @format(cond * ifTrue * ifFalse * loc)
*
N0{ "if" 2[ +d {cond} ]
*
+1 "then" 2[ +d {ifTrue} ]
*
+1 "else" 2[ +d {ifFalse} ] }
*)
EXPIF of exp * exp * exp * loc
¦ (*%
* @format(exp * rule rules * loc)
* N0{ "case" 2[+d {exp}] 2[+1 "of" ]+ {rules(rule)( 2[ +1 "¦"] +)} }
* @format:rule(pat * exp) {{pat} + "=>" +1 {exp}}
*)
EXPCASE of exp * (pat * exp) list * loc
ＳＭＬＰＰの使用例（２）
プリント例
let
val exn = getException context
val message =
case exn
of SystemError => "SystemError"
¦ UserError msg =>
"User:" ^ msg ^
(
concatWith "¥n"
(
map (frameToString context) (getFrames context)
)
)
in raise Error message end
成果の詳細：Ｊava解析ツール
目的
Webアプリケーションなどのコンポーネントベースの
大規模ソフトの高信頼化ツール
現状
インターフェイスの不整合により，大規模システムは
脆弱性をもつ（開発者の一般的な認識）
我々の戦略
Ｓｔｒｕｔｓを基礎とする現実の大規模開発の調査による脆弱
性の原因の分析（平成１５年度完了）
型理論によりチェック方式の構築（完了）
システム開発（システム設計，プロトタイプ開発終了，現在
リリース版を開発中）
現実のシステムでの有効性確認と改良
開発事例による脆弱性分析概要
全弱製の主な要因は，コンポーネント間の依存関係による
パターン1
JavaClass
JSP
パターン2
属性名
パターン3
ActionForm
メッセージ
パターン4
JavaBeans キー名
・ActionForm 論理名
・DynaActionForm 属性名
・リクエストパス名
・フォワード名
リソースファイル
ActionError キー名
属性名
ActionForm
論理名
validation.xml
ルール名
ActionError 値
Action
JavaBeans キー名
・フォワード名
・ActionForm
論理名
struts-config.xml
validation-rules.xml
依存関係の分析と分類
依存関係は大別すると以下の２つ
静的マッピング生成
設定ファイルを参照する依存関係
キーと値の組が初期化時に生成される
動的マッピング生成
ソース中に記述した文字列等を参照する依存関係
キーと値の組がAP実行中に生成される
派生パターンが２つ
静的，動的マッピング生成に付随する段階チェック
キーで取得したオブジェクトの属性をチェックする
静的，動的マッピングの複合
依存性チェックツール構築戦略
重要でかつ大部分の脆弱性の原因は静的依存性
静的依存性の分析
インタフェースを実現する種々の属性
属性名の共有によるコンポーネント間の依存
多相型レコード計算の考え方を使い，依存性解析問
題を，型付け問題に還元
依存性チェックロジックの構築する
インターフェイス依存性分析のための型システムを定義
型推論アルゴリズムを構築
以上の型理論を構築済み．現在システム開発中
開発ツールの概要
プログラマが記述したソースコード，設定ファイル間の整合
性チェックを行う
Java
XML
<action path=“login” ・・・
JSP
<html:form action="/logon">
リソース
ファイル
入力 チェックツール
出力
○△.jsp ファイル，
△行目の×× が
コンフィグファイル
と不整合
依存チェック処理概要
Java ソース
(Action，Form)
struts-config.xml
メッセージ
リソースファイル
JSP ファイル
XML情報
設定処理
リソースファイル
解析関数
JSP ファイル
解析関数
Action ファイル
解析関数
JSP
型情報
Action
型情報
システム型情報
型判定処理
Form ファイル
解析関数
Form
型情報