IPAが公開した形式手法の調査報告書

IPAが形式手法の調査報告書を公開していたのでメモ。

【元ネタ】
「形式手法適用調査」報告書～情報処理推進機構：ソフトウェアエンジニアリング

形式手法は理論としては古いけれども、実際の開発でどこまで使えるのか、正直分からない。
でも、日本ではFelicaの開発で成功した事例がある。
海外では、フランスの地下鉄や、航空宇宙、軍需産業、医療機器などで事例があるらしい。

形式手法が密かなブームになっている理由は、高信頼性を要求される組込ソフトウェアの開発で形式手法を使って、設計の早い段階で品質を担保したいからだろう。
並列性、排他制御、フェールセーフなどの非機能要件を設計段階で、抽象的な仕様でシミュレーションしてバグ出ししたいのだろう。

つまり、日本のIT業界を主導するIPAとしては、製造業を補完する組込ソフトウェア開発の生産性Upや信頼性Upに形式手法を取り入れたいのだろうと思う。

IPAが公開する調査報告書は、詳細に書かれていて、最近のIT技術の動向を知る上で非常に参考になる。
ウォッチしていると良いかもしれない。

Rails検証報告書: プログラマの思索

IPAが書いたアジャイル開発の研究会報告書: プログラマの思索

IPAが公開したRubyやRails教育プログラム: プログラマの思索