FM2014参加報告

摘要

形式手法(Formal Methods)とは，数理論理学に基づき効率よく高信頼なソフトウェアを構築するためのアプローチの総称である.形式手法においては.文法と意味論が厳密に定められた言語による仕様や設計の記述や，それらあるいは実装コードに対する強力な検証を扱う.以下に挙げるような手法·ツールがよく知られており，コンピュータソフトウェア誌にも多くの解説がある(など).1. 汎用性の高い言語でモデル記述を行い様々な方法で検証を行うVDM.Event-B,CafeObj,Alloyなどの形式仕様記述手法やその支援ツール2. 状態遷移の網羅的な検証を行うSPIN, SMV, UPPAALなどのモデル検査ツール3. 定理証明による検証を行うIsabelleやCoqなどの証明ツール国内でも近年多数書籍が出ており，産業界でのICチップなどの適用事例発表,ガイドラインなどの提供を通し，よく知られるようになってきている.本稿では形式手法に関する国際会議FM2014の参加報告を行う.招待講演·特別講演について紹介するほか，国内での知名度が高いVDMに基づく， 2つの発展プロジェクト(COMPASS, DESTECS)に関する情報も紹介する.