抽象ステートマシン

コンピュータ サイエンスにおいて、抽象状態マシン( ASM )は、任意のデータ構造 (数学的論理の意味における構造、つまり、空でない集合とその集合上のいくつかの関数(操作)および関係を組み合わせたもの) である状態で動作する状態マシンです。

ASMメソッドは、システム開発の 2 つの目的の間のギャップを埋める、 実用的かつ科学的に十分に根拠のあるシステム エンジニアリングメソッドです。

• 現実世界の問題に対する人間の理解と定式化（特定のアプリケーションドメインによって決定される抽象化レベルでの正確な高レベルモデリングによる要件の捕捉）
• 変化するプラットフォーム上のコード実行マシンによるアルゴリズムソリューションの展開（設計上の決定、システムおよび実装の詳細の定義）。

この方法は、次の 3 つの基本概念に基づいています。

• ASM :有限状態マシンを任意のデータ構造で動作するように一般化した擬似コードの正確な形式
• 地上モデル：設計の権威ある参照モデルとして機能する厳密な形式の青写真
• 改良: モデルの抽象化を具体的なシステム要素に段階的にインスタンス化するための最も一般的なスキームであり、システム開発の連続的な段階で、より詳細な記述間の制御可能なリンクを提供します。

ASM の本来の概念では、単一のエージェントが一連のステップでプログラムを実行し、場合によっては環境と対話します。この概念は、複数のエージェントが同時にプログラムを実行する分散計算を捉えるために拡張されました。

ASM は任意の抽象レベルでアルゴリズムをモデル化するため、ハードウェアまたはソフトウェア設計の高レベル、低レベル、および中レベルのビューを提供できます。ASM 仕様は、多くの場合、抽象基本モデルから始まり、連続的な改良または粗化でより詳細なレベルに進む一連の ASM モデルで構成されます。

これら 3 つの概念のアルゴリズム的および数学的性質により、ASM モデルとその対象プロパティは、あらゆる厳密な形式の検証(推論による) または検証(実験、モデル実行のテストによる) を使用して分析できます。

ASM の概念は、ユーリ・グレヴィッチによるもので、彼は 1980 年代半ばに、あらゆるアルゴリズムは適切なチューリング マシンによってシミュレートされるというチューリングの命題を改良する方法としてこれを初めて提案しました。彼は、あらゆるアルゴリズムは、どんなに抽象的であっても、適切な ASM によって段階的にエミュレートされるというASM 命題を定式化しました。2000 年に、グレヴィッチは順次アルゴリズムの概念を公理化し、それらの ASM 命題を証明しました。大まかに言えば、公理は次のとおりです。

• 国家は構造であり、
• 状態遷移は状態の限られた部分のみに関係し、
• 構造の同型性の下ではすべてが不変です。(構造は代数として見ることができ、これが ASM の元の名前である進化代数の由来です。)

順次アルゴリズムの公理化と特徴付けは、並列アルゴリズムと対話型アルゴリズムに拡張されました。

1990年代には、コミュニティの努力により^[1]、コンピュータのハードウェアとソフトウェアの形式仕様と分析（検証と妥当性確認）にASMを使用するASM方式が開発されました。プログラミング言語（ Prolog、C、Javaなど）と設計言語（UMLとSDL ）の包括的なASM仕様が開発されました。

詳細な歴史的説明は他の場所で見ることができる。^{[2] [3]}

ASM の実行と分析のためのソフトウェア ツールが多数利用可能です。

• AsmBook: Egon Börger、Robert Stärk。抽象ステートマシン: 高レベルシステム設計および分析の方法
• JBook: R.Stärk、J.Schmid、E.Börger。 Java と Java 仮想マシン: 定義、検証、検証
• 議事録/ジャーナル号（2000年以降）
  • 2008: Springer LNCS 5238 抽象ステートマシン、B および Z
  • 2007: ASM'07 から選ばれた論文を掲載した J.UCS 特別号
  • 2006: Springer LNCS 5115 ソフトウェア構築と分析のための厳密な方法、ASM、B Dagstuhl セミナー
  • 2005: ASM'05 から選ばれた論文を掲載した Fundamenta Informatica 特別号 (電子会議)
  • 2004: Springer LNCS 3052 抽象ステートマシン 2004
  • 2003: Springer LNCS 2589 抽象ステートマシン 2003: 理論と実践の進歩
  • 2003: ASM'03 からの厳選論文を掲載した TCS 特別号
  • 2002: ダグシュトゥールセミナーレポート 抽象ステートマシンの理論と応用
  • 2001: J.UCS 7.11 ASM'01 からの選りすぐりの論文特集号
  • 2000: Springer LNCS 1912 抽象ステートマシン: 理論と応用
• ASM 貢献による比較ケーススタディ
  • 蒸気ボイラー制御: 仕様ケーススタディ、Springer LNCS 1165
  • プロダクションセル: ソフトウェア開発のケーススタディ、ASM モデル
  • Railcrossing: リアルタイムコンピューティングのための形式手法、ASM モデル
  • ライトコントロール: 要件エンジニアリングのケーススタディ、Dagstuhl セミナー
  • 請求書発行: 要件把握のケーススタディ

• OMG for BPMN (バージョン 2006): Springer LNCS 5316
• BPEL 用 OASIS: IJBPMI 1.4 (2006)
• ECMA for C#: 「C♯ のセマンティクスの高レベル モジュール定義」doi :10.1016/j.tcs.2004.11.008
• SDL-2000 の ITU-T: SDL-2000 の形式的意味論と SDL-2000 の形式的定義 - SDL 仕様を ASM モデルとしてコンパイルして実行する
• VHDL93 の IEEE: E.Boerger、U.Glaesser、W.Mueller。EA-Machines による抽象 VHDL'93 シミュレータの形式定義。Carlos Delgado Kloos および Peter T.~Breuer (編)、『VHDL の形式的意味論』、pp. 107–139、Kluwer Academic Publishers、1995 年
• Prolog の ISO: 「完全な Prolog の数学的定義」doi :10.1016/0167-6423(95)00006-E

（2000年以降の歴史的順）

• ASMワークベンチ
• ASMETA、抽象ステートマシンメタモデルとそのツールセット
• アスmL
• CoreASM は、拡張可能な ASM 実行エンジンである CoreASM で入手可能です。
• Archive.orgの AsmGofer
• SourceForgeの XASM オープンソース プロジェクト

• Y. Gurevich, Evolving Algebras 1993: Lipari Guide、E. Börger (ed.)、Specification and Validation Methods、Oxford University Press、1995、9-36。( ISBN 0-19-853854-5 ) 
• Y. Gurevich、「シーケンシャル抽象ステートマシンによるシーケンシャルアルゴリズムの捕捉」、ACM Transactions on Computational Logic 1(1) (2000年7月)、77–111。
• R. Stärk、J. Schmid、および E. Börger、『Java および Java 仮想マシン: 定義、検証、検証』、Springer-Verlag、2001 年 ( ISBN 3-540-42088-6 ) 
• E. Börger および R. Stärk、「Abstract State Machines: A Method for High-Level System Design and Analysis」、Springer-Verlag、2003 年 ( ISBN 3-540-00702-4 ) 
• E. Börger および A. Raschke、Modeling Companion for Software Practitioners、Springer-Verlag、2018. ^[4] ( ISBN 978-3-662-56639-8、doi :10.1007/978-3-662-56641-1) 

• 抽象ステートマシン
• AsmCenter は 2019-09-13 にWayback Machineにアーカイブされました
• TASM ツールセット: リアルタイム システムの仕様、シミュレーション、形式検証