Tokeneer

4.9.7 顧客とのコミュニケーション

顧客とのコミュニケーションはまずは英語による要求獲得が行われ、自然言語やプロトタ イプによるレビューが行われた。

4.9.8 開発者間のコミュニケーション

機能面に関しては Z 記法による仕様および CSP によるプロセス設計を参照して、Ada お

よび SPARK のパッケージ仕様が作成され、そこから実装コードが作成された。英語によ

る要求定義から実装コードまで完全な追跡性が確保された。

4.9.9 教育

このプロジェクトの教育的側面については公表されていない。

開発主体となった英国Praxis社は形式手法による開発に実績があり、また、既にセキュリ ティクリティカルな高信頼性情報システムの開発経験があった。開発は新手法の導入では なく、Praxis 社が発展させてきた数々の高信頼性ソフトウェア開発プロセスと開発技術が 適用された。

開発は顧客側のドメイン専門家や社外技術者も形式手法の教育を受け、遠隔地に分散し開 発者側の形式手法専門家の助けを受けながら、形式仕様を直接レビューした。開発は大別 してカーネル部分と周辺部分に分けられ、カーネル部分は英国にて証明を含む構成的正当 性(Correctness by Construction)が適用され、周辺部分は米国ニューメキシコ州にて、通常 のソフトウェア工学的手法で開発された。本報告では、カーネル部分の開発を対象とする。

システム開発は3名の技術者によりパートタイムで合計260人日で遂行された（参考文献 7 より）。独立したシステム信頼性検査においても、また、出荷後においても、開発され たシステムに誤りは発見されていない。

プロジェクト終了後、成果物も含め全開発文書がインターネット上で一般に公開されてい る。本プロジェクトの目的はセキュリティ基準の達成だが、セキュリティ基準適合に限ら ず形式手法による信頼性の高いソフトウェア開発についての成功事例としての価値は非常 に高いと考えられる。

4.10.3 開発プロセス概要

このプロジェクトは、高いセキュリティ基準から要請される構成的正当性(Correctness by

Construction)と呼ばれる詳細化と証明を基盤とする形式手法を用いて実際にセキュリティ

クリティカルな高信頼性システムをスクラッチから開発するための参照となるべき開発と して開始された。既に形式手法に熟達し実績のある専門家がおり、その形式手法による開 発経験を生かして開発を進めつつ、顧客への形式手法の教育を提供し開発プロセスに受け 入れて開発を遂行した。

開発プロセスの原則として、下記の項目を掲げた（具体的な記述は参考文献7を参照）。

• 正しい記述：必要な情報を混乱や曖昧や煩雑さなく記述する

• 飛躍なき進行：開発の各作業は小さなステップで進める。大きなステップは 誤りを生み、また、誤り発見を困難にする。

• 単一の記述：未だ記述されていない情報やデザインデシジョンを、明確な目 的とともに文書化する。同じ情報の繰り返しは不必要な作業を生み、本当の デザインデシジョンを不明にする。

• 確認してからの実行：各記述は可能な限り早急に検証する。それまでの記述 と突き合わせてレビューすることで検証を容易にし、簡明な記述を得る。

• 論証の記述：デザインデシジョンの根拠とそれが正しいと考える理由を文書 化する。理由付けは後の分析に役立ち、誤り発見につながる。

• 正しい道具：検証したい特性に最も適した方法で検証する。方法には公式レ ビュー、非公式ピアレビュー、証明、検査などが含まれる。

• 頭脳：作業全てについて頭を働かせる。顧客とのレビューでの注意深さ、矛

の思慮深さと文書化での注意深さを持つ。

開発プロセスをデータフローダイアグラムとして記述したものを下図に示す。

図4-15: 開発プロセス概要[HS10]

4.10.4 記述と支援ツール

このプロジェクトで形式手法に関連して用いられた主な言語と主なツールを以下に挙げる。

表4-17: 使用された言語と主なツール

Z記法 SPARK

ファイル形式 LaTeX ソース

構文/型検査 fuzz SPARK toolset

静的検証(証明等) - SPARK toolset 動的検証(テスト等) - SPARK実行時検査

自動生成 - -

4.10.5 厳密な仕様記述の効果

(1) セキュリティ基準の達成

構成的正当性(Correctness by Construction)により情報セキュリティ国際標準(Common

Criteria, CC) EAL5に適合する高信頼システム開発が可能であることを実証した。

(2) 遠隔地の顧客側レビュー

Z 記法で記述された仕様に対するレビューを米国メリーランド州にいる Z 記法の専門家と 米国ニューメキシコ州にいるドメイン専門家の間で、電話によるレビューセッションを行 い、生産的な結果を得ることができた。これは、Z 記法の基本的な読解スキルを身につけ ることで同一の仕様記述について解釈の曖昧性なしに複数人で討議することができたこと を意味する。

4.10.6 厳密な仕様記述を適用するための工夫と効果

(1) 顧客数名と開発者1名のチームによるレビュー

ドメイン知識豊富な顧客側スタッフがZ記法の専門家による補足説明を受けながらZ記法 による仕様記述を直接レビューすることができた。

(2) 構成的正当性による堅実な開発

前述の開発プロセス概要で示した通り、開発者は形式手法による高信頼性ソフトウェアの 開発を数多く手がけており、そこで得られた教訓から開発プロセスで守るべき原則を掲げ た。

4.10.7 顧客とのコミュニケーション

顧客から英語による要求を獲得した後、開発側が英語による要求を Z 記法による仕様記述 として策定した。Z 記法による仕様記述は顧客のレビューを受けた。レビューでは Z 記法 専門家が顧客のアシスタントを努めることで、1 週間程度の教育コースを受けただけの基 礎的な読解を持つ顧客側ドメイン専門家もイディオム等を恐れずにレビューすることがで きた。

設計に関しては顧客による詳細なレビューは必要なかった。設計は Z 記法による仕様と同 様の構成をしており、対応する項目間の比較は容易だった。

4.10.8 開発者間のコミュニケーション

各工程でそれぞれの詳細度での記述が行われたが、前工程での記述の構造を大きく変える ことなく、必要な詳細の追加をひとつひとつ理由や根拠を示しながら記述を重ねていった。

これによって、前工程と後工程の間の関係を把握することが容易になり、後工程が前工程 の正当な詳細化であることを検証するのに役立った。

4.10.9 教育

顧客側のドメイン専門家が1週間のZ記法の教育コースを受けた。その後、Z記法の専門

客レビューを効果的に実施することができた。