Xマシン – 日本語百科事典辞書

X-machine
Xマシン（XM）の理論モデルで計算することによって導入さサミュエル・アイレンベルグ1974年 X「X-マシン」では、機械が動作する基本データ型を表します。たとえば、データベース（データベースタイプのオブジェクト）を操作するマシンは、database-machineになります。Xマシンモデルは、マシンの遷移にラベルを付けるために使用される記号がタイプX Xの関係を示すことを除いて、構造的に有限状態マシンと同じです。。遷移を通過することは、遷移にラベルを付ける関係を適用すること（データ型Xへの一連の変更を計算すること）と同等であり、マシン内のパスをトラバースすることは、関連するすべての関係を次々に適用することに対応します。

コンテンツ
1 元の理論
1.1 例 1.2 大会
2 1980年代
3 1990年代
4 2000年代
5 主要な亜種
5.1 アナログXマシン（AXM） 5.2 ストリームXマシン（SXM） 5.3 X-Machine（CXM）の通信 5.4 通信ストリームXマシン（CSXM） 5.5 オブジェクトX-マシン（OXM）
6 も参照してください
6.1 ダウンロード可能なテクニカルレポート
7 外部リンク
8 参考文献

元の理論
アイレンバーグの元のXマシンは、完全に一般的な計算の理論モデルであり（たとえば、チューリングマシンを想定）、決定論的、非決定論的、および非終了の計算を許可していました。彼の独創的な研究は、基本的なXマシンモデルの多くのバリエーションを公開しており、それぞれがわずかに異なる方法で有限状態マシンを一般化しました。
最も一般的なモデルでは、Xマシンは本質的に「タイプXのオブジェクトを操作するためのマシン」です。Xがいくつかあると仮定するデータ型と呼ばれ、基本データ型、およびΦは、（部分的）関係のセットであることと、φ：XXのアンXマシンは、有限状態機械その矢印Φにおける関係によって標識されます。任意の与えられた状態では、一つ以上の遷移がされてもよい有効場合ドメインφ関連する関係のiは全ての遷移が取られると仮定されている有効、各サイクルでXに格納された電流値（のサブセット）を受け付けます。機械による各認識パスは、φリスト生成1 …φ nは関係のを。私たちは、φの組成を呼び出す1 O … O φ nはこれらの関係のパスの関係、そのパスに対応します。Xマシンの動作は、そのパス関係によって計算されたすべての動作の和集合であると定義されています。一般に、これは非決定論的です。関係を適用するとXで一連の結果が計算されるためです。正式なモデルでは、考えられるすべての結果が並行して一緒に考慮されます。
実用的な目的のために、Xマシンはいくつかの有限の計算を記述する必要が符号化関数α：YXは、ある入力データ型YからXの初期状態に変換し、復号化関数β：XZは、Xの最終状態からある出力データ型Zに変換し直します。 Xの初期状態が入力されると、Xマシンが実行されて完了し、出力が監視されます。一般に、マシンはデッドロック（ブロックされる）、ライブロック（停止しない）、または1つ以上の完全な計算を実行する場合がこのため、最近の研究では、動作をより正確に制御および観察できる決定論的Xマシンに焦点が当てられています。

例
のぞき穴オプティマイザを備えたコンパイラは、プログラム構造を最適化するためのマシンと考えることができます。このオプティマイザマシンでは、エンコーディング関数αは入力タイプY（プログラムソース）からソースコードを取得し、それをメモリタイプX（解析ツリー）にロードします。マシンに、FindIncrements、FindSubExprs、およびCompletedと呼ばれるいくつかの状態があるとします。マシンは初期状態FindIncrementsで起動します。これは、遷移を介して他の状態にリンクされています。
FindIncrements DoIncrement FindIncrements FindIncrements SkipIncrement FindSubExprs FindSubExprs DoSubExpr FindSubExprs FindSubExprs SkipSubExpr 完了
リレーションDoIncrementは、「x：= x + 1」に対応する解析済みサブツリーを、最適化されたサブツリー「++ x」にマップします。リレーションDoSubExprは、同じ式「x + y … x + y」の複数のオカレンスを含む解析ツリーを、繰り返される計算「z：= x + y; … z」を格納するローカル変数を持つ最適化されたバージョンにマップします。 … z “。これらの関係は、Xにそれらが動作するドメイン値（サブツリー）が含まれている場合にのみ有効になります。残りのリレーションSkipIncrementとSkipSubExprは、補完的なケースで有効になっているnullops（IDリレーション）です。
したがって、オプティマイザは-machineが最初インプレースインクリメント（にある間に些細な追加の変換、完了まで実行されFindIncrementsの状態）、それはに移りますFindSubExprsの状態と共通部分式の除去のシリーズを実行した後に最終状態の完了に移行します。次に、デコード関数βは、メモリタイプX（最適化された解析ツリー）から出力タイプZ（最適化されたマシンコード）にマップされます。

大会
アイレンバーグの元のモデルを参照する場合、「X-machine」は通常、小文字の「m」で記述されます。これは、意味が「Xを処理するための任意のマシン」であるためです。後で特定のモデルを参照する場合、慣例では、そのバリアントの固有名詞の一部として大文字の「M」を使用します。

1980年代
Xマシンへの関心は、1980年代後半にMike Holcombe によって復活しました。彼は、モデルが制御フローを処理から明確に分離するため、ソフトウェアの形式仕様の目的に理想的であることに気づきました。十分に抽象的なレベルで機能する場合、計算の制御フローは通常、有限状態マシンとして表すことができます。したがって、Xマシンの仕様を完成させるために必要なのは、マシンの各遷移に関連する処理を指定することだけです。モデルの構造が単純なため、非常に柔軟です。このアイデアの他の初期の例証には、ホルコムのヒューマンコンピュータインターフェースの仕様、細胞生化学におけるプロセスのモデリング、、および軍事コマンドシステムにおける意思決定のスタネットのモデリングが含まれていました。

1990年代
Xマシンは、GilbertLaycockの決定論的なStreamX -Machine が、完全にテスト可能な大規模なソフトウェアシステムを指定するための基礎として機能することがわかった1990年代半ばから新たな注目を集めています。別の変形であるCommunicatingStream X-Machineは、生物学的プロセスおよび将来の群れベースの衛星システムのための有用なテスト可能なモデルを提供します。

2000年代
Xマシンは、Andras Kornaiによって語彙セマンティクスに適用されました。AndrasKornaiは、基本セットXの1つのメンバーが区別される「尖った」マシンによって単語の意味をモデル化します。言語学の他の分野、特にパーニニの現代的な再定式化への応用は、ジェラール・ヒュエットと彼の同僚によって開拓されました

主要な亜種
Xマシンが元の形式で検出されることはめったにありませんが、後続のいくつかの計算モデルを支えています。ソフトウェアテストの理論で最も影響力のあるモデルは、StreamX-Machineです。NASAは最近、群れ衛星システムの設計とテストにおいて、通信ストリームXマシンとプロセス計算WSCSSの組み合わせを使用することについて議論しました。

アナログXマシン（AXM）
最も初期のバリアントである連続時間アナログXマシン（AXM）は、1990年にMike Stannettによって、潜在的に「スーパーチューリング」の計算モデルとして導入されました。その結果、ハイパーコンピューティング理論での作業に関連しています。

ストリームXマシン（SXM）
ストリームX-マシン
最も一般的に遭遇するX-machineバリアントは、GilbertLaycockの1993Stream X-Machine（SXM）モデルであり、MikeHolcombeとFlorentinIpateの完全なソフトウェアテストの理論の基礎を形成します。。 Stream X-Machineは、基本データ型XがOut *× Mem × In *の形式であるという点で、アイレンバーグの元のモデルとは異なります。ここで、In *は入力シーケンス、Out *は出力シーケンスです。、およびMemは（残りの）メモリです。
このモデルの利点は、各ステップでの出力を観察しながら、システムをその状態と遷移を通じて一度に1ステップずつ駆動できることです。これらは、特定の機能が各ステップで実行されたことを保証する監視値です。その結果、複雑なソフトウェアシステムは、Stream X-Machinesの階層に分解され、トップダウン方式で設計され、ボトムアップ方式でテストされる可能性が設計とテストに対するこの分割統治アプローチは、Florentin Ipateの正しい統合の証明によって裏付けられています。これは、階層化されたマシンを個別にテストすることが、構成されたシステムをテストすることと同等であることを証明します。

X-Machine（CXM）の通信
「CXM」はそのIATAコードを持つアンゴラ空港については
、Camaxilo空港を参照してください複数のXマシンを並列に接続するための最初の提案は、Judith Barnardの1995年のCommunicatingX-machine（CXMまたはCOMX）モデルで、マシンは名前付き通信チャネル（ポートと呼ばれる）を介して接続されます。このモデルは、離散およびリアルタイムの両方のバリアントに存在します。この作品の以前のバージョンは完全に正式ではなく、完全な入力/出力関係を示していませんでした。
バッファリングされたチャネルを使用した同様のCommunicatingX-Machineアプローチは、PetrosKefalasによって開発されました。この作業の焦点は、コンポーネントの構成における表現力にありました。チャネルを再割り当てできるということは、StreamX-Machinesのテスト定理の一部が引き継がれなかったことを意味します。
これらのバリアントについては、別のページで詳しく説明しています。

通信ストリームXマシン（CSXM）
同時Xマシン構成の最初の完全に正式なモデルは、1999年にCristinaVertanとHoriaGeorgescuによって提案され、PhilipBirdとAnthonyCowlingによる自動通信に関する以前の研究に基づいています。 Vertanのモデルでは、マシンは、共有チャネルを介して直接通信するのではなく、共有通信マトリックス（基本的には鳩の穴の配列）を介して間接的に通信します。
Bălănescu、Cowling、Georgescu、Vertanなどは、このCSXMモデルの形式的な特性を詳細に研究しています。完全な入力/出力関係を表示できます。通信マトリクスは、同期通信のためのプロトコルを確立します。これの利点は、各マシンの処理を通信から切り離し、各動作を個別にテストできることです。この組成モデルは、標準的に等価で証明されたストリームX-マシン、ホルコムとIpateによって開発された以前のテスト理論を活用するようにします。
このX-machineバリアントについては、別のページで詳しく説明しています。

オブジェクトX-マシン（OXM）
KirillBogdanovとAnthonySimonsは、オブジェクト指向システムでのオブジェクトの動作をモデル化するために、Xマシンのいくつかのバリエーションを開発しました。このモデルは、モノリシックデータ型Xが、シリアルに構成された複数のオブジェクトに分散され、カプセル化されるという点で、StreamX-Machineアプローチとは異なります。システムは、入力と出力ではなく、メソッドの呼び出しと戻りによって駆動されます。この分野でのさらなる作業は、拡張されたサブクラスオブジェクトのスーパークラスの状態空間を分割する継承のコンテキストでの正式なテスト理論の適応に関するものでした。
「CCS-増強Xマシン」（CCSXM）モデル以降の非同期通信の存在下で、オブジェクト指向システムの完全な行動試験をサポートするために2002年にサイモンとStannettによって開発されたこれは、といくつかの類似性を負担することが期待されますNASAの最近の提案。しかし、2つのモデルの明確な比較はまだ行われ

も参照してください
Xマシンをストリーミングする
X-Machineテスト
Xマシンの通信

ダウンロード可能なテクニカルレポート
M. Stannett and AJH Simons（2002）CCS拡張Xマシンを使用したオブジェクト指向システムの完全な動作テスト。技術レポートCS-02-06、シェフィールド大学コンピュータサイエンス学部。ダウンロード
J. Aguado and AJ Cowling（2002）テストのためのXマシン理論の基礎。技術レポートCS-02-06、シェフィールド大学コンピュータサイエンス学部。ダウンロード
J. Aguado and AJ Cowling（2002）分散システムを指定するためのXマシンの通信システム。技術レポートCS-02-07、シェフィールド大学コンピュータサイエンス学部。ダウンロード
M.スタネット（2005）Xマシンの理論-パート1。技術レポートCS-05-09、シェフィールド大学コンピュータサイエンス学部。ダウンロード

外部リンク
http://www.dcs.shef.ac.uk/~ajc/csxms/index.html-TonyCowlingのCommunicatingSXMSystemsページ
http：//x-machines.com-MikeStannettのTheoryofX -Machinesサイト

参考文献
^ S. Eilenberg（1974）Automata、Languages and Machines、Vol。A。アカデミックプレス、ロンドン。
^ M. Holcombe（1988）「動的システム仕様の基礎としてのXマシン」、 Software Engineering Journal 3（2）、69-76ページ。
^ M. Holcombe（1988）「ヒューマンマシンインターフェイスの仕様における形式手法」、 International J. Command and Control、Communications andInfo。システム。 2頁24-34。
^ M. Holcombe（1986）「細胞生化学の数学的モデル」。テクニカルレポートCS-86-4、シェフィールド大学コンピュータサイエンス学部。
^ M. Stannett（1987）「コマンドシステムにおける意思決定への組織的アプローチ」。国際J.コマンドアンドコントロール、コミュニケーションおよび情報。システム。 1頁23-34。
^ Gilbert Laycock（1993）仕様ベースのソフトウェアテストの理論と実践。シェフィールド大学博士論文。抽象アーカイブで2007年11月5日、ウェイバックマシン
^ M. Holcombe and F. Ipate（1998）正しいシステム-ビジネスプロセスソリューションの構築。Springer、AppliedComputingシリーズ。
^ A. Bell and M. Holcombe（1996）「細胞処理の計算モデル」、「細胞および分子生物学システムにおける計算」、eds。M. Holcombe、R。Paton、R。Cuthbertson、シンガポール、World Scientific Press
^ MG Hinchey、CA Rouff、JL Rash、およびWF Truszkowski（2005）「インテリジェントスウォームの統合された正式な方法の要件」、FMICS’05の議事録、2005年9月5〜6日、ポルトガル、リスボン。Association for Computing Machinery、pp.125-133。
^ A. Kornai（2009）語彙意味論の代数。言語数学協会の2009年会議で発表された論文。In C. Ebert、G。Jäger、J。Michaelis（eds）Proc。第11回言語数学ワークショップ（MOL11）Springer LNCS 6149 174-199
^ G. Huet and B. Razet（2008）「Computingwith Relational Machines」チュートリアルがICON、2008年12月、Poona「Archivedcopy」（PDF）で発表されました。2015年2月19日にオリジナル（PDF）からアーカイブされました。
^ P. Goyal、G。Huet、A。Kulkarni、P。Scharf、R。Bunker（2012）「サンスクリット語処理のための分散プラットフォーム」Proc。COLING 2012、pp 1011-1028
^ M. Stannett（1990）「Xマシンと停止問題：スーパーチューリングマシンの構築」。コンピューティングの形式的側面 2、pp.331-41。
^ BJ Copeland（2002）「ハイパーコンピューティング」。マインドアンドマシーンズ 12、pp.461-502。
^ F. Ipate and M. Holcombe（1998）「一般化された機械仕様を改良およびテストする方法」。Int。J.Comp。算数。 68、pp.197-219。
^ F. Ipate and M. Holcombe（1997）「すべての障害を見つけることが証明されている統合テスト方法」、 International Journal of Computer Mathematics 63、pp.159-178。
^ J. Barnard、C。Theaker、J。Whitworth、およびM. Woodward（1995）「リアルタイムシステムの正式な設計のためのリアルタイム通信Xマシン」、 Proceedings of DARTS ’95、Universite Libre、ブリュッセル、ベルギー、2005年11月9〜11日
^ J. Barnard（1996） COMX：通信Xマシンを使用したコンピューターシステムの正式な設計のための方法論。スタッフォードシア大学博士論文。
^ A. Alderson and J. Barnard（1997） ‘On Making a Crossing Safe’、 Technical Report SOCTR / 97/01、School of Computing、StaffordshireUniversity。（Citeseer）
^ E. Kehris、G。Eleftherakis、およびP. Kefalas（2000）「離散イベントシミュレーションプログラムをモデル化およびテストするためのXマシンの使用」、 Proc。回路、システム、通信、コンピューターに関する第4回世界マルチカンファレンス、アテネ。
^ P. Kefalas、G。Eleftherakis、およびE. Kehris（2000）「Xマシンの通信：大規模システムのモジュール仕様の実用的なアプローチ」、テクニカルレポートCS-09 / 00、コンピュータサイエンス学部、シティカレッジ、テッサロニキ。
^ H. Georgescu and C. Vertan（2000）「ストリームXマシンを通信するための新しいアプローチ」、 Journal of Universal Computer Science 6 （5）、pp.490-502。
^ PR Bird and AJ Cowling（1994）「通信マシンのネットワークを使用した論理プログラミングのモデリング」、 Proc。並列および分散処理に関する第2回Euromicroワークショップ、マラガ、1994年1月26〜28日、156〜161ページ。概要
^ T.Balanescu、AJ Cowling、H。Georgescu、M。Gheorghe、M。Holcombe、C。Vertan（1999）「X-machinesシステムの通信はX-machinesにすぎない」、 Journal of Universal Computer Science、 5 （9 ）、pp。494-507。
^ AJH Simons、KE Bogdanov、およびWML Holcombe（2001）「オブジェクトマシンを使用した完全な機能テスト」、テクニカルレポートCS-01-18、シェフィールド大学コンピュータサイエンス学部
^ AJH Simons（2006）「動作的に互換性のあるオブジェクトタイプの回帰テストの理論」、ソフトウェアテスト、検証および信頼性、 16 （3）、John Wiley、pp.133-156。
^ M. Stannett and AJH Simons（2002） ‘CCS-Augmented X-Machines’、 Technical Report CS-2002-04、Department of Computer Science、Sheffield University、UK。