成功した形式手法導入調査例の分析と発見どのように形式手法は導入されたか? 酒匂寛 Designers Den Corp. 2012/11/15 形式手法の導入 2012, Sako Hiroshi 1

(1)

成功した形式手法導入調査例の

分析と発見

〜

どのように形式手法は導入されたか？

〜

酒匂寛

Designers’ Den Corp.

(2)

自己紹介

• 1980 年代

– 

COBOL とワークステーションの時代

–  汎用機・オフコンを用いた

COBOL 開発

–  ワークステーション上での開発環境の開発

• 1990 年代

–  大規模プロジェクトとオブジェクト指向の時代

– 

2000人月超の大規模プロジェクトをOOで

–  組込み機器のソフトウェアをフレームワーク化

• 2000 年代

–  モデリングと形式手法の時代

–  証券、組込み機器に形式手法を適用

–  領域・課題・仕様・設計・検証のフレームワーク化

2 2012/11/15 形式手法の導入 _{©
2012,

Sako
Hiroshi}

証券業務

_(TradeOne)

FeliCa Firmware

(3)

内容

•  形式手法とは

•  事例ピックアップ

•  事例分析を通して観察された点

•  学習リソース

•  まとめ

(4)

形式手法とは

(5)

形式手法とは？

•  銀の弾丸ではない

•  数学でもない（類似した記法は使う）

•  ただ開発対象をより

厳密に書き留め

、

解析可

能にする

ための単なる「工学的」手法である

•  世界中で少しずつ採用が進んでいる

– 欧州：一番伝統もありリソースもある

– 米国：モデル検査に強みがある

– 日本：世界的成功事例（FeliCa）を擁する

(6)

厳密さのレベル

• レベル１

：離散数学の概念や記法を用いる

• レベル２

：適切なツールの支援と共に形式仕

様記述言語を利用する

• レベル３

：厳密な仕様を検証する

• レベル４

：完全に形式的に開発する（抽象的

な仕様を詳細化して行く）

PETER GORM LARSEN教授 (PGL@IHA.DK) による

2012/11/15 形式手法の導入 _{©
2012,

Sako
Hiroshi} 6

このレベルまでは比較的容易

(7)

形式手法の色々

•  モデルベースアプローチ

_{(VDM,
Z,
B)}

•  代数アプローチ

(Act One, Larch, OBJ)

•  プロセス代数

(CSP, CCS)

•  論理アプローチ

(RTL, TLA)

•  リアクティブアプローチ

(Petri-‐nets, SDL, SAO)

•  複合アプローチ：

eg. RAISE (VDM + CSP) and

LOTOS (Act One + CCS)

今回の話題で取り上げる手法

形式仕様記述を行い検証

(8)

簡単な例：「

N営業日後」の仕様

2012/11/15 形式手法の導入 _{©
2012,

Sako
Hiroshi} ₈

指定した日付（平日）から休日を除いた

N 日後の日付を返す関数の「仕様」は？

public

N営業日後

: 日付 * nat -‐> 日付

N営業日後

(起算日, 日数) ==

is not yet speciﬁed -‐-‐ アルゴリズムは未定

pre

not 休日(起算日) and 日数 > 0

post

let days = 全日付(起算日,

RESULT

) in

card 平日集合 (days) -‐ 1 = 日数;

事後条件に注目。

_RESULT

（関数の戻り値）そのものが式の一部に使われている。

RESULT の

求め方

はここには示されていないが、

RESULT が

どのような性質を満た

(9)

(10)

調査対象事例

組み込み

FeliCa, BPS1000紙幣検査機

航空管制

SHOLIS, iFACTS

金融

TradeOne

言語処理

オランダ軍メッセージ分析

, CAVA

機密情報処理

MULTOS CA, Tokeneer

電子商取引

オランダ花市場

2012/11/15 形式手法の導入 _{©
2012,

Sako
Hiroshi} 10

以下の形式手法導入プロジェクトに関して実担当者にインタビューを行った

(11)

FeliCa ファームウェア (1)

問題領域：

IC カードファームウェア

仕様記述言語：

VDM++

工夫

効果

VDM仕様を開発チームで共有される辞書と

位置づけた

開発対象への共通理

解が得られた

VDM仕様のテスト、品質管理チームによる

テストケースレビューをおこなった

製品の信頼性が非常

に高くなった

VDMのトレーニングとして１週間のコースと

現場での

VDM専門家のコンサルテーション

を受けた

仕様の読み書き

(12)

FeliCa フォアームウェア (1) -‐ プロジェクトの流れ

(13)

FeliCaファームウェア(2)

仕様記述言語: VDM++

工夫

効果

スタイルを操作的記述から関数

的記述へ変更した

可読性の向上

VDM仕様から決定表を導出したテストケース作成時の仕

様の可読性の向上

命名規則により隠蔽関数を区別

した

仕様と設計を分離するこ

とができた

(1)に引き続きVDM専門家のコ

ンサルテーションを受けている

仕様に関する工程の改

善

(14)

FeliCa ファームウェア (2)

2012/11/15

(15)

オランダ軍メッセージ分析

問題領域：オランダ軍メッセージデータマイニング

仕様記述言語：

VDM-‐SL, 自然言語

工夫

効果

定型化された要求記述

仕様とテスト仕様をそれぞ

れ独立して策定

VDM仕様のアニメーション

実行

仕様の実行で得た知見を

使って自然言語で効果的

な顧客レビュー

VDM仕様からのコード自

動生成

仕様記述の工数を確保し

ながら全体の工期を圧縮

(16)

DOD - プロジェクトの流れ

(17)

オランダ軍メッセージ分析：コスト配分

実装

テスト

実装

テスト

分析・設計

伝統的手法

:

VDMTools

®

:

Cost

分析・設計

900 2000

700 1200

500

600 0%

64%

100%

単位は人時

(18)

MULTOS CA

マスターカード認証サーバ

仕様記述言語：

Z記法(+SPARK)、UML、自然言語

ITSEC E6セキュリティ基準(形式的検証済み設計、テスト)

工夫

効果

コンテキスト図、クラス図、構造

化操作定義、英語から

Z仕様を

作成し、

CSP,　SPARKで設計/実

装

従来手法による顧客との対話

と形式手法による仕様記述と

設計、実装を両立

SPARKによりバッファオーバラ

ンや実行時例外等の検証、静

的分析

信頼性の向上

2012/11/15 形式手法の導入 _{©
2012,

Sako
Hiroshi} 18

(19)

(20)

iFACTS

英国航空管制システム

安全性、スケジュール厳守(ロンドンオリンピック)

顧客もZ記法を学習し、開発に参加

読み

書き

人数

75名

11名

職種

開発者、ドメイン専門

家、航空管制官

開発者

コース

3日間

実地訓練

1週間

3ヶ月

2012/11/15 形式手法の導入 _{©
2012,

Sako
Hiroshi} 20

(21)

(22)

Tokeneer

米国国家安全保障庁(NSA)の生体認証システム

仕様記述言語： Z記法(+SPARK)

Common Criteria EAL5(準形式的設計、及びテスト)

工夫

効果

顧客がZ記法を学習し、Z仕様

をレビュー

遠隔地にいる顧客によ

る正確なレビュー

１週間のコース、Z専門家がア

シストしイディオム等の解説

仕様の読み

全ての開発リソースが公開さ

れている

厳密な手法を用いた開

発経験の共有

2012/11/15 形式手法の導入 _{©
2012,

Sako
Hiroshi} 22

(23)

(24)

TradeOne

証券バックオフィスパッケージ

仕様記述言語: VDM++

工夫

効果

ユースケース仕様の回帰テ

スト、仕様を繰り返し改善

システムの信頼性が向上し

た

第二期では日本語の識別子

を採用

仕様の生産性と可読性が

大幅に向上した

ドメインフレームワークの採

用

仕様と設計の追跡性が向

上し、ユースケースの誤り

に素早く対応できた

2012/11/15 形式手法の導入 _{©
2012,

Sako
Hiroshi} 24

(25)

(26)

事例分析を通して観察された点

(27)

成功プロジェクト共通の属性

•  ヒアリング調査の結果から、どのプロジェクトも共通して、厳

密な仕様を、プロジェクト全体から参照される辞書あるいは

情報のハブ

として用いていることが明らかとなった。

•  ヒアリング調査したプロジェクトでは、「厳密な仕様」の取りま

とめに形式手法を用いることにより、検証済の

記述単位と記

述範囲を明確化

することができていた。

•  仕様の一部を、

形式手法以外の表現手段

（日本語による文

章

、

多様な図や表

、

等）

として抽出

することで、議論したりレ

ビューしたりという作業が大幅に容易化されていた。

(28)

要

求

_{妥当性を検証}

仕

様

_{正当性を検証}

設

計

検証

テストケース

システム

テスト

単体・結合

テスト

テストケース

ユーザー

テスト

利用者の確認精度向上

早期の検証によるコスト減

下流工程への精度の高い指示

効果的なテストケース作成

厳密な仕様の位置付け

2012/11/15 形式手法の導入 _{©
2012,

Sako
Hiroshi} 28

(29)

FeliCa フォアームウェア (1) -‐ プロジェクトの流れ

(30)

FeliCa (１)から FeliCa (２)へ

厳密な仕様記述の改善例

考察：ラベル付き条件によるレビュー容易性の評価

cases false : (パケットサイズ十分？("サービス数”)), (サービス数範囲内？ (cmd_pkt, cmnd_pkt_st))) -> <ERROR_NO_RESPONSE>, others -> <SUCCESS> end; -- パケットの長さがサービス数まで存在する十分なパケットであること packet_len_of_service_num >= 9 and -- パケットにおいて指定されたサービス数が規定の範囲内であること

1 <= service_num and service_num <= 32

private サービス数範囲内？ : PACKET_DATA * PACKET_STRUCTURE -> bool

サービス数範囲内？(cmnd_pkt, cmnd_pkt_st) == let

CmndPkt = パケット要素取得(cmnd_pkt, cmnd_pkt_st), num = hd CmndPkt(“サービス数")

in

1 <= num and num <= 32;

ラベル付き条件を用いない場合ラベル付き条件を用いた場合

左上の「ラベル付き条件を用

いない場合」は

_{FeliCa(1)
の}

記述方式の一部である。日

本語による注釈が読みやす

さの向上のために添えられ

ていた。

FeliCa(2) では更に読みやす

さを向上させることを狙い、

左下の「ラベル付き条件を用

いた場合」のような工夫を

行った。

述語に日本語識別子を用い

たり、記述形式を工夫したり

することによって、レビューの

しやすさを向上させた。

2012/11/15 形式手法の導入 _{©
2012,

Sako
Hiroshi} 30

(31)

FeliCa (２)

形式仕様からのテストケース導出

「ラベル付き条件」の形式で

書かれた仕様から、体系的

に左のようなデシジョンテー

ブルを抽出し、テストケース

を設計できるような仕掛けを

考えた。

レビューがしやすくなり、機械

的なテストケースのチェック

ツールも用意された。

ディシジョンテーブルの活用

条件 同値分割 境界値 TC1 TC2 TC3 TC4 実行可能モード？ TRUE 0..2 Y Y Y FALSE 3 Y パケットサイズ十分？ TRUE 10 Y Y Y FALSE 9 Y サービス数範囲内？ TRUE 1..32 Y Y N FALSE 0, 33 N Y 結果正常応答 Y 応答なしエラー Y 応答ありエラー Y Y

テストケースの網羅性を視覚的に確認する

ことができる

。

レビューが容易になる

。

(32)

形式仕様の適用箇所

• 形式手法はどの段階にも適用可能

o 

仕様、設計、実装、検証のどの段階でも利用されている

o 

成功したプロジェクトは皆、形式記述がその前後の段階

や成果物とどのように対応しているかが明確にされてい

る

• 特定の特性全域を記述

o 

成功したプロジェクトはプロジェクト内で着目したある特性

に関しては全面的に選んだ形式記述を適用している

o 

複数の作業者が協調するためには必須

2012/11/15 形式手法の導入 _{©
2012,

Sako
Hiroshi} 32

(33)

自然言語(日本語)記述との共存

• 開発チーム内での扱い

o 

形式記述と非形式記述（自然言語による説明や図など）

を併記・併用することにより、読み易さと厳密さを共存さ

せることができる

o 

両者の間の食い違いを取り除き易いように適度な粒度

（例えば１ページ程度）の単位で構成する

• 開発チームと外部との関係での扱い

o 

外部を形式手法の読み手として訓練する方法

o 

外部を形式手法の読み手としては訓練せず、形式手法

を使う技術者が様々な形に変換して外部に提示する方

(34)

調査事例における「顧客」との対話手段

形式仕様を利用

形式仕様を利用せず

国内

（

_{*FeliCa
は
API
文書を形}

式仕様から半自動生成）

FeliCa(1)

FeliCa(2)

TradeOne

海外

iFACTS

Tokeneer

SHOLIS

オランダ軍メッセージ分析

MULTOS CA

BPS1000

CAVA

オランダ花市場

2012/11/15 形式手法の導入 _{©
2012,

Sako
Hiroshi} 34

このプロジェクトを受託した

Altran Praxsis という会社は、顧客との契約も形

式仕様の項目ベースで行い、問題が生じたときにそれがどちらの責任か

が逐一明確になるようになっている

(35)

iFacts:テストケースの記述

自然言語

+ 形式記述

(36)

厳密な仕様策定手順の一例

•  要求記述の内容のうち、問題領域自身の性質（システムが変える

ことのできない部分）と、構築対象（システムが影響を及ぼす部分）

への記述を区別する（

à

領域資産化）

•  要求記述を読み、用語を切り出す

•  クラスもしくは型と、関数もしくは操作の候補を見つける

•  クラスの構造（型、属性、関連）に関する概略を書く

•  関数／操作に関する概略を書く（シグニチャを決める）

•  要求記述から不変な性質を抽出して定義する

•  事前条件、事後条件もしくは定義本体を記入することによって、関

数／操作定義を完成させる、必要ならば型定義を変更する

•  作成された仕様のモデルが利用者の期待や、要求中に現れる項

目や制約を満たしているかどうかをアニメーション等を通して検証

する

•  以上のステップを必要なだけ繰り返す

2012/11/15 形式手法の導入 _{©
2012,

Sako
Hiroshi} 36

(37)

「問題領域」の語彙の充実

厳密さ

((

機械処理

、

テスト可能

))

貸出機能

_{:
図書館型 * 書籍型 * 利用者型}

-‐> 図書館型

貸出機能

_{(lib,
book,
user)
==}

is not yet speciﬁed

pre

book in set dom lib.登録書籍

-‐-‐ 書籍が登録書籍であること

_{and
user
in
set
lib.登録利用者}

-‐-‐ 利用者が登録利用者であること

_{and
書籍貸出可能数(lib,
book)
>
0}

-‐-‐ 書籍に貸し出し用の余裕があること

_{and
(user
in
set
dom
lib.貸出中 and
(card
lib.貸出}

中

_{(user)
<
3))}

-‐-‐ 利用者の利用制限冊数を超えていないこと

_post

-‐-‐ 指定された書籍が「貸出中」に登録されてい

る

_{(user
in
set
dom
RESULT.貸出中)
and
(book
in
set}

厳密さ＋読み易さ

貸出機能

_{:
図書館型 * 書籍型 * 利用者型}

-‐> 図書館型

貸出機能

_{(lib,
book,
user)
==}

is not yet speciﬁed

pre

登録済み書籍(lib, book)

and 登録済み利用者(lib, user)

and 貸出可能書籍(lib, book)

and 利用者貸出制限数内(lib, user)

post

書籍貸出中(RESULT, book, user);

問題領域の語彙を充実させることに

よって仕様の見通しが良くなる。

(38)

既存資産の進化例

Level 0

現状

Level 1

現状記述

Level 2

現状改善

Level 3

次世代準備

（既存の仕様書）階層構造を持つ機種共通部分と独自部分に分かれる（仕様の回帰テストにより）既存の日本語仕様書との一致を保証済み全体像を把握しやすい仕様の十分な抽象化検索性の向上ある関心に特化した閲覧性がある日本語仕様書 Ver. A 日本語仕様書 Ver. A 日本語仕様書 Ver. B 形式仕様書 Ver. X 形式仕様書 Ver. Y 日本語仕様書 Ver. C 形式仕様書 Ver. Z 日本語仕様書との対応が明確で読みやすい記述リファクタリングフィードバック 2012/11/15 形式手法の導入 _{©
2012,

Sako
Hiroshi} 38

(39)

階層記述の例

記述階層名

記述目的

記述例

検証シナリオ階層

仕様アニメーションを行うための

検証シナリオ（テストケースなど）を

定義した階層

(例えば非接触ICカードの場合)

個別コマンド検証シナリオなど

機能仕様階層

特定の応用に対する機能仕様を

定義する階層

カード操作コマンド仕様など

問題領域データ階層

問題領域に特有の共通データ等

を定義した階層

具体的なファイル構造など

問題領域階層

共通問題領域で繰り返し利用さ

れる関数や不変条件などを定義す

る階層

カードファイルシステム、データパケッ

トの変換など

共通領域階層

特定の問題領域に依存しない階

層。ネットワーク（数学的な意味で）

や、組合せアルゴリズム、文字列

や数値に関する共通処理などがこ

こで記述される

階層型データ処理など

(40)

学習リソース

(41)

利用できる様々なリソース

•  様々な実践ノ

ウハウの提供

•  実践ノウハウ

の共有

•  VDM, B, SPIN,

etc …

•  基本的な情報

書籍

ツール

コンサ

ルタン

ト

コミュニ

ティ

VDM研究会

SEA SIGFM

FM Europe

(42)

バートランド・メイヤー氏による、「オブジェクト指向の原理とモデル」を徹底的に考察

した入門書。「契約による設計」に関する解説もオリジナル故にしっかりとしている。

契約による設計

形式仕様記述で用いられる事前条件、事後条件、

不変条件などについて、日本語で詳しく説明された

書籍の代表。

ソフトウェア工学の学習書籍としても読み応えあり。

(43)

要求と仕様の大切さ

ソフトウェア要求と仕様　

_{―　実践、原理、偏見の辞典}

マイケル

ジャクソン

_(著),

玉井

哲雄

_(訳),

酒匂

寛

_(訳)

本体価格：

_\3,570

単行本

_{:
267
p
;
サイズ(cm):
21
x
15}

出版社

_{:
新紀元社
;
ISBN:
4775302876
;
(2004/04)}

ソフトウェア開発を「記述」の体系として捉え

、

そ

れにまつわる様々な話題を取り扱った本

(44)

形式仕様記述

ソフトウェア開発のモデル化技法

岩波書店

VDM-‐SL の教科書。形式仕様を用いたモデル

化の基本を解説

(45)

形式仕様記述

VDM++によるオブジェ

クト指向システムの高品

質設計と検証（翔泳社）

ジョン・フィッツジェラルド、ピー

ター・ゴルム・ラーセン、ポール・

マッカージー、ニコ・プラット、マー

セル・バーホフ

(著), 酒匂寛 (翻訳)

VDM++を用いて、形式モ

デリングの基礎と応用を学

習します。他の形式手法に

も応用可能。

(46)

モデル検査

SPINモデル検査―検証モ

デリング技法

中島震

近代科学社

2008年

モデル検査ツール

SPIN を用いたモデル

検査入門書

(47)

(48)

形式仕様導入のための留意点

•  厳密な仕様記述をプロジェクト情報のハブとする

–  常に頼れる検証済みの情報の起点として利用できるようにす

ることが必要

–  記述対象を選んだらそれに関しては完全に記述する

•  複数の手法を組み合わせる

–  仕様記述以外にも適切な手法を組み合わせることにより、厳密

な仕様記述の効果が増加する

•  適切なツールを選択/調整/作成する

–  単体のツールだけではなく、必要に応じた組合せが必要

–  形式的記述を核に形式的ではない記述との相互変換を行う

•  積極的な事例開示を行う

–  積極的な事例開示によって皆の知恵を集めやすい土壌を作る

(49)

形式手法とは

•  銀の弾丸ではない

•  数学でもない（類似した記法は使う）

•  ただ開発対象をより厳密に書き留め、解析可

能にするための単なる「工学的」手法である

•  世界中で少しずつ採用が進んでいる

– 欧州：一番伝統もありリソースもある

– 米国：モデル検査に強みがある

– 日本：世界的成功事例（FeliCa）を擁する

再掲

(50)

明日から始めるには？

•  現状の棚卸をする

–  プロセスとドキュメントを整理する

•  形式仕様、形式手法適用が相応しい部分

/対象

を選ぶ

–  いくつか候補を選び、記述を用いたプロセスを試行す

る。同時にコアメンバーを訓練する

•  可能ならば「新しいプロジェクト」の上流から適用

してみる

–  コンサルタントのアドバイスとレビューが初期にはとて

成功した形式手法導入調査例の 分析と発見 どのように形式手法は導入されたか? 酒匂寛 Designers Den Corp. 2012/11/15 形式手法の導入 2012, Sako Hiroshi 1