有効性が唱えられて久しくも、なかなか大輪の花を咲かせなかった形式手法。90年代後半から適用例が増えた欧州に比べ国内ではその導入が今一歩進んでいなかった。しかし現在、分散システムの開発のニーズの増加から日本でも形式手法の普及が広まる機運が高まっている。
形式手法がないと乗り切れない!?
形式手法が導入されてこなかった理由の一つとして、形式手法に頼らなくても要求品質をほぼ満足することが出来ていたという事情がある。レビューやテストを徹底すれば設計ミスをカバーできるという状況ならば、せっかく蓄積してきたノウハウを捨ててまで導入するという選択肢が積極的に取られることはない。
その反面、形式手法が無ければ達成できない大きな壁が現れれば導入が一気に進む可能性がある。その大きな壁となりうるものとして挙げられるのが、CPSやスマートシティといったセンサネットワークで実現されるM2M型システムである。これらのシステムはその相互連携の仕組みの複雑さから従来の検証方法ではコスト高になりすぎる。そこで網羅的に検証できる形式手法適用の恰好の対象として欧米中心に研究が進められてきた。
日本でもスマートシティ関連IT市場の急速な拡大が予測されるなどM2M型システムに対する技術ニーズが高まっており、大学・研究機関だけでなく企業でも積極的に形式手法を用いた開発が行われるなど技術開発の裾野が広がっている。最近では、中小企業庁の事業支援対象に形式手法による組込みセキュリティ技術の開発案件(株式会社ヴィッツが主体となり実施)が採択されたことが例として挙げられる。
導入を支援する環境の整備
ニーズの高まりだけでなく、適用を支援する環境が整備されてきたことも普及を後押しする原動力となっている。
今年4月、「ディペンダブル・ソフトウェア・フォーラム(DSF)」が、形式手法の適用実験を行い当団体の作るガイドの有効性を実証した。これは東京証券取引所のシステムの設計書を対象に行われたものであり、組込み系と比べ実例の不足していたエンタプライズ系での有効性を確認した意義は非常に大きい。
また近年技術者の教育環境も整備されてきており、特に社会人向けの教育環境が充実してきている。国立情報学研究所のTOPSEプログラムや、IPA/SECによる形式手法導入セミナーなどがその例だ。
形式手法導入のこれから
上記のように開発ニーズの高まり、導入支援環境の整備といった明るい材料が揃いつつあるが、日本国内での形式手法普及がうまくいくにはまだまだ超えるべき峠が有る。
特に必要だと思われるのが、形式手法適用の制度化だ。一部案件で形式手法が必須であってもまだまだ大半の開発案件は従来手法を徹底すれば十分であり、組織の経済活動を維持できるという企業がほとんどだと思われる。このような状況下では、一時的にしろコスト増となる技術導入はなかなか進まない。ユーザ・ベンダ双方の導入コストが無駄にならないよう、足並みを揃えて段階的に移行できるよう社会制度として支援することが必要だと思われる。
また、機能安全の国際規格ISO26262やIEC61508等の例のようにエンタプライズ系システムにおいても信頼性レベルに応じて形式手法の導入を推奨する制度の策定が望まれるほか、調達要件に用いることのできるような形式手法に関する資格の創設なども期待される。
このような環境を整備しなければ、形式手法を用いた開発の妥当な対価の算定や形式手法導入の戦略的判断はできないのではないだろうか。地道に導入を進めてきた欧州と比べると、日本はやや急激な変化であることが心配だ。ユーザ・ベンダの自助努力では補えない部分は社会制度によるサポートが必要だ。