Zenn
📝

形式手法のまとめ

2016/02/28に公開
形式手法
alloyanalyzer
eventb
vdm
uppaall
tech

形式手法概論

形式手法関連のリンク集

数理論理学関連のリンク集

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の特長は「モデル化表記法での集合論利用」、「異なる抽象レベルのシステム表現のためのリファインメントの利用」、「リファインメントレベル間の一貫性の検証のための数学的証明の利用」の３点である。

詳細な記事はこちら

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は「ほとんどのバグは小さな反例を持つ」という小スコープ仮説に基づき、モデルの網羅的全通り検証の代わりに、適切な小スコープを設定して反例の有無を検証する。

詳細な記事はこちら

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な言語とツールのグループであり、高額な製造契約がなされる前に初期の設計段階でシステムモデルを表現し分析するためのものである。

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の検証ツールである。このツールはマルチスレッドなアプリケーションの形式検証に使われる。

Discussion