形式手法はバグの少ないソフトウェア開発を行うための数学を基礎とする分野であり、高信頼性が要求される軍事、宇宙航空、社会インフラ関連システムなどで重要視されている手法である。
2009年のSOSP(Symposium on Operating Systems Principles)でオーストラリアのNICTA (National ICT Australia)がOSカーネル(SeL4)の8,700行のコードを形式的検証したことにより話題なった。これはセキュリティ保証要件を規定しているEAL(Evaluation Assurance Level)のLevel6相当の検証を可能にし、今後のソフトウェア開発で形式的検証が使えることを示した。
NICTAは形式的検証の人材確保やベンチャーのOpen Kernel Labsを作るなど活発な活動をしており、今後もその動向に注目。
GEのSmallworldが実装しているロングトランザクション処理の中核技術ではないかと思われる、同一データブロックを共有する重複除外(DeDuplication)技術はメモリとストレージを効率的に利用する環境下では。今後重要度を増すと予想される技術。
メモリ重複除外はすでにVMWware、Xen、KVMなど仮想化ソフトウェアで現時点で利用可能。またトレージではDetaDomainやOcarina Networksのベンチャーが既に存在しており、今後この技術を活用する技術が普及するだろう。既にUSENIX Annual Tech Conf 2005で発表されたSLINKYで重複除外を想定したOS構成法技術が出ている。
忘却型コンピューティング技術は、MITのMartin Rinard教授が提唱するもの。これは2004年のSOSPで発表されFailure Oblivious Computingと呼ばれ大規模な分散処理を可能とする重要な概念であると考えられている。この技術の有効性はエラーを即座に処理せず、処理を中断することなく処理を進めることができ、不正ポインタを利用したセキュリティ攻撃を回避できる。
この概念は Colombia 大学のSoftware Self-healingにも引き継がれている。
注目すべきはSoftware Self-healingを開発していたStelios SidiroglouがMITのMartin Rinard教授の研究室に移籍しているので、忘却型コンピューティング技術の研究開発は更に加速するだろう。
