maszyna X

Maszyna X ( XM ) to teoretyczny model obliczeń wprowadzony przez Samuela Eilenberga w 1974 r. X w „maszynie X” reprezentuje podstawowy typ danych, na których działa maszyna; na przykład maszyna, która operuje na bazach danych (obiektach typu database ) byłaby bazą danych -maszyna. Model maszyny X jest strukturalnie taki sam jak maszyna skończona , z wyjątkiem tego, że symbole używane do oznaczania przejść maszyny oznaczają relacje typu X → X . Przekroczenie przejścia jest równoznaczne z zastosowaniem relacji, która je opisuje (obliczenie zestawu zmian w typie danych X ), a przejście przez ścieżkę w maszynie odpowiada zastosowaniu wszystkich powiązanych relacji, jedna po drugiej.

Oryginalna teoria

Oryginalna maszyna X Eilenberga była całkowicie ogólnym teoretycznym modelem obliczeń (na przykład obejmującym maszynę Turinga ), który dopuszczał obliczenia deterministyczne, niedeterministyczne i niekończące. Jego przełomowa praca opublikowała wiele wariantów podstawowego modelu maszyny X, z których każdy uogólniał maszynę skończoną w nieco inny sposób.

W najbardziej ogólnym modelu maszyna X jest zasadniczo „maszyną do manipulowania obiektami typu X”. Załóżmy, że X jest pewnym typem danych , zwanym podstawowym typem danych , oraz że Φ jest zbiorem (częściowych) relacji φ: X → X. Maszyna X jest maszyną skończoną , której strzałki są oznaczone relacjami w Φ. W dowolnym danym stanie jedno lub więcej przejść może być włączonych , jeśli dziedzina powiązanej relacji φ i akceptuje (podzbiór) bieżących wartości przechowywanych w X. W każdym cyklu zakłada się, że wszystkie włączone przejścia zostały wykonane. Każda rozpoznana ścieżka przez maszynę generuje listę φ 1 ... φ n relacji. Złożenie φ 1 o ... o φ n tych relacji nazywamy relacją po ścieżce odpowiadającą tej ścieżce. Zachowanie _ maszyny X jest zdefiniowana jako suma wszystkich zachowań obliczonych przez jej relacje ścieżek. Ogólnie rzecz biorąc, jest to niedeterministyczne, ponieważ zastosowanie dowolnej relacji oblicza zestaw wyników na X. W modelu formalnym wszystkie możliwe wyniki są rozpatrywane razem, równolegle.

Ze względów praktycznych maszyna X powinna opisywać pewne skończone obliczenia. Funkcja kodująca α: Y → X konwertuje z pewnego wejściowego typu danych Y na stan początkowy X, a funkcja dekodująca β: X → Z, konwertuje z powrotem ze stanu końcowego X na pewien wyjściowy typ danych Z. Po zapełnieniu stanu początkowego X maszyna X działa do końca, a następnie obserwuje się wyjścia. Ogólnie rzecz biorąc, maszyna może być zablokowana (zablokowana) lub aktywna (nigdy się nie zatrzymywać) lub wykonać jedno lub więcej pełnych obliczeń. Z tego powodu nowsze badania koncentrowały się na deterministycznych maszynach X, których zachowanie można dokładniej kontrolować i obserwować.

Przykład

Kompilator z optymalizatorem wizjera można traktować jako maszynę do optymalizacji struktury programu. W tej optymalizatora funkcja kodowania α pobiera kod źródłowy z typu wejściowego Y (źródło programu) i ładuje go do pamięci typu X (drzewo analizy). Załóżmy, że maszyna ma kilka stanów o nazwach FindIncrements , FindSubExprs i Completed . Maszyna uruchamia się w stanie początkowym FindIncrements , który jest połączony z innymi stanami poprzez przejścia: 

  
  
  
   FindIncrements  →  DoIncrement  FindIncrements  FindIncrements  →  SkipIncrement  FindSubExprs  FindSubExprs  →  DoSubExpr  FindSubExprs  FindSubExprs  →  SkipSubExpr  Zakończono

Relacja DoIncrement odwzorowuje przeanalizowane poddrzewo odpowiadające „x := x + 1” na zoptymalizowane poddrzewo „++x”. Relacja DoSubExpr odwzorowuje drzewo analizy zawierające wielokrotne wystąpienia tego samego wyrażenia „x + y… x + y” w zoptymalizowaną wersję ze zmienną lokalną do przechowywania powtórzonych obliczeń „z := x + y; ... z ... z". Relacje te są włączone tylko wtedy, gdy X zawiera wartości domeny (poddrzewa), na których działają. Pozostałe relacje SkipIncrement i SkipSubExpr są puste (relacje tożsamościowe) włączone w komplementarnych przypadkach.

Tak więc maszyna Optymalizatora będzie działać do końca, najpierw konwertując trywialne dodatki na przyrosty w miejscu (w stanie FindIncrements ), następnie przejdzie do stanu FindSubExprs i wykona serię typowych usunięć wyrażeń podrzędnych, po czym przejdzie do stanu końcowego Completed . Funkcja dekodowania β będzie następnie mapować z typu pamięci X (zoptymalizowane drzewo analizy) na typ wyjściowy Z (zoptymalizowany kod maszynowy).

Konwencja

Odnosząc się do oryginalnego modelu Eilenberga, „maszyna X” jest zwykle zapisywana małą literą „m”, ponieważ sens to „dowolna maszyna do przetwarzania X”. Odnosząc się do późniejszych konkretnych modeli, konwencja polega na użyciu dużej litery „M” jako części nazwy własnej tego wariantu.

lata 80

Zainteresowanie X-machine zostało wznowione pod koniec lat 80. XX wieku przez Mike'a Holcombe'a, który zauważył, że model ten jest idealny do celów formalnej specyfikacji oprogramowania , ponieważ wyraźnie oddziela przepływ sterowania od przetwarzania . Pod warunkiem, że działa się na wystarczająco abstrakcyjnym poziomie, przepływy sterowania w obliczeniach można zwykle przedstawić jako maszynę o skończonych stanach, więc aby uzupełnić specyfikację maszyny X, pozostaje tylko określić przetwarzanie związane z każdym przejściem maszyny. Konstrukcyjna prostota modelu sprawia, że ​​jest on niezwykle elastyczny; inne wczesne przykłady tego pomysłu obejmowały specyfikację interfejsów człowiek-komputer autorstwa Holcombe'a, jego modelowanie procesów w biochemii komórkowej oraz modelowanie procesu podejmowania decyzji w wojskowych systemach dowodzenia przez Stannetta.

lata 90

X-machines zyskały nowe zainteresowanie od połowy lat 90., kiedy stwierdzono, że deterministyczna Stream X-Machine Gilberta Laycocka służy jako podstawa do określania dużych systemów oprogramowania, które są w pełni testowalne. Inny wariant, Communicating Stream X-Machine, oferuje użyteczny, testowalny model dla procesów biologicznych i przyszłych systemów satelitarnych opartych na rojach .

2000s

Maszyny X zostały zastosowane do semantyki leksykalnej przez Andrasa Kornai , który modeluje znaczenie słów za pomocą „spiczastych” maszyn, które wyróżniają jeden element podstawowego zbioru X. Pionierami zastosowania do innych gałęzi językoznawstwa, w szczególności do współczesnego przeformułowania Pāṇiniego , byli Gerard Huet i jego współpracownicy

Główne warianty

Maszyna X jest rzadko spotykana w swojej pierwotnej formie, ale stanowi podstawę kilku kolejnych modeli obliczeń. Najbardziej wpływowym modelem teorii testowania oprogramowania był Stream X-Machine . NASA niedawno omawiała wykorzystanie kombinacji Communicating Stream X-Machines i rachunku procesów WSCSS w projektowaniu i testowaniu systemów satelitarnych roju .

Analogowa maszyna X (AXM)

Najwcześniejszy wariant, analogowa maszyna X w czasie ciągłym ( AXM ), został wprowadzony przez Mike'a Stannetta w 1990 roku jako potencjalnie „super-Turingowy” model obliczeń; jest to w konsekwencji związane z pracą w hiperkomputacji .

Strumień X-Machine (SXM)

Główny artykuł: Stream X-Machine

Najczęściej spotykanym wariantem X-machine jest model Stream X-Machine ( SXM ) Gilberta Laycocka z 1993 r., który stanowi podstawę teorii kompletnego testowania oprogramowania Mike'a Holcombe'a i Florentina Ipate'a, która gwarantuje znane właściwości poprawności po zakończeniu testowania. Stream X-Machine różni się od oryginalnego modelu Eilenberga tym, że podstawowy typ danych X ma postać Out * × Mem × In *, gdzie In * to sekwencja wejściowa, Out * to sekwencja wyjściowa, a Mem to (reszta) pamięci.

Zaletą tego modelu jest to, że umożliwia sterowanie systemem, krok po kroku, przez jego stany i przejścia, obserwując wyjścia na każdym kroku. Są to wartości świadków, które gwarantują wykonanie poszczególnych funkcji na każdym kroku. W rezultacie złożone systemy oprogramowania można rozłożyć na hierarchię Stream X-Machines, projektowanych odgórnie i testowanych oddolnie. To podejście do projektowania i testowania oparte na zasadzie „dziel i zwyciężaj” jest poparte dowodem prawidłowej integracji przeprowadzonym przez Florentina Ipate, który dowodzi, że niezależne testowanie maszyn warstwowych jest równoważne testowaniu złożonego systemu.

Komunikacja X-Machine (CXM)

„CXM” przekierowuje tutaj. Informacje na temat lotniska w Angoli z tym kodem IATA można znaleźć na stronie Port lotniczy Camaxilo .

Najwcześniejszą propozycją równoległego połączenia kilku maszyn X jest model Communicating X-machine ( CXM lub COMX ) Judith Barnard z 1995 r. , W którym maszyny są połączone nazwanymi kanałami komunikacyjnymi (znanymi jako porty ); model ten istnieje zarówno w wariantach dyskretnych, jak iw czasie rzeczywistym. Wcześniejsze wersje tej pracy nie były w pełni sformalizowane i nie pokazywały pełnych relacji wejścia/wyjścia.

Podobne podejście do Communicating X-Machine wykorzystujące buforowane kanały zostało opracowane przez Petrosa Kefalasa. W tej pracy skupiono się na wyrazistości kompozycji składników. Możliwość ponownego przypisania kanałów oznaczała, że ​​niektóre twierdzenia testowe ze Stream X-Machines nie zostały przeniesione.

Warianty te omówiono bardziej szczegółowo na osobnej stronie.

Komunikacja Stream X-Machine (CSXM)

Pierwszy w pełni formalny model współbieżnej kompozycji X-machine został zaproponowany w 1999 roku przez Cristinę Vertan i Horię Georgescu, w oparciu o wcześniejsze prace Philipa Birda i Anthony'ego Cowlinga nad automatami komunikacyjnymi. W modelu Vertana maszyny komunikują się pośrednio, poprzez wspólną matrycę komunikacyjną (zasadniczo szereg przegródek), a nie bezpośrednio przez wspólne kanały.

Bălănescu, Cowling, Georgescu, Vertan i inni szczegółowo zbadali formalne właściwości tego modelu CSXM. Można pokazać pełne relacje wejścia/wyjścia. Macierz komunikacyjna ustanawia protokół komunikacji synchronicznej. Zaletą tego jest to, że oddziela przetwarzanie każdej maszyny od ich komunikacji, umożliwiając osobne testowanie każdego zachowania. Ten model kompozycyjny okazał się równoważny ze standardowym Stream X-Machine , wykorzystując w ten sposób wcześniejszą teorię testowania opracowaną przez Holcombe i Ipate.

Ten wariant maszyny X jest omówiony bardziej szczegółowo na osobnej stronie.

Obiektowa maszyna X (OXM)

Kirill Bogdanov i Anthony Simons opracowali kilka wariantów maszyny X do modelowania zachowania obiektów w systemach zorientowanych obiektowo. Ten model różni się od Stream X-Machine tym, że monolityczny typ danych X jest rozproszony i zawarty w kilku obiektach, które są składane szeregowo; a systemy są napędzane przez wywołania i zwroty metod, a nie przez dane wejściowe i wyjściowe. Dalsze prace w tym obszarze dotyczyły adaptacji formalnej teorii testowania w kontekście dziedziczenia, które dzieli przestrzeń stanów nadklasy na rozszerzone obiekty podklas.

Model „CCS-augmented X-machine” (CCSXM) został później opracowany przez Simonsa i Stannetta w 2002 roku w celu wspierania pełnego testowania behawioralnego systemów zorientowanych obiektowo w obecności komunikacji asynchronicznej. Oczekuje się, że będzie on w pewnym stopniu podobny do modelu NASA ostatnia propozycja; ale nie przeprowadzono jeszcze ostatecznego porównania tych dwóch modeli.

Zobacz też

Raporty techniczne do pobrania

  • M. Stannett i AJH Simons (2002) Kompletne testy behawioralne systemów zorientowanych obiektowo przy użyciu maszyn X wspomaganych CCS. Raport techniczny CS-02-06, Wydział Informatyki Uniwersytetu w Sheffield. Pobierać
  • J. Aguado i AJ Cowling (2002) Podstawy teorii maszyny X do testowania. Raport techniczny CS-02-06, Wydział Informatyki Uniwersytetu w Sheffield. Pobierać
  • J. Aguado i AJ Cowling (2002) Systems of Communicating X-machines for Specifying Distributed Systems. Raport techniczny CS-02-07, Wydział Informatyki, Uniwersytet w Sheffield. Pobierać
  • M. Stannett (2005) The Theory of X-Machines - Part 1. Tech Report CS-05-09, Dept of Computer Science, University of Sheffield. Pobierać

Linki zewnętrzne

  1. ^ a b S. Eilenberg (1974) Automaty, języki i maszyny, tom. A. _ Prasa Akademicka, Londyn.
  2. ^ M. Holcombe (1988) „Maszyny X jako podstawa specyfikacji systemu dynamicznego”, Software Engineering Journal 3 (2), s. 69-76.
  3. ^ M. Holcombe (1988) „Metody formalne w specyfikacji interfejsu człowiek-maszyna”, International J. Command and Control, Communications and Info. Systemy. 2 , s. 24-34.
  4. ^ M. Holcombe (1986) „Modele matematyczne biochemii komórki”. Raport techniczny CS-86-4, Wydział Informatyki, Sheffield University.
  5. ^ M. Stannett (1987) „Organizacyjne podejście do podejmowania decyzji w systemach dowodzenia”. International J. Command and Control, Communications and Info. Systemy. 1 , s. 23-34.
  6. ^ a b Gilbert Laycock (1993) Teoria i praktyka testowania oprogramowania opartego na specyfikacji . Praca doktorska, Uniwersytet w Sheffield. Streszczenie zarchiwizowane 5 listopada 2007 r. W Wayback Machine
  7. ^ a b M. Holcombe i F. Ipate (1998) Correct Systems - Budowanie rozwiązania dla procesów biznesowych . Springer, Seria Informatyki Stosowanej.
  8. ^ A. Bell i M. Holcombe (1996) „Modele obliczeniowe przetwarzania komórkowego”, w Computation in Cellular and Molecular Biological Systems , wyd. M. Holcombe, R. Paton i R. Cuthbertson, Singapur, World Scientific Press.
  9. ^ a b MG Hinchey, CA Rouff, JL Rash i WF Truszkowski (2005) „Wymagania zintegrowanej metody formalnej dla inteligentnych rojów”, w Proceedings of FMICS'05, 5–6 września 2005 r., Lizbona, Portugalia . Association for Computing Machinery, s. 125-133.
  10. ^ A. Kornai (2009) Algebra semantyki leksykalnej . Referat wygłoszony na Zjeździe Stowarzyszenia Matematyki Języka w 2009 roku . W In C. Ebert, G. Jäger, J. Michaelis (red.) Proc. 11. Warsztat Matematyki Języka (MOL11) Springer LNCS 6149 174-199 [1]
  11. ^ G. Huet i B. Razet (2008) Samouczek „Computing with Relational Machines” zaprezentowany na ICON, grudzień 2008, Poona „Zarchiwizowana kopia” (PDF) . Zarchiwizowane od oryginału (PDF) w dniu 19 lutego 2015 r . Źródło 7 sierpnia 2013 r . {{ cite web }} : CS1 maint: zarchiwizowana kopia jako tytuł ( link )
  12. ^ P. Goyal, G. Huet, A. Kulkarni, P. Scharf, R. Bunker (2012) „Rozproszona platforma do przetwarzania sanskrytu” w Proc. COLING 2012, s. 1011–1028 [2]
  13. ^ M. Stannett (1990) „Maszyny X i problem zatrzymania: budowa maszyny super-Turinga”. Formalne aspekty informatyki 2 , s. 331-41.
  14. ^ BJ Copeland (2002) „Hyperkomputacja”. Umysły i maszyny 12 , s. 461-502.
  15. ^ F. Ipate i M. Holcombe (1998) „Metoda udoskonalania i testowania uogólnionych specyfikacji maszyn”. Int. J. Komp. Matematyka 68 , s. 197-219.
  16. ^ F. Ipate i M. Holcombe (1997) „Metoda testowania integracji, której udowodniono, że znajduje wszystkie błędy”, International Journal of Computer Mathematics 63 , s. 159-178.
  17. ^ J. Barnard, C. Theaker, J. Whitworth i M. Woodward (1995) „Komunikujące się w czasie rzeczywistym maszyny X do formalnego projektowania systemów czasu rzeczywistego”, w Proceedings of DARTS '95, Universite Libre, Bruksela, Belgia, 9–11 listopada 2005 r
  18. ^ J. Barnard (1996) COMX: Metodologia formalnego projektowania systemów komputerowych przy użyciu komunikujących się maszyn X. Praca doktorska, Staffordshire University.
  19. ^ A. Alderson i J. Barnard (1997) „On Making a Crossing Safe”, Raport techniczny SOCTR / 97/01 , School of Computing, Staffordshire University. (cytat)
  20. ^ E. Kehris, G. Eleftherakis i P. Kefalas (2000) „Używanie maszyn X do modelowania i testowania programów symulacji zdarzeń dyskretnych”, Proc. Czwarta Światowa Multikonferencja Obwodów, Systemów, Komunikacji i Komputerów , Ateny.
  21. ^ P. Kefalas, G. Eleftherakis i E. Kehris (2000) „Komunikacja maszyn X: praktyczne podejście do specyfikacji modułowej dużych systemów”, Raport techniczny CS-09/00, Wydział Informatyki , City College, Saloniki.
  22. ^ H. Georgescu i C. Vertan (2000) „Nowe podejście do komunikacji strumieniowej maszyn X”, Journal of Universal Computer Science 6 (5) , s. 490-502.
  23. ^ PR Bird i AJ Cowling (1994) „Programowanie logiki modelowania przy użyciu sieci komunikujących się maszyn”, w Proc. 2nd Euromicro Workshop on Parallel and Distributed Processing, Malaga, 26-28 stycznia 1994 , s. 156-161. Abstrakcyjny
  24. ^ T.Balanescu, AJ Cowling, H. Georgescu, M. Gheorghe, M. Holcombe i C. Vertan (1999) „Komunikacyjne systemy maszyn X to nic więcej niż maszyny X”, Journal of Universal Computer Science , 5 (9 ) , s. 494-507.
  25. ^ AJH Simons, KE Bogdanov i WML Holcombe (2001) „Kompletne testy funkcjonalne przy użyciu maszyn obiektowych”, Raport techniczny CS-01-18, Wydział Informatyki , Uniwersytet w Sheffield
  26. ^ AJH Simons (2006) „Teoria testowania regresji dla behawioralnie zgodnych typów obiektów”, Testowanie oprogramowania, weryfikacja i niezawodność , 16 (3) , John Wiley, s. 133-156.
  27. ^ M. Stannett i AJH Simons (2002) „CCS-Augmented X-Machines”, raport techniczny CS-2002-04, Wydział Informatyki , Sheffield University, Wielka Brytania.
Pobrano z „ https://en.wikipedia.org/w/index.php?title=X-machine&oldid=1035252157 ”