形式手法
形式手法（Formal Methods）は、ソフトウェア工学において、数学的な理論を基盤としたソフトウェアおよびハードウェアシステムの仕様記述、開発、検証を行うための技術です。この手法は、他の工学分野と同様に、適切な数学的解析を用いることで設計の信頼性と頑健性を高めるという考えに基づいています。形式手法は、理論[[計算機科学]]の様々な成果を応用しており、特に数理[[論理学]]、形式言語、オートマタ理論、プログラム意味論、型システム、代数的データ型などの概念を活用して、システムの仕様を記述し、その正当性を検証します。
形式手法は、その適用レベルに応じて以下の3つの水準に分類されます。
水準0: 軽い形式手法
このレベルでは、形式的な仕様記述を行いながらも、プログラム自体の開発は非形式的に進めます。このアプローチは「軽い形式手法」とも呼ばれ、比較的少ない労力で効果を上げることができるため、費用対効果を重視する場合に適しています。
水準1: 形式的な開発と検証
このレベルでは、形式手法をより深く活用し、開発と検証の両方を形式的に行います。例えば、仕様記述からプログラムを作成する際に、詳細化と属性の証明を厳密に行います。このアプローチは、高信頼性が求められるシステムに適しています。
水準2: 自動定理証明による完全な検証
このレベルでは、自動定理証明を用いて、システムの検証を完全に機械的に行います。このアプローチは非常に厳密ですが、導入には高度な専門知識と多大なコストがかかるため、特に重要なシステム（例えばマイクロプロセッサの設計の中核部分）など、エラーが大きな損失につながる場合に限定して適用されます。
また、プログラム意味論に基づいた分類として、形式手法は以下の3つの主要なアプローチに大別されます。
表示的意味論
このアプローチでは、システムの意味を領域理論を用いて表現します。システムの挙動を数学的な関数として捉え、領域理論の性質を通じてその意味を解析します。しかし、すべてのシステムが関数として直感的に表現できるわけではないという課題があります。
操作的意味論
このアプローチでは、より単純な計算モデルを用いて、システムがどのように動作するかを表現します。システムの意味を、計算モデルの一連の動作として捉え、その単純さによって表現を明確にしようとします。しかし、使用する計算モデルの意味論をどのように定義するかという問題が残ります。
公理的意味論
このアプローチでは、システムがある処理を行う前後の状態に着目し、その状態変化によってシステムの意味を表現します。古典的な論理学との関連が深く、システムの動作を事前条件と事後条件で記述します。しかし、事前状態と事後状態を示すだけで、システムが実際に行う処理を完全に表現できるかという疑問も指摘されています。
軽量形式手法（Lightweight Formal Methods）
一部の開発者からは、形式手法が過度に完全な形式化を重視しすぎているという意見があります。システムの複雑さや使用する言語の表現能力の限界から、完全な形式化が困難になる場合もあります。そのため、部分的な仕様記述や特定の応用に焦点を当てた軽量形式手法が提案されています。例えば、型システム、Uppaal、Alloy、Z言語を用いたユースケース駆動開発、CSK VDMツールセットなどが挙げられます。
形式手法は、ソフトウェア開発の様々な段階で利用できます。
仕様記述
形式手法は、開発対象システムの仕様を任意のレベルで記述するために利用できます。形式的な記述は、その後の開発活動のガイドとなるだけでなく、開発されたシステムの機能が要求通りであるかを検証するためにも用いられます。ジョン・バッカスが提案したプログラミング言語の文法を記述するBNF記法のように、形式仕様記述の必要性は早くから認識されてきました。
開発
形式仕様記述に基づいて、システムの設計を行い、実際の開発（ソフトウェアやハードウェアの実装）を行います。例えば、操作的意味論に基づく形式仕様記述では、実際のシステムの動作と仕様上の動作を比較したり、一部ツールでは仕様記述から自動的にコードを生成したりします。一方、公理的意味論に基づく形式仕様記述では、仕様に記述された事前状態と事後状態が実行コード内にアサーションとして組み込まれます。
検証
形式仕様記述は、システムの正当性を検証するための根拠としても使用されます。検証方法には、人間による証明と自動証明があります。
人間による証明
システムの正当性を証明する動機は、必ずしも品質保証のためだけではありません。システムの動作をより深く理解するために、証明を数学的な形式で行うことがあります。この場合、自然言語を使って証明が記述されることが多く、他の人が理解できるような形で記述されることが重要です。しかし、自然言語の曖昧さが原因でエラーを見逃す可能性や、高度な数学的専門知識が必要となる点が課題として指摘されています。
自動証明
システムの正当性を自動的に証明することへの関心が高まっています。自動化技術は大きく2つに分けられます。自動定理証明では、システムの説明、論理的公理、推論規則を入力として、形式的な証明を自動的に生成します。モデル検査では、実行時に取りうるすべての状態を検索し、特定の特性が満たされているかを確認します。これらの手法は、人間による証明よりも数学的に正確であるとされていますが、システムの「神託」的な性質や検証プログラム自体の検証が必要となる点が指摘されています。
形式手法は、その有効性が認識されている一方で、コストや適用範囲に関する批判も存在します。現状では、人間による証明も自動的な証明も多大な時間と費用を要するため、形式手法はコストが利益に見合う場合や、エラーの混入が多大な損害につながる場合に限定して用いられる傾向があります。例えば、航空宇宙工学のようにエラーが人命に関わる分野では、他の分野よりも形式手法が広く用いられています。また、形式手法がソフトウェア危機の特効薬のように過度に宣伝されることに対する批判もあります。
以下に、主な形式手法とそれらの記述法を列挙します。
仕様記述言語
アクターモデル
プロセス計算 (例: CSP, LOTOS, π計算)
ペトリネット
抽象状態機械 (ASM)
Alloy
ANSI/ISO C Specification Language (ACSL)
B-Method
CADP
Common Algebraic Specification Language (CASL)
Esterel
Lustre
mCRL2
Perfect Developer
RAISE
Rebeca Modeling Language
SPARK Ada
Specification and Description Language (SDL)
Temporal logic of actions (TLA)
uppaal
USL
VDM (VDM-SL, VDM++)
Z言語
モデルチェッカ
SPIN
PAT
* MALPAS Software Static Analysis Toolset
形式手法は、ソフトウェアの信頼性と品質を高める上で重要な役割を果たしますが、その適用には慎重な判断と専門的な知識が必要です。
形式手法の分類
形式手法は、その適用レベルに応じて以下の3つの水準に分類されます。
水準0: 軽い形式手法
このレベルでは、形式的な仕様記述を行いながらも、プログラム自体の開発は非形式的に進めます。このアプローチは「軽い形式手法」とも呼ばれ、比較的少ない労力で効果を上げることができるため、費用対効果を重視する場合に適しています。
水準1: 形式的な開発と検証
このレベルでは、形式手法をより深く活用し、開発と検証の両方を形式的に行います。例えば、仕様記述からプログラムを作成する際に、詳細化と属性の証明を厳密に行います。このアプローチは、高信頼性が求められるシステムに適しています。
水準2: 自動定理証明による完全な検証
このレベルでは、自動定理証明を用いて、システムの検証を完全に機械的に行います。このアプローチは非常に厳密ですが、導入には高度な専門知識と多大なコストがかかるため、特に重要なシステム（例えばマイクロプロセッサの設計の中核部分）など、エラーが大きな損失につながる場合に限定して適用されます。
また、プログラム意味論に基づいた分類として、形式手法は以下の3つの主要なアプローチに大別されます。
表示的意味論
このアプローチでは、システムの意味を領域理論を用いて表現します。システムの挙動を数学的な関数として捉え、領域理論の性質を通じてその意味を解析します。しかし、すべてのシステムが関数として直感的に表現できるわけではないという課題があります。
操作的意味論
このアプローチでは、より単純な計算モデルを用いて、システムがどのように動作するかを表現します。システムの意味を、計算モデルの一連の動作として捉え、その単純さによって表現を明確にしようとします。しかし、使用する計算モデルの意味論をどのように定義するかという問題が残ります。
公理的意味論
このアプローチでは、システムがある処理を行う前後の状態に着目し、その状態変化によってシステムの意味を表現します。古典的な論理学との関連が深く、システムの動作を事前条件と事後条件で記述します。しかし、事前状態と事後状態を示すだけで、システムが実際に行う処理を完全に表現できるかという疑問も指摘されています。
軽量形式手法（Lightweight Formal Methods）
一部の開発者からは、形式手法が過度に完全な形式化を重視しすぎているという意見があります。システムの複雑さや使用する言語の表現能力の限界から、完全な形式化が困難になる場合もあります。そのため、部分的な仕様記述や特定の応用に焦点を当てた軽量形式手法が提案されています。例えば、型システム、Uppaal、Alloy、Z言語を用いたユースケース駆動開発、CSK VDMツールセットなどが挙げられます。
形式手法の利用
形式手法は、ソフトウェア開発の様々な段階で利用できます。
仕様記述
形式手法は、開発対象システムの仕様を任意のレベルで記述するために利用できます。形式的な記述は、その後の開発活動のガイドとなるだけでなく、開発されたシステムの機能が要求通りであるかを検証するためにも用いられます。ジョン・バッカスが提案したプログラミング言語の文法を記述するBNF記法のように、形式仕様記述の必要性は早くから認識されてきました。
開発
形式仕様記述に基づいて、システムの設計を行い、実際の開発（ソフトウェアやハードウェアの実装）を行います。例えば、操作的意味論に基づく形式仕様記述では、実際のシステムの動作と仕様上の動作を比較したり、一部ツールでは仕様記述から自動的にコードを生成したりします。一方、公理的意味論に基づく形式仕様記述では、仕様に記述された事前状態と事後状態が実行コード内にアサーションとして組み込まれます。
検証
形式仕様記述は、システムの正当性を検証するための根拠としても使用されます。検証方法には、人間による証明と自動証明があります。
人間による証明
システムの正当性を証明する動機は、必ずしも品質保証のためだけではありません。システムの動作をより深く理解するために、証明を数学的な形式で行うことがあります。この場合、自然言語を使って証明が記述されることが多く、他の人が理解できるような形で記述されることが重要です。しかし、自然言語の曖昧さが原因でエラーを見逃す可能性や、高度な数学的専門知識が必要となる点が課題として指摘されています。
自動証明
システムの正当性を自動的に証明することへの関心が高まっています。自動化技術は大きく2つに分けられます。自動定理証明では、システムの説明、論理的公理、推論規則を入力として、形式的な証明を自動的に生成します。モデル検査では、実行時に取りうるすべての状態を検索し、特定の特性が満たされているかを確認します。これらの手法は、人間による証明よりも数学的に正確であるとされていますが、システムの「神託」的な性質や検証プログラム自体の検証が必要となる点が指摘されています。
形式手法への批判
形式手法は、その有効性が認識されている一方で、コストや適用範囲に関する批判も存在します。現状では、人間による証明も自動的な証明も多大な時間と費用を要するため、形式手法はコストが利益に見合う場合や、エラーの混入が多大な損害につながる場合に限定して用いられる傾向があります。例えば、航空宇宙工学のようにエラーが人命に関わる分野では、他の分野よりも形式手法が広く用いられています。また、形式手法がソフトウェア危機の特効薬のように過度に宣伝されることに対する批判もあります。
主な形式手法とその記述法
以下に、主な形式手法とそれらの記述法を列挙します。
仕様記述言語
アクターモデル
プロセス計算 (例: CSP, LOTOS, π計算)
ペトリネット
抽象状態機械 (ASM)
Alloy
ANSI/ISO C Specification Language (ACSL)
B-Method
CADP
Common Algebraic Specification Language (CASL)
Esterel
Lustre
mCRL2
Perfect Developer
RAISE
Rebeca Modeling Language
SPARK Ada
Specification and Description Language (SDL)
Temporal logic of actions (TLA)
uppaal
USL
VDM (VDM-SL, VDM++)
Z言語
モデルチェッカ
SPIN
PAT
* MALPAS Software Static Analysis Toolset
形式手法は、ソフトウェアの信頼性と品質を高める上で重要な役割を果たしますが、その適用には慎重な判断と専門的な知識が必要です。
もう一度検索
【記事の利用について】
タイトルと記事文章は、記事のあるページにリンクを張っていただければ、無料で利用できます。
※画像は、利用できませんのでご注意ください。
【リンクついて】
リンクフリーです。