バグを出さないシステムは完璧な仕様書から - CSKシステムズ

CSKシステムズは、形式的手法を用いてシステムの仕様を記述するための言語「VDM」(Vienna Development Method)に関する展示を行った。

動画6(WMV形式)

仕様にはない想定外の入力の組み合わせにより、システムに重大な障害を与えるという例はさまざまな分野で多く見られる。それが航空宇宙、自動車、金融など、ちょっとしたシステムの障害であっても重大な事故に繋がるような分野では、開発にはとくに慎重にならなければならない。

しかし最近のマルチコアCPU環境など、複数のコンピュータが連動するような分野では、入力の組み合わせだけでも膨大な数になり、すべての組み合わせを検証することは人間の手作業だけでは無理である。こういった問題を解決するのが「形式的手法」(Formal Methods)である。これは、システムの仕様に破綻がないことをを数学(論理学)的に検証する手法である。爆撃機の制御システムや、ロシアの衛星制御システムなど、きわめて高い信頼性が要求される分野では、以前から採用されている。

この形式的手法によるシステム設計の導入を支援しているのが、CSKシステムズである。形式的手法を導入する場合、具体的には仕様記述言語と呼ばれる言語を利用して、システムの仕様を記述し検証することになる。仕様記述言語は現在100種類以上存在するというが、同社では「VDM」(Vienna Development Method)を推薦している。担当者によると、その理由としては、ツールが整備されていることと、日本語によるドキュメントが存在することが挙げられるという。同社では学習に時間がかかるという形式的手法をスムーズに導入できるよう、VDMの学習セミナやシステム設計のコンサルティングを行っており、3日間でVDMの読み書きが可能になるというセミナも用意している。

同社は証券バックオフィスシステムなどで導入実績をもち、このシステムのリリース後の欠陥は事実上ゼロだという。同社では複数のECUの制御を行う自動車分野など、マルチコア環境の増加が予想される組み込み分野での採用を見込んでいるという。