コンピュータサイエンス において、形式仕様は 、システムやソフトウェアの実装を支援することを目的とした数学に基づいた手法です。これらは、システムを記述し、その動作を分析し、厳密かつ効果的な推論ツールによって重要な特性を検証することで、その設計を支援するために使用されます。[ 1 ] [ 2 ] 形式的です。 [ 3 ]
モチベーション 数十年ごとにコンピュータシステムはますます強力になり、その結果、社会への影響も大きくなっています。そのため、信頼性の高いソフトウェアの設計と実装を支援するためのより優れた技術が必要とされています。確立された工学分野では、製品設計の作成と検証の基礎として数学的解析が用いられています。形式仕様は、かつて予測されたように、ソフトウェアエンジニアリングの信頼性を実現するための方法の一つです。 テスト などの他の方法は、 コードの品質を向上させるためによく用いられます。[ 1 ]
用途 このような仕様が与えられれば、 形式検証 技術を用いて、システム設計が仕様に照らして正しいこと を証明することが可能です。これにより、実際の導入に多額の投資を行う前に、誤ったシステム設計を修正することができます。別の方法としては、証明可能な正当性を備えた改良手順を用いて仕様を設計に変換し、最終的に 構成上正しい 実装へと変換するという方法があります。
形式仕様は実装そのもの ではなく 、実装を開発するための手段として用いられる。形式仕様はシステムが何 をするべきかを記述するものであり、システムがどのように動作するべきかを記述するものではない。
優れた仕様書には、以下の属性のいくつかが備わっている必要があります。適切であること、内部的に一貫性があること、曖昧さがないこと、完全であること、要件を満たしていること、最小限であること。[ 3 ]
優れた仕様には以下が含まれます。[ 3 ]
構築性、管理性、進化性 ユーザビリティ コミュニケーション能力 強力かつ効率的な分析 形式仕様に関心が寄せられる主な理由の1つは、ソフトウェア実装の証明を実行できる 能力を提供することである。 [ 2 ] [ 2 ]
制限事項 設計（または実装）は、それ自体で「正しい」と断言できるものではありません。それは「与えられた仕様に関して正しい」としか言えません。形式仕様が解決すべき問題を正しく記述しているかどうかは、別の問題です。また、これは最終的に非公式な具体的な問題領域 の抽象化された形式表現を構築する問題に関わるため、対処が難しい問題でもあります。このような抽象化のステップは形式的な証明には適さないからです。しかし、仕様が示すと期待される特性に関する「チャレンジ」定理を 証明することで、仕様を検証する ことは可能です。これらの定理が正しければ、仕様作成者の仕様および基礎となる問題領域との関係についての理解が強化されます。そうでなければ、仕様の作成（および実装）に関わる人々の領域理解をよりよく反映するように、仕様を変更する必要があるでしょう。
ソフトウェア開発の形式手法は 、業界では広く使われていません。ほとんどの企業は、ソフトウェア開発プロセスに形式手法を適用することは費用対効果が高いとは考えていません。[ 4 ]
時間 柔軟性 多くのソフトウェア企業は、柔軟性を重視したアジャイル手法 を採用しています。システム全体の形式仕様を事前に作成することは、柔軟性とは正反対であると見なされることが多いです。しかし、「アジャイル」開発で形式仕様を使用することの利点に関する研究もいくつかあります[ 5 ]。 複雑 それらを理解するには高度な数学的専門知識と分析スキルが必要であり、効果的に適用できる必要がある[ 5 ]。 これに対する解決策は、これらの技術を実装できるが、その根底にある数学を隠蔽するツールやモデルを開発することである[ 2 ] [ 5 ]。 限定された範囲[ 3 ] これらは、プロジェクトのすべての利害関係者 にとって関心のある特性を捉えていません[ 3 ] ユーザーインターフェースとユーザーインタラクションの指定がうまくできていない[ 4 ] 費用対効果が低い これは完全に正しいとは言えません。重要なシステムのコア部分のみに使用を限定することで、費用対効果が高いことが示されています[ 4 ]。 その他の制限事項：[ 3 ]
分離 低レベルオントロジー 指導が不十分 関心の分離が 不十分ツールのフィードバックが不十分
パラダイム 形式仕様の手法は、さまざまな分野や規模でかなり長い間存在してきました。[ 6 ] [ 2 ]
履歴に基づく仕様[ 3 ] システム履歴に基づく動作 主張は時間の経過とともに解釈される 状態ベースの仕様[ 3 ] システムの状態に基づく動作 一連の連続した手順（例：金融取引） Z 、VDM 、B などの言語はこのパラダイムに依存している[ 3 ]。 遷移ベースの仕様[ 3 ] システムの状態遷移に基づく動作 反応型システムと併用するのが最適です Statecharts、PROMELA、STeP-SPL、RSML、SCRなどの言語はこのパラダイムに依存しています[ 3 ]。 機能仕様[ 3 ] システムを数学関数の構造として指定する OBJ、ASL、PLUSS、LARCH、HOL、PVSはこのパラダイムに依存している[ 3 ]。 運用仕様書[ 3 ] マルチパラダイム言語 FizzBeeは、遷移/アクションベースの仕様記述、非原子遷移を伴う振る舞いの仕様記述、およびアクターモデルを可能にするマルチパラダイム仕様記述言語です。 上記のパラダイムに加えて、これらの仕様の作成を改善するために特定のヒューリスティックを適用する方法があります。ここで参照されている論文は、仕様を設計する際に使用するヒューリスティックについて最もよく説明しています。[ 6 ] 分割統治 アプローチを適用することでこれを行っています。
参考文献 1 2 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 . 1 2 3 4 5 Gaudel, M.-C. (1994). "形式仕様記述技法". 第16回国際ソフトウェア工学会議議事録 . pp. 223–227 . doi : 10.1109/ICSE.1994.296781 . ISBN 978-0-8186-5855-6 . S2CID 60740848 . 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 Lamsweerde, AV ( 2000). "形式仕様". Proceedings of the conference on the future of Software engineering - ICSE '00 . pp. 147–159 . doi : 10.1145/336512.336546 . ISBN 978-1581132533 . S2CID 4657483 . 1 2 3 4 Sommerville, Ian (2009). "形式仕様" (PDF) . ソフトウェアエンジニアリング. 2013年 2月3日 取得 . 1 2 3 ヌンメンマー、ティモ。ティエンスー、アレクシ。ベルキ、エレニ。ミコネン、トミ。クイッティネン、ユッシ。クルティマ、アンナカイサ（2011年8月4日）。 「実行可能な正式な仕様との自然なユーザー対話を促進することにより、アジャイル開発をサポートします。」 ACM SIGSOFT ソフトウェア エンジニアリング ノート 。 36 (4): 1–10 . 土井 : 10.1145/1988997.2003643 。 S2CID 2139235 。 1 2 van der Poll, John A.; Paula Kotze (2002). 「形式仕様の有用性を高める設計ヒューリスティクスとは何か？」 . 南アフリカコンピュータ科学者・情報技術者協会2002年年次研究会議「技術による実現」議事録 . SAICSIT '02: 179–194 . ISBN 9781581135961 。↑ Sキューブ知識モデル：形式仕様
外部リンク ウィキメディア・コモンズには、形式仕様 に関連するメディアがあります。
