Transmisja strumieniowa X-Machine

Stream X-machine ( SXM ) to model obliczeniowy wprowadzony przez Gilberta Laycocka w jego rozprawie doktorskiej z 1993 r., Teoria i praktyka testowania oprogramowania opartego na specyfikacjach . Oparty na maszynie X Samuela Eilenberga , rozszerzonej maszynie skończonej do przetwarzania danych typu X , Stream X-Machine jest rodzajem maszyny X do przetwarzania pamięci typu Mem z powiązanymi strumieniami wejściowymi i wyjściowymi . * i Wyj *, czyli gdzie X = Out * × Mem × In *. Przejścia Stream X-Machine są oznaczone funkcjami postaci φ: Mem × In → Out × Mem , to znaczy, które obliczają wartość wyjściową i aktualizują pamięć z bieżącej pamięci i wartości wejściowej.

Chociaż ogólna maszyna X została zidentyfikowana w latach 80. jako potencjalnie użyteczny model formalny do określania systemów oprogramowania, dopiero pojawienie się Stream X-Machine umożliwiło pełne wykorzystanie tego pomysłu. Florentin Ipate i Mike Holcombe opracowali teorię pełnego testowania funkcjonalnego , w której złożone systemy oprogramowania z setkami tysięcy stanów i milionami przejść można rozłożyć na oddzielne SXM, które można wyczerpująco przetestować, z gwarantowanym dowodem poprawnej integracji .

Ze względu na intuicyjną interpretację Stream X-Machines jako „środków przetwarzających z wejściami i wyjściami”, wzbudziły one coraz większe zainteresowanie ze względu na ich użyteczność w modelowaniu zjawisk w świecie rzeczywistym. Model SXM ma ważne zastosowania w tak różnych dziedzinach, jak biologia obliczeniowa , testowanie oprogramowania i ekonomia obliczeniowa oparta na agentach .

Stream X-Maszyna

Stream X-Machine (SXM) to rozszerzona maszyna skończona z pamięcią pomocniczą, wejściami i wyjściami. Jest to wariant ogólnej maszyny X , w której podstawowy typ danych X = Out * × Mem × In *, czyli krotka składająca się ze strumienia wyjściowego, pamięci i strumienia wejściowego. SXM oddziela przepływ sterowania systemu od przetwarzania przeprowadzanego przez system. Sterowanie jest modelowane przez maszynę skończoną (znaną jako skojarzony automat ), którego przejścia są oznaczone funkcjami przetwarzającymi wybranymi ze zbioru Φ (znanym jako typ maszyny), które działają na podstawowym typie danych.

Każda funkcja przetwarzania w Φ jest funkcją częściową i można uznać, że ma typ φ: Mem × In → Out × Mem , gdzie Mem to typ pamięci, a In i Out to odpowiednio typy wejścia i wyjścia. W dowolnym stanie przejście jest możliwe , jeśli dziedzina powiązanej funkcji φ _i obejmuje następną wartość wejściową oraz aktualny stan pamięci. Jeśli (co najwyżej) jedno przejście jest włączone w danym stanie, maszyna jest deterministyczna . Przekroczenie przejścia jest równoznaczne z zastosowaniem powiązanej funkcji φ _i , która zużywa jedno wejście, ewentualnie modyfikuje pamięć i daje jedno wyjście. Każda rozpoznana ścieżka przez maszynę generuje zatem listę φ ₁ ... φ _n funkcji, a SXM komponuje te funkcje razem, aby wygenerować relację na podstawowym typie danych | φ ₁ ... φ _n |: X → X .

Związek z maszynami X

Stream X-Machine jest wariantem X-machine , w którym podstawowy typ danych X = Out * × Mem × In *. W pierwotnej maszynie X φ _i są ogólnymi relacjami na X . W Stream X-Machine są one zwykle ograniczone do funkcji ; jednak SXM jest nadal deterministyczny tylko wtedy, gdy (co najwyżej) jedno przejście jest włączone w każdym stanie.

Ogólna maszyna X obsługuje dane wejściowe i wyjściowe przy użyciu wcześniejszej funkcji kodowania α: Y → X dla danych wejściowych i późniejszej funkcji dekodowania β: X → Z dla danych wyjściowych, gdzie Y i Z są odpowiednio typami wejściowymi i wyjściowymi. W Stream X-Machine te typy to strumienie:

  Y  =  wejście  *  Z  =  wyjście  *

a funkcje kodowania i dekodowania są zdefiniowane jako:

₀ α(  ins  ) = (<>,  mem  ,  ins  ) β(  out  ,  mem _n , <>) =  out

gdzie ins: In *, outs: Out * i mem _i : Mem . Innymi słowy, maszyna jest inicjowana z całym strumieniem wejściowym; a zdekodowany wynik to cały strumień wyjściowy, pod warunkiem, że strumień wejściowy zostanie ostatecznie zużyty (w przeciwnym razie wynik jest niezdefiniowany).

Każdej funkcji przetwarzającej w SXM nadano skrócony typ φ _SXM : Mem × In → Out × Mem . Można to odwzorować na ogólną X-maszyna typu φ: X → X, jeśli traktujemy to jako obliczenie:

 φ(  out  ,  mem _ja ,  in  ::  ins  ) = (  out  ::  out  ,  mem _i+1 ,  ins  )

gdzie :: oznacza konkatenację elementu i sekwencji. Innymi słowy, relacja wyodrębnia początek strumienia wejściowego, modyfikuje pamięć i dołącza wartość do końca strumienia wyjściowego.

Przetwarzanie i testowalne właściwości

₀ Ze względu na powyższą równoważność uwaga może skupić się na sposobie, w jaki Stream X-Machine przetwarza dane wejściowe na wyjścia, używając pamięci pomocniczej. Biorąc pod uwagę początkową pamięć stanu pamięci i strumień wejściowy ins , maszyna wykonuje krok po kroku, zużywając jedno wejście na raz i generując jedno wyjście na raz. Pod warunkiem, że istnieje (co najmniej) jedna rozpoznana ścieżka ścieżka = φ ₁ ... φ _n prowadząca do stanu, w którym wejście zostało zużyte, maszyna zwraca końcowy stan pamięci mem _n i strumień wyjściowy wychodzi . Ogólnie rzecz biorąc, możemy myśleć o tym jako o relacji obliczonej przez wszystkie rozpoznane ścieżki: | ścieżka | : Wejście * → Wyjście *. Nazywa się to często zachowaniem Stream X-Machine.

Zachowanie jest deterministyczne, jeśli (co najwyżej) jedno przejście jest włączone w każdym stanie. Ta właściwość oraz możliwość stopniowego kontrolowania zachowania maszyny w odpowiedzi na dane wejściowe i pamięć sprawiają, że jest to idealny model do specyfikacji systemów oprogramowania. Jeśli zakłada się, że zarówno specyfikacja, jak i implementacja to Stream X-Machines, wówczas implementacja może zostać przetestowana pod kątem zgodności ze specyfikacją maszyny, obserwując wejścia i wyjścia na każdym kroku. Laycock po raz pierwszy podkreślił użyteczność przetwarzania jednoetapowego z obserwacjami do celów testowych.

Holcombe i Ipate rozwinęli to w praktyczną teorię testowania oprogramowania, która była w pełni kompozycyjna i skalowała się do bardzo dużych systemów. Dowód poprawnej integracji gwarantuje, że testowanie każdego komponentu i każdej warstwy integracji z osobna odpowiada testowaniu całego systemu. Takie podejście typu „dziel i zwyciężaj” sprawia, że wyczerpujące testy są wykonalne dla dużych systemów.

Metoda testowania została opisana w osobnym artykule na temat metodologii testowania Stream X-Machine .

Zobacz też

X-machines , ogólny opis modelu X-machine, w tym prosty przykład.
Metodologia testowania Stream X-Machine , kompletna technika testowania funkcjonalnego . Korzystając z tej metodologii, można zidentyfikować skończony zestaw testów, które wyczerpująco określają, czy implementacja jest zgodna ze specyfikacją. Technika ta pokonuje formalne ograniczenia nierozstrzygalności, nalegając, aby użytkownicy stosowali starannie określony projekt zasad testowania podczas implementacji.
Communicating Stream X-Machines (CSXM) , współbieżna wersja modelu SXM, z zastosowaniami w różnych dziedzinach, od owadów społecznych po ekonomię.

Linki zewnętrzne

Projekt MOTIVE wykorzystujący techniki SXM do generowania zestawów testów dla oprogramowania obiektowego.
Projekt EURACE , zastosowanie technik CSXM w ekonomii obliczeniowej opartej na agentach.
x-machines.net , witryna opisująca tło badań nad X-machine.
Strona internetowa Mike'a (prof. WML) Holcombe'a na Uniwersytecie w Sheffield .

^ ^a ^b Gilbert Laycock (1993) Teoria i praktyka testowania oprogramowania opartego na specyfikacji . Praca doktorska, University of Sheffield, Wydział Informatyki. Streszczenie zarchiwizowane 05.11.2007 w Wayback Machine
^ Samuel Eilenberg (1974) Automaty, języki i maszyny, tom. A. _ Londyn: prasa akademicka.
^ M. Holcombe (1988) „Maszyny X jako podstawa dynamicznej specyfikacji systemu”. Software Engineering Journal 3 (2) , s. 69-76.
^ ^a ^b Mike Holcombe i Florentin Ipate (1998) Poprawne systemy - budowanie rozwiązania procesów biznesowych . Seria informatyki stosowanej . Berlin: Springer-Verlag.
^ ^a ^b F. Ipate i WML Holcombe (1997) „Metoda testowania integracji, której udowodniono, że znajduje wszystkie błędy”. Int. J. Komp. Matematyka , 63 , s. 159-178.
^ F. Ipate i M. Holcombe (1998) „Metoda udoskonalania i testowania uogólnionych specyfikacji maszyn”. Int. J. Komp. Matematyka 68 , s. 197-219.

[Lay93-1] Gilbert Laycock (1993) Teoria i praktyka testowania oprogramowania opartego na specyfikacji . Praca doktorska, University of Sheffield, Wydział Informatyki. Streszczenie zarchiwizowane 05.11.2007 w Wayback Machine

[Eil74-2] Samuel Eilenberg (1974) Automaty, języki i maszyny, tom. A. _ Londyn: prasa akademicka.

[Hol88-3] M. Holcombe (1988) „Maszyny X jako podstawa dynamicznej specyfikacji systemu”. Software Engineering Journal 3 (2) , s. 69-76.

[HolIp98-4] Mike Holcombe i Florentin Ipate (1998) Poprawne systemy - budowanie rozwiązania procesów biznesowych . Seria informatyki stosowanej . Berlin: Springer-Verlag.

[IpHol97-5] F. Ipate i WML Holcombe (1997) „Metoda testowania integracji, której udowodniono, że znajduje wszystkie błędy”. Int. J. Komp. Matematyka , 63 , s. 159-178.

[IpHol98-6] F. Ipate i M. Holcombe (1998) „Metoda udoskonalania i testowania uogólnionych specyfikacji maszyn”. Int. J. Komp. Matematyka 68 , s. 197-219.