SHOLIS

SL 専門家から 1 週間のコースを受け、その後、その VDM-SL専門家のコンサルテーショ ンを受けた。

1995 年当時としては非常に挑戦的なプロジェクトであり、開発プロセスに関してもシン プルな構成で工夫をし、形式手法の効果的な応用を切り拓いたプロジェクトである。

4.4.3 開発プロセス概要

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

図4-8: 開発プロセスの全体像[HS04]

ユーザからの要求(図中ではUser Requirements)が英語で仕様策定者に伝えられ、Z記法お よびその補足説明となる英語による仕様(図中では Software Requirements Specification, SRS)が記述された。仕様は、同じく Z 記法で記述された安全項目に対して証明による検 証が行われた。約130個の証明がZ記法による仕様記述に対して行われた。

Z記法による詳細化の技術によって、Z記法での設計を派生し、更にSPARKでpre, post, assert, returnといった論理的表明や、global, derives, own, inheritといった情報のフロー に関する表明の注釈記述を伴う設計を派生させた。詳細化の各ステップや、Z 記法による

設計から SPARK による設計への派生に関する正当性の証明が行われた。Z 記法による設

計に対しては約20の証明が行われ、SPARK による設計に対しては、3,100 個の機能要件 や安全要件に関する証明が行われた（参考文献 4 より）。また、SPARK の実装に関して も、スタックサイズや入出力帯域、ループ停止条件が静的分析により検証された。

Z記法およびSPARKに関する証明はピアレビューの対象となった。また、SPARKの実装 に関する証明は、ピアレビューに加えて、開発社内の別チームによるレビューを受けた。

従来手法と同様の単体テストおよび結合テストも行われ、全工程のうち約 37%の工数が当 てられた。テストにより、証明や静的分析では検出できなかった誤りを検出し、最終的に は安全性を確保して実行時検査を取り除き、出荷した。

4.4.4 記述と支援ツール

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

表4-8: 形式手法に関して利用された言語と主なツール

Z記法 SPARK

ファイル形式 LaTeXファイル ソースファイル 構文/型検査 Fuzz SPARK toolset 静的検証(証明等) HOL/Z SPARK toolset 動的検証(テスト等) - SPARK実行時検査

自動生成 - 証明課題

4.4.5 厳密な仕様記述の効果

(1) 高品質

Z記法の仕様記述により主要な安全項目を満たすことが検証され、また、SPARKによる設 計および実装が Z 記法による仕様記述を満たすことも証明および静的解析により検証され た。これにより、Def Stan 00-55（英国国防省の安全規格）およびそのSIL4⁷で要求される 高い安全基準を満たすことができた。

(2) 誤りの早期発見(1)

Z 記法による仕様記述は型検査器にかけられ、記述者によって誤りの早期発見が行われた。

データや機能や操作に関する型の矛盾を早期に発見することで、仕様記述の基本的な整合 性を確保することができた。

7 Security Integrity Level 4

(3) 誤りの早期発見(2)

Z 記法による仕様記述に関する証明によって、重大な誤りを早期に発見することができた。

下に各工程における誤りの発見に関するデータを引用する。

図4-9: 誤りの発見に関するデータ(参考文献4より引用)

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

(1) 異なる言語間での追跡性の確保

仕様記述と設計で異なる言語を用いたために、異なる言語間での追跡性を確保する必要が あった。また、仕様記述言語と設計／実装言語では使用できるデータ型が異なっているた めに、そのギャップを埋める必要があった（参考文献4より）。

追跡性を確保するため、仕様記述で用いられた Z 記法上の識別子と設計および実装で用い

られた SPARK 上の識別子をできる限り統一させた。双方の言語の間で同じ変数について

異なる型が用いられた場合には、SPARK 上での表明としてその制約条件が記述され、ほ とんど誤り混入の元とはならなかった（参考文献4より）。

(2) 検証コストの低減(1)

システム全体が安全基準SIL4の対象であったのではなく、SIL4対象部分と非SIL4部分が あった。そこでSIL4準拠部分と非SIL4部分を機能的に分離し、静的検証によって分離を 検証することで、機能要求に関する検証をSIL4部分に対してのみ行った。

(3) 検証コストの低減(2)

型検査を Z記法の仕様および SPARK による設計全てに対して行うことで記述時の誤り発 見に大きな効果を得た一方で、仕様記述および設計に対する検証項目をキーとなる安全項 目に絞った。

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

顧客と開発者の間では自然言語が用いられた。顧客はシステムが満たすべき仕様および安 全要件を自然言語で示し、開発者はそれらを Z 記法で記述し、Z 記法で仕様が主要な安全 要件を満たすことを検証した。ここで開発者は仕様に関する証明を行うことでドメインお よびシステムについてより深い理解ができ、それを顧客とのコミュニケーションに役立て ることができた。

4.4.8 開発者内でのコミュニケーション

Z 記法による仕様記述から SPARK による実装まで異なる詳細化レベルでの記述があり、

開発者はその作業工程に応じた詳細度での記述を参照した。

4.4.9 教育

仕様記述および証明を行ったのは、プロジェクト開始時には既に形式手法に熟達した技術 者だった。実装者に対して 1 週間の形式手法のコースを受講させ、形式的記述の読み方の 教育を行い、現場での指導を行った。