いわゆる「要求仕様の問題」が発生する1つの側面として、要求仕様の「曖昧さ」がある。開発の指針であるはずの要求仕様が曖昧なため、後続の工程に悪い影響を与え、指針としての役割を果たしていないというものだ。本稿では、要求仕様の曖昧さを回避する方法について述べる。

厳密な要求仕様が要求される背景

 曖昧さを回避する方法を論じる前に、まず要求仕様を厳密にしなければならない背景を説明する。「曖昧ではない厳密な要求仕様書」の記述法といえば、真っ先に取り上げられるのが形式手法だ。しかし、精密な制御が求められるにもかかわらず、形式手法を用いなくてよい開発対象もある。例えば複写機やプリンターなどの機能を1台にまとめた「複合機」もその1つ。複写機は我が国の輸出を支える重要な製品だが、開発において厳密な形式手法で仕様を記述をしているという話を聞いたことがない。複写機は精密な制御を行う製品だが、多少の瑕疵は許されているのかもしれない。

 ただし、例えば複合機を米国防省に納入する場合には、「複合機のIT(情報技術)セキュリティー認証を取りなさい」といった要請がある。こうした要請からくる認証制度はかなり厳格だ。納入物件の種類に応じて取得すべきITセキュリティーの認証レベルが定められており、レベルに応じて遵守すべき要求仕様事項が決められている注1)。といっても商用の複合機ではITセキュリティーを保証する箇所に対して、形式手法の適用は必須とはなっていない(軍事機器は必須であるが)。

注1) 評価保証レベル (EAL:Evaluation Assurance Level)を指す。制度の詳細に関しては情報処理推進機構(IPA)のWebページ(https://www.ipa.go.jp/security/jisec/forusers/abouteal.html)や日立製作所のWebページ(http://www.hitachi.co.jp/Prod/comp/soft1/sec_cert/)などを参照。

 他方、ICカードの「モバイルFeliCa」では、開発において形式手法のVDM(vienna development method)が用いていることが知られている注2)。しかし、こうしたICカード類も、セキュリティー認証の制度で形式手法を用いるのは必須とはなっていない。メーカーの自主的な選択によるものだ。商用とはいえ「財産を扱う」という認識があるからだろう。

注2)モバイルFeliCaの開発にはVDMが採用され、品質評価の報告がある。下記資料はIPAのWebサイト(https://www.ipa.go.jp/)などからダウンロード可能である。
『システム開発への形式手法の適用による品質の確保』(栗田太郎、2010年8月)
『形式手法の基づく高信頼性システム』(荒木啓二郎、2011年7月)

 ところで、形式手法が厳密と言われているのは、形式手法が数理論理学に基づく方法であり、この方法で記述されたものが「最も厳密で確実で論駁しがたい」と信じられているからである注3)

注3)「なぜ数理論理学的な方法が信じるに足るか」という問いがまれに現場から出される。この問いは、三段論法(の形式)を疑う(あるいは採用しない)に等しいということと思われる。

 ICカードの財産管理と同様に、人命を預かる自動車にも厳密な方法の適用が求められている。しかし自動車の安全に関する国際標準規格において、形式手法を用いるのは必須とはなっておらず、「Simulink」などの半形式手法でよいことになっている。

 ただし当然ながら、「自動車の制御に形式手法を用いる必要がない」というわけではない。むしろその効果を期待して、自主的に採用を試みる動きもある。要求仕様の厳密さ、あるいは精度を上げるという傾向は今後大きくなると思われる。