コンピュータサイエンスにおいて、形式仕様とは、システムやソフトウェアの実装を支援することを目的とした数学に基づく技術です。システムの記述、動作の分析、そして厳密かつ効果的な推論ツールを用いて重要な特性を検証することで設計を支援するために使用されます。[1] [2]これらの仕様は、構文を持ち、意味が単一のドメインに収まり、有用な情報を推論するために使用できるという意味で形式的であると言えます。 [3]

モチベーション

コンピュータシステムは10年ごとにますます強力になり、その結果、社会への影響も大きくなっています。そのため、信頼性の高いソフトウェアの設計と実装を支援するためのより優れた技術が必要とされています。確立された工学分野では、製品設計の作成と検証の基盤として数学的解析が用いられています。形式仕様は、かつて予測されていたように、ソフトウェア工学の信頼性においてこれを実現する方法の一つです。コード品質の向上には、テストなどの他の手法が より一般的に使用されています。[1]

用途

このような仕様が与えられれば、形式検証技術を用いてシステム設計が仕様に沿って正しいことを証明することが可能になります。これにより、実際の実装に大規模な投資を行う前に、誤ったシステム設計を修正することが可能になります。もう一つのアプローチは、証明可能な正確性を備えた改良手順を用いて仕様を設計に変換し、最終的に構成上正しい実装に変換することです。

形式仕様は実装そのものではなく、実装を開発するために用いられるものです。形式仕様は、システムが何をすべきかを記述するものであり、どのようにすべきかを記述するものではありません。

優れた仕様には、適切、内部的に一貫性がある、曖昧でない、完全、満足のいく、最小限といった属性がいくつか備わっていなければなりません。[3]

良い仕様には次のようなものが含まれます。[3]

  • 構築可能性、管理可能性、進化可能性
  • ユーザビリティ
  • コミュニケーション能力
  • 強力で効率的な分析

形式仕様が関心を集めている主な理由の一つは、ソフトウェア実装の証明を可能にすることです。 [2]これらの証明は、仕様の検証、設計の正しさの検証、プログラムが仕様を満たしていることを証明するために使用できます。[2]

制限事項

設計 (または実装) は、それ自体では「正しい」と宣言することはできません。「特定の仕様に関して正しい」としか言いようがありません。形式仕様が解決すべき問題を正しく記述しているかどうかは、また別の問題です。これは、究極的には非形式的な具体的な問題ドメインの抽象化された形式表現を構築する問題に関係しており、そのような抽象化のステップは形式的な証明に馴染みがないため、対処が難しい問題でもあります。ただし、仕様が示すと予想される特性に関する「チャレンジ」定理を証明することで、仕様を検証することは可能です。これらの定理が正しければ、仕様作成者の仕様に対する理解、および仕様と基礎となる問題ドメインとの関係を強化します。正しくない場合は、仕様の作成 (および実装) に関わった人々のドメイン理解をよりよく反映するように、仕様を変更する必要があるでしょう。

ソフトウェア開発における形式手法は、産業界では広く利用されていません。多くの企業は、ソフトウェア開発プロセスに形式手法を適用することは費用対効果が高いとは考えていません。[4]これには様々な理由が考えられますが、その一部を以下に示します。

  • 時間
    • 初期費用は高いが、測定可能な収益は低い
  • 柔軟性
    • 多くのソフトウェア企業は、柔軟性に重点を置いたアジャイル開発手法を採用しています。システム全体の正式な仕様を事前に作成することは、柔軟性とは正反対であると認識されることがよくあります。しかしながら、「アジャイル」開発において正式な仕様を使用することの利点に関する研究はいくつかあります[5]。
  • 複雑
    • これらを理解し効果的に適用するには、高度な数学的専門知識と分析スキルが必要です[5]
    • この問題を解決するには、これらの技術を実装できるようにしながらも、その基礎となる数学を隠すツールやモデルを開発することである[2] [5]
  • 限定的な範囲[3]
    • プロジェクトに関わる全ての関係者にとって興味深い特性を捉えていない[3]
    • ユーザーインターフェースやユーザーインタラクションの仕様が不十分である[4]
  • 費用対効果が低い
    • これは完全に真実ではない。重要なシステムのコア部分のみに使用を限定することで、コスト効率が良いことが証明されている[4]

その他の制限事項: [3]

  • 分離
  • 低レベルのオントロジー
  • 不十分な指導
  • 関心の分離が不十分
  • ツールのフィードバックが悪い

パラダイム

形式仕様記述技術は、様々な分野や規模で、古くから存在してきました。[6] 形式仕様の実装は、モデル化しようとしているシステムの種類、適用方法、そしてソフトウェアライフサイクルのどの時点で導入されたかによって異なります。[2]これらのモデルは、以下の仕様パラダイムに分類できます。

  • 履歴ベースの仕様[3]
    • システム履歴に基づく動作
    • 主張は時間の経過とともに解釈される
  • 状態ベースの仕様[3]
    • システム状態に基づく動作
    • 一連の連続したステップ（例：金融取引）
    • Z、VDM、Bなどの言語はこのパラダイムに依存している[3]
  • 遷移ベースの仕様[3]
    • システムの状態から状態への遷移に基づく動作
    • 反応型システムと併用すると最適
    • ステートチャート、PROMELA、STeP-SPL、RSML、SCRなどの言語はこのパラダイムに依存しています[3]
  • 機能仕様[3]
    • システムを数学関数の構造として指定する
    • OBJ、ASL、PLUSS、LARCH、HOL、PVSはこのパラダイムに依存している[3]
  • 運用仕様[3]
    • ペイズリー、GIST、ペトリネット、プロセス代数などの初期の言語はこのパラダイムに依存している[3]
  • マルチパラダイム言語
    • FizzBee は、遷移/アクション ベースの仕様、非アトミック遷移による動作仕様を可能にし、アクター モデルも備えたマルチパラダイム仕様言語です。

上記のパラダイムに加えて、仕様作成の改善に役立つ特定のヒューリスティックを適用する方法があります。ここで参照されている論文は、仕様設計時に使用するヒューリスティックについて最もよく解説されています。[6]彼らは分割統治アプローチを適用することでこれを実現しています。

ソフトウェアツール

Z記法は、主要な形式仕様言語の一例です。他には、ウィーン開発方式の仕様言語（VDM-SL）やB方式の抽象機械記法（AMN）などがあります。Webサービス分野では、形式仕様は非機能特性を記述するためによく使用されます[7]（Webサービスのサービス品質）。

いくつかのツールは以下のとおりです: [4]

参考文献

  1. ^ ab Hierons, RM; Bogdanov, K.; Bowen, JP ; Cleaveland, R.; Derrick, J.; Dick, J.; Gheorghe, M.; Harman, M .; Kapoor, K.; Krause, P.; Lüttgen, G.; Simons, AJH; Vilkomir, SA ; Woodward, MR; Zedan, H. (2009). 「テストをサポートする形式仕様の使用」. ACM Computing Surveys . 41 (2): 1. CiteSeerX  10.1.1.144.3320 . doi :10.1145/1459352.1459354. S2CID  10686134.
  2. ^ abcde Gaudel, M.-C. (1994). 「形式仕様記述技術」.第16回国際ソフトウェア工学会議論文集. pp.  223– 227. doi :10.1109/ICSE.1994.296781. ISBN 978-0-8186-5855-6. S2CID  60740848。
  3. ^ abcdefghijklmno Lamsweerde, AV (2000). 「形式仕様」.ソフトウェア工学の将来に関する会議議事録 - ICSE '00 . pp.  147– 159. doi :10.1145/336512.336546. ISBN 978-1581132533. S2CID  4657483。
  4. ^ abcd Sommerville, Ian (2009). 「形式仕様」(PDF) .ソフトウェアエンジニアリング. 2013年2月3日閲覧。
  5. ^ abc ヌンメンマー、ティモ;ティエンスー、アレクシ。ベルキ、エレニ。ミコネン、トミ。クイッティネン、ユッシ。クルティマ、アンナカイサ（2011年8月4日）。 「実行可能な正式な仕様との自然なユーザー対話を促進することにより、アジャイル開発をサポートします。」ACM SIGSOFT ソフトウェア エンジニアリング ノート。36 (4): 1–10 .土井:10.1145/1988997.2003643。S2CID  2139235。
  6. ^ ab van der Poll, John A.; Paula Kotze (2002). 「どのような設計ヒューリスティックが形式仕様の有用性を高めるのか？」南アフリカコンピュータ科学者・情報技術者協会2002年年次研究会議議事録「技術による支援」 . SAICSIT '02: 179–194 . ISBN 9781581135961。
  7. ^ S-Cube知識モデル：形式仕様
ウィキメディア コモンズには、形式仕様に関連するメディアがあります。
  • 形式仕様の事例（テクノロジー） 2005年10月21日アーカイブ、Wayback Machineより Coryoth 2005年7月30日