ソフトウェア開発方法論

ソフトウェア開発方法論
北陸先端科学技術大学院大学
片山卓也
平成13年3月7日
公開シンポジウム
1
目標
• 科学的方法論に基づく実用的ソフトウェ
ア開発方法論の確立
– 科学的・理論的研究にもとづいたパラダイムや方法
論によって現実のソフトウェア開発問題を解決する
– 理論のためだけの研究は行わない
– 現実問題の複雑性、規模を考えたアプローチ
• Toy problemsだけに適用可能な手法はとらない
平成13年3月7日
公開シンポジウム
2
背景
• 現代社会を支える大規模、高度ソフトウェアの開発・
保守の必要性
• ソフトウェア開発方法論の実務
– オブジェクト指向方法論、ソフトウェアプロセス、開発環境
• ソフトウェア開発のための理論
– 形式的仕様記述、意味論、検証法
• ソフトウェア開発の実務と理論の乖離
– 理論的成果が現実のソフトウェア開発に生かされていない
• 新しいソフトウェアに対する需要
– モーバイル、分散協調
平成13年3月7日
公開シンポジウム
3
サブプロジェクト
• 発展的ソフトウェア開発方法論（北陸先端大：片山）
– 形式的オブジェクト指向開発方法論、発展的ソフトウェア開
発原理・方式、フォールトトレラントソフトウェア開発方法
論
• ソフトウェア開発アルゴリズム（早稲田：二村）
– 一般部分計算（ＧＰＣ)にもとづくプログラム最適化、プログ
ラム性能・信頼性評価
• ソフトウェア開発における形式化技術と環境（東工
大：米崎）
– 形式論理に基づく平行・分散システムの仕様記述、定理証明
技術による仕様検証および環境
• 開放性をもつ並行・分散ソフトウェア記述系(東大：米
澤)
公開シンポジウム
平成13年3月7日
4
北陸先端科学技術大学院大学
要求分析、ソフトウェア発展
問題Ｐ
形式的オブジェクト指向方法論
ソフトウェア発展方式、メカニズム
実世界Ｗ
仕様書
東京工業大学
仕様検証
Spec Item 1：pop(push(X,s))=X
Spec Item 2：∀x1,x2∃z1,z2.
{ x1,x2≧0⊃x1=x2*z1+z2
Λ 0≦z2＜x2}
形式論理による仕様記
述
定理証明
早稲田大学
プログラム生成・最適化、評価
一般化部分計算、評価システム自動生成
平成13年3月7日
公開シンポジウム
東京大学
モーバイル言語、
安全性
設計と実装
(
d
e
f
u
n
(
r
c
s
w
r
i
t
e
(
i
f
(
e
r
r
o
r
o
c
c
u
r
r
e
d
(
w
r
i
t
e
c
u
r
r
e
n
t
f
i
l
e
)
)
(
i
f
b
u
f
f
e
r
i
s
m
o
d
i
f
i
e
d
(
d
o
c
h
e
c
k
o
u
t
(
c
u
r
r
e
n
t
b
u
f
f
e
r
n
a
m
e
)
)
)
)
(
n
o
v
a
l
u
e
)
)
(
d
o
c
h
e
c
k
o
u
t
c
b
u
f
c
o
f
n
a
m
e
(
s
e
t
q
c
b
u
f
(
a
r
g
1
)
)
(
s
e
t
q
c
o
f
n
a
m
e
(
a
r
g
2
)
)
(
i
f
(
|
(
f
i
l
e
e
x
i
s
t
s
(
c
o
n
c
a
t
"
R
C
S
/
"
c
b
u
f
"
.
v
"
)
)
(
p
r
o
g
n
(
m
e
s
s
s
a
g
e
"
p
l
e
a
s
e
w
a
i
t
,
n
o
w
l
o
o
k
i
n
g
"
)
(
e
x
e
c
u
t
e
m
o
n
i
t
o
c
o
m
m
a
n
d
(
c
o
n
c
a
t
.
.
.
(
m
e
s
s
a
g
e
"
d
o
n
e
"
)
5
研究成果
• 代表的研究成果
– 形式的オブジェクト指向分析支援環境F-Developer、
リアクティブモデルObTS実行環境、ソフトウェア
発展のための理論体系(片山グループ)
– GPCによるプログラム自動超高速化システム
WSDFU、テストデータ自動生成システム、計算量
自動評価器(二村グループ)
– 時間論理によるリアクティブシステム仕様記述記述
のための種々の論理体系、時間論理証明システム
T3(米崎グループ)
– 移動コード技術に基づく安全なソフトウェア構築た
め言語の設計と実装、次世代ネットワークソフト
ウェア配信システム(米沢グループ)
平成13年3月7日
公開シンポジウム
6
• 開催したワークショップ、国際会議（11件）
– International Workshop on Principles of Software Evolution, （Kyoto,
April,1998）
– ---（Fukuoka,July,1999）
– International Symposium on Principles of Software Evolution, Kanazawa, Nov.
2000
– Waseda Partial Evaluation and Program Transformation Day, Nov.15,
Tokyo,1999
– プログラム変換と記号・数式処理シンポジウム、Nov.1999, 京都
– Colloquium on Attribute Grammar and Program Optimization, Tokyo, July,
2000
– International Software Engineering Symposium, China, March, 2001
– International Workshop on Timed System, Kyoto, March，1999
– International Workshop on Software Specification and Design, Toba, May,
1998
– Workshop on Foundations for Secure/Survival Systems and Networks, Tokyo,
2001
– International Workshop on Mobile Objects/Code and Security, Tokyo, Oct.2000
平成13年3月7日
公開シンポジウム
7
• 査読つき論文総数
• 招待講演、論文
１７８
２１件
• 特許
(二村グループ)
– ランダムデータジェネレータ生成方式およぶそのプ
ログラム
– 連結グラフの生成方式およびそのプログラム
– 出願準備中2件
• 新聞報道
（二村グループ）
平成13年3月7日
5件
公開シンポジウム
8
• 公開ソフトウェア
–
–
–
–
–
–
–
–
–
–
–
–
–
–
リアクティブシステム設計支援システムObTS
形式的オブジェクト指向分析支援システムF-Developer
ランダムデータサーバ RDS
T(n)ソルバー
プログラム高速化システムWSDFU
T3エンジン、ビューワ、プリコンパイラ
デザインパターンにもとづクラス図作成支援システム
CTAGシステム
PF-Webシステム
CATシステム
Stack Threads/MP
Distributed GC
JavaGo
MIC
平成13年3月7日
公開シンポジウム
9
発展的ソフトウェア開発方法論
（片山グループ）
• 研究内容
– 発展的にソフトウェアを開発するための原理とその
ためのモデル、方法論
• 発展的ソフトウェア開発原理・方式
– 発展ドメイン理論によるソフトウェア発展原理
– 抽象解釈原理にもとづく発展的ソフトウェア開発法
• 形式的オブジェクト指向方法論
– 形式的分析モデル構築・検証システム
– リアクティブシステム構築システム
平成13年3月7日
公開シンポジウム
10
発展的ソフトウェア開発原理・方式
– 発展ドメイン理論によるソフトウェア発展原理
• 発展ドメイン：
– 許容可能な仕様やプログラムの「変化」を表す順序構造
• 合理的な発展を許容する開発プロセス：
– 発展ドメイン間の準同型写像
– 抽象解釈原理にもとづく発展的ソフトウェア開発法
• 段階的詳細化法
• 詳細化の初期の段階から抽象的に動かす
• データの抽象化：
– 関数型プログラム
• イベントの抽象化：
– オブジェクトの振る舞いの段階的構築
平成13年3月7日
公開シンポジウム
11
形式的オブジェクト指向方法論
• オブジェクト指向方法論
– ソフトウェア設計の最も有効かつ自然な設計･開発
方法論
• 現在のオブジェクト指向開発方法論
– 形式性が低く有効な計算機支援が困難。
– 分析から実装までの一貫した方法論が存在しない。
平成13年3月7日
公開シンポジウム
12
形式的オブジェクト指向方法論
• 形式的アプローチ
– 仕様やモデルを数学的対象としてとらえる。
• オブジェクト指向方法論への形式的アプローチ
– 「形式的方法論」のオブジェクト指向化
• オブジェクト指向Ｚ、代数的アプローチ、ＶＤＭ、･･･
• 現実のオブジェクト指向方法論の実際とは方向性が異なる。
– 現実に行われているオブジェクト指向方法論の形式
的アプローチが必要。
平成13年3月7日
公開シンポジウム
13
形式的オブジェクト指向方法論
• 目標：形式的手法にもとづく一貫した方法論の展開
– 形式的モデル記述体系
• 複数の観点からのモデル化
• オブジェクトモデル、動的モデル、…
• UML：9モデル
– 分析モデル間の整合性、統合モデルの構成
– 分析モデルの適切性・一貫性の検証
• 統合モデルのプロトタイプ実行
• 定理証明技術による検証
– 統合モデルからソフトウェアアーキテクチャへの変
換
– ソフトウェアアーキテクチャ
+ 実装モデル => 実装
公開シンポジウム
平成13年3月7日
14
形式的オブジェクト指向方法論
通常のオブジェクト指向方法論
非形式的分析モデル(図形+自然言語)
クラスモデル
要求
分析
動的モデル
設計
実装
…モデル
設計・実装段階でのモデル統合
(設計・実装者の頭の中)
平成13年3月7日
公開シンポジウム
15
形式的オブジェクト指向方法論
本形式的方法論
形式的モデル
クラスモデル
要求
分析
動的モデル
実行可能モデル
モデル統合
統合モデル
…モデル
プロトタイプ
実行
一貫性検証
ソフトウェア
アーキテクチャ
決定
ソフトウエア
生成・実装
ソフトウェア
定理証明技術の利用
実装モデル
平成13年3月7日
公開シンポジウム
16
形式的オブジェクト指向方法論（研究成果）
形式的モデルF-Model（関数モデル）
要求
分析
クラスモデル
統合写像
動的モデル
モデル統合
統合モデル
リアクティブシステム
モデルObTS
機能モデル
モデル構築システム F-Developer
（エディター、プロトタイパー、検証系）
プロトタイプ
実行
一貫性検証
ソフトウェア
アーキテクチャ
決定
ソフトウエア
生成・実装
ソフトウェア
スレッドモデルへの変換
不変制約検証公理系
SESモデル
データフロー検証公理系
実装モデル
定理証明系HOLによる実装
平成13年3月7日
公開シンポジウム
17
形式的オブジェクト指向方法論
• オブジェクト指向分析への形式性の導入では最も先進
的
– 分析モデルの統合、不変制約のための公理系
– 分析過程への本格的定理証明技術の利用
• 概念の再利用などが可能な高階論理
– 標準言語UML：制約記述言語OCLによる不変制約記述
– MIT：有限領域についての「軽い」整合性検証
– ＮＡＳＡ、UCI ：完成された状態図
• 一般ソフトウェア技術者が使える段階には、更なら研究が必要
– OCL
=>
SQL
変換
– 分析モデルの実行
• 通常は、分析モデルは実行出来るほど形式性が高くない
• ObTSモデルは、Statechartモデルの最も自然なオブジェクト指向
拡張
– 公開システムとして分析環境を構築
平成13年3月7日
公開シンポジウム
18
統合分析支援環境 F-Developer
Model Builder
1. 形式的分析モデルF-Modelに基づいたモデル構築
Model Builder
2. 構築した分析モデルを、関数型言語処理系SML上で
プロトタイプ実行
F-Prototyper
3. 構築した分析モデルを、定理証明系HOLを用いて検証
F-Verifier
独立なモデル構築
基本クラスモデル
統合写像の入力
基本ステートチャートモデル
平成13年3月7日
公開シンポジウム
19
プロトタイプ実行環境
FPrototyper
1. F-Prototyperでは構築した分析モデルのプロトタイプ実行を
関数型言語処理系SML上で行う。
2. プロトタイプ実行に必要な実行系を自動生成
3. オブジェクトが持つ属性やメソッドの計算をSMLの関数で与える
実行系自動生成器＆
SMLインタプリタ
分析モデルにSMLの関数を割り当て
アニメーションで動作を確認
実行スクリプトエディタで、実行系列を定義
実行系列のソースコードの生
成
平成13年3月7日
(* INSTANTIATE OBJECT*)
Class_IncrementCounter.new
“inc_counter”;
(*INSTANTIATE OBJECT*)
Class_DecrementCounter.new
“database”;
(*ADD LINK *)
RuntimeLib.addLink (“inc_counter”,
“database”);
テスト用スクリプトを作成して、
プロトタイプ実行環境でテスト
公開シンポジウム
20
検証支援環境 F-Verifier
1.構築した分析モデルから公理系を自動生成
2. HOLのデータ型オブジェクトの属性やメソッドを容易に表現
3. Model Builderと連携して、検証に必要な表明群の導入
4. HOLによるインタラクティブプルーフ
HOLによる表現を割り当てる
公理系自動生成器＆
HOLインタプリタ
-対話的な証明を行う。
検証に必要な表明群を導入する
平成13年3月7日
公開シンポジウム
21
リアクティブシステムモデルObTSと実行
環境
• リアクティブシステムモデルObTS、言語
ObCL、実行システムObML
– ObTS ：Statechartモデルのオブジェクト指向化
• 統合モデル＋同期型通信モデル
– ObML ： ML環境上での実行系
– ML環境でのリアクティブシステムの設計とテスト
• 設計・テストスクリプトのMLでの記述
• MLの豊富なデータ構造、高階関数を利用した設計・テス
トスクリプトの構成と再利用
• 他のML-based ツールとの結合： HOL，Design CPN
– 実用規模問題の記述ＩｒＬＡＰ、TCPIP
– 北陸先端大「ソフトウェア設計論」で200名の学生が利用
平成13年3月7日
公開シンポジウム
22
記述対象システムの世界刺激（ボタン押下）
応答（エレベータの移動）
外部環境
（例：エレベータの利用者）
リアクティブシステム
（例：エレベータシステム）
スクリプト化
ランダムイベント列生成
モデル化
オブジェクト(状態遷移図)と
オブジェクト間通信
網羅的イベント列生成
動作解析器
ObTS(ツール)の世界
フィードバック
ObCL
記述
イベント列
生成器
ObCL
コンバータ
動作スクリプト
ObMLコード
動作解析器
動作
結果
シミュレータエンジン
Standard ML
平成13年3月7日
公開シンポジウム
23
解析
結果

Download Report