形式手法概論
形式手法関連のリンク集
- ディペンダブル・システムのための形式手法の実践ポータル
- 中島震, 形式手法入門―ロジックによるソフトウェア設計―, オーム社, 2012
- 赤間世紀, 形式手法教科書, I・O BOOKS, 2012
- IPA, 形式手法活用ガイドならびに参考資料, 2012
- ディペンダブル・システムのための形式手法の実践ポータル
- 吉川健, JAXAにおける形式手法に対する取組み ～ソフトウェアIV&Vにおける形式手法の活用事例～, 2012
数理論理学関連のリンク集
Event-B
Event-Bとは以下のような形式手法である。
Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels.
Event-B.org より引用
＜拙訳＞
Event-Bとは、「システムレベルのモデル化と解析のための形式手法」である。Event-Bの特長は「モデル化表記法での集合論利用」、「異なる抽象レベルのシステム表現のためのリファインメントの利用」、「リファインメントレベル間の一貫性の検証のための数学的証明の利用」の３点である。
- Event-B.org
- 中島震, 來間啓伸, Event-B: リファインメント・モデリングに基づく形式手法, 近代科学社, 2015
- 佐藤直人, タイソンホアン, デビッドベイジン, 來間啓伸, Event-Bによる列車監視システムのモニタリング要件の検証, 情報処理学会論文誌, Vol.54, No.6, pp.1738-1750, 2013
Alloy
Alloyとは以下のような形式手法である。
Alloy is an open source language and analyzer for software modeling. It has been used in a wide range of applications, from finding holes in security mechanisms to designing telephone switching networks.
Alloy - Website より引用
＜拙訳＞
Alloyとは、「ソフトウェアのモデル化のためのオープンソースの言語およびアナライザ」であり、「セキュリティホールの発見から電話交換ネットワークまで、幅広く応用」される形式手法である。
Alloyは、形式手法の困難さを克服するために、ある種の制約を仮定する代わりに表現力と自動検証能力を両立した「軽量形式手法（Lightweight Formal Method）」の一種である。Alloyは以下の特徴を有する言語及び開発環境である。なお、Alloyの開発環境は特にAlloy Analyzerと呼ばれる 。
Alloyは「ほとんどのバグは小さな反例を持つ」という小スコープ仮説に基づき、モデルの網羅的全通り検証の代わりに、適切な小スコープを設定して反例の有無を検証する。
- Daniel Jackson(著), 中島震(訳), 今井健男(訳), 酒井政裕(訳), 遠藤侑介 (訳), 片岡欣夫(訳), 抽象によるソフトウェア設計−Alloyではじめる形式手法−, オーム社, 2011
- Alloy - Website
- alloy-4-eclipse
VDM++
The Vienna Development Method (VDM) is one of the longest established model-oriented formal methods for the development of computer-based systems and software. It consists of a group of mathematically well-founded languages and tools for expressing and analyzing system models during early design stages, before expensive implementation commitments are made.
Overture Tool - The Vienna Development Method
＜拙訳＞
Vienna Development Method (VDM) は、コンピュータベースのシステム及びソフトウェアの開発のため、最も古いモデル指向形式手法の1つである。これは数学的にwell-foundedな言語とツールのグループであり、高額な製造契約がなされる前に初期の設計段階でシステムモデルを表現し分析するためのものである。
- VDM++による形式仕様記述
- 石川冬樹, 荒木啓二郎(監修), VDM++による形式仕様記述 (トップエスイーシリーズ 実践講座), 近代科学社, 2011
- VDMTools
- Overture tool
UPPAAL
UPPAALとは以下のような形式手法である。
Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.).
UPPAALより引用
＜拙訳＞
UPPAALは、時間オートマトンのネットワークとしてモデリングされ、データ型により拡張したリアルタイムシステムのモデリング、検証、妥当性確認のための統合開発ツールである。
SPIN
SPINとは以下のような形式手法である。
Spin is a popular open-source software verification tool, used by thousands of people worldwide. The tool can be used for the formal verification of multi-threaded software applications.
SPIN - Websiteより引用
＜拙訳＞
SPINは世界中の人々に使われているポピュラーなOSSの検証ツールである。このツールはマルチスレッドなアプリケーションの形式検証に使われる。