Testowanie maszyny X

Metodologia testowania (Stream) X-Machine to kompletne podejście do testowania funkcjonalnego oprogramowania i sprzętu, które wykorzystuje skalowalność modelu obliczeniowego Stream X-Machine . Korzystając z tej metodologii, można prawdopodobnie zidentyfikować skończony zestaw testów, który wyczerpująco określa, czy implementacja testowanego systemu jest zgodna ze specyfikacją. Cel ten osiąga się dzięki podejściu „dziel i zwyciężaj”, w którym projekt jest rozkładany poprzez udoskonalenie na kolekcję Stream X-Machines , które są implementowane jako osobne moduły, a następnie testowane oddolnie. Na każdym etapie integracji metoda testowania gwarantuje, że testowane komponenty są poprawnie zintegrowane.

Metodologia przezwycięża formalne ograniczenia nierozstrzygalności , wymagając, aby podczas specyfikacji i implementacji przestrzegano pewnych zasad projektowania dla testów . Wynikająca z tego skalowalność oznacza, że ​​praktyczne systemy programowe i sprzętowe składające się z setek tysięcy stanów i milionów przejść zostały pomyślnie przetestowane.

Motywacja

Wiele testów oprogramowania ma jedynie nadzieję, polegającą na wypróbowaniu systemu oprogramowania na różne sposoby, aby sprawdzić, czy można wykryć jakiekolwiek błędy. Testowanie może rzeczywiście ujawnić pewne błędy, ale nigdy nie gwarantuje poprawności działania systemu po zakończeniu testowania. testowania funkcjonalnego mają na celu poprawę tej sytuacji poprzez opracowanie formalnej specyfikacji opisującej zamierzone zachowanie systemu, względem której następnie testowana jest implementacja (rodzaj testów zgodności ). Specyfikację można zweryfikować pod kątem wymagań użytkownika, a następnie zweryfikować być spójne i kompletne dzięki rozumowaniu matematycznemu (eliminując wszelkie logiczne wady projektowe). Kompletne testowania funkcjonalnego systematycznie wykorzystują specyfikację, generując zestawy testów, które wyczerpująco sprawdzają zaimplementowany system oprogramowania , aby określić, czy jest on zgodny ze specyfikacją. W szczególności:

• Pełne pozytywne testy: potwierdza, że ​​wszystkie pożądane zachowania są obecne w systemie;
• Pełne testy negatywne: potwierdzają, że w systemie nie występuje żadne niezamierzone zachowanie.

Ten poziom testowania może być trudny do osiągnięcia, ponieważ systemy oprogramowania są niezwykle złożone, z setkami tysięcy stanów i milionami przejść. Potrzebny jest sposób rozbicia specyfikacji i problemu testowego na części, którymi można zająć się oddzielnie.

Skalowalne, abstrakcyjne specyfikacje

Mike Holcombe po raz pierwszy zaproponował wykorzystanie teoretycznego modelu maszyny X Samuela Eilenberga jako podstawy specyfikacji oprogramowania pod koniec lat 80. Dzieje się tak, ponieważ model wyraźnie oddziela przepływ sterowania systemu od przetwarzania przeprowadzanego przez system. Na danym poziomie abstrakcji system można postrzegać jako prostą maszynę o skończonych stanach , składającą się z kilku stanów i przejść. Bardziej złożone przetwarzanie jest delegowane do funkcji przetwarzania w przejściach, które modyfikują bazowy podstawowy typ danych X. _ Później każda funkcja przetwarzania może być oddzielnie eksponowana i scharakteryzowana przez inną maszynę X , modelującą zachowanie działania tego systemu.

Obsługuje to podejście typu „dziel i zwyciężaj”, w którym najpierw określa się ogólną architekturę systemu, następnie określa się każdą główną operację systemu, a następnie podprogramy i tak dalej. Na każdym etapie poziom złożoności jest możliwy do opanowania ze względu na niezależność każdej warstwy. W szczególności inżynierom oprogramowania łatwo jest zweryfikować proste maszyny skończone pod kątem wymagań użytkownika.

Specyfikacje testowalne przyrostowo

Gilbert Laycock jako pierwszy zaproponował szczególny rodzaj maszyny X , Stream X-Machine , jako podstawę metody testowania. Zaletą tego wariantu był sposób, w jaki można było kontrolować testy. W Stream X-Machine podstawowy typ danych ma określoną postać: X = Out * × Mem × In *, gdzie In * to strumień wejściowy, Out * to strumień wyjściowy, a Mem to pamięć wewnętrzna. Przejścia Stream X-Machine są oznaczone funkcjami przetwarzania w postaci φ: Mem × In → Out × Mem , to znaczy zużywają jedno wejście ze strumienia wejściowego, prawdopodobnie modyfikują pamięć i wytwarzają jedno wyjście w strumieniu wyjściowym ( więcej szczegółów w powiązanym artykule ).

Korzyści z testowania polegają na tym, że systemy oprogramowania zaprojektowane w ten sposób są obserwowalne na każdym etapie. Dla każdego wejścia maszyna wykonuje jeden krok, wytwarzając wyjście, tak że pary wejście/wyjście mogą być dokładnie dopasowane. Kontrastuje to z innymi podejściami, w których system działa do końca (wykonując wiele kroków) przed dokonaniem jakiejkolwiek obserwacji. Ponadto warstwowe Stream X-Machines oferują wygodną abstrakcję. Na każdym poziomie tester może zapomnieć o szczegółach funkcji przetwarzania i traktować (pod)system jako prostą maszynę skończoną . Istnieją skuteczne metody testowania systemów zgodne ze specyfikacjami stanów skończonych, takie jak metoda W Chowa.

Metoda specyfikacji

Postępując zgodnie z metodologią (Stream) X-Machine, pierwszym etapem jest identyfikacja różnych typów danych, które mają być przetwarzane. Na przykład edytor tekstu będzie używał podstawowych typów Znak (wprowadzanie z klawiatury), Pozycja (pozycja kursora myszy) i Polecenie (polecenie myszy lub menu). Mogą istnieć inne skonstruowane typy, takie jak Tekst ::= Znak * (sekwencja znaków), Wybór ::= Pozycja × Pozycja (początek i koniec zaznaczenia) oraz Dokument ::= Text × Selection × Boolean (tekst, możliwy wybór i flaga sygnalizująca, czy dokument został zmodyfikowany).

Specyfikacja wysokiego poziomu

Specyfikacją najwyższego poziomu jest Stream X-Machine opisująca interakcję głównego użytkownika z systemem. Na przykład edytor tekstu będzie istniał w wielu stanach, w których naciśnięcia klawiszy i polecenia będą miały różne skutki. Załóżmy, że ten edytor tekstu istnieje w stanach { Pisanie , Wybieranie , Archiwizacja , Edycja }. Oczekujemy, że edytor tekstu uruchomi się w początkowym pisania , ale przejdzie do stanu zaznaczania , jeśli przeciągniemy mysz lub naciśniemy klawisz Shift jest przytrzymywany. Po ustaleniu wyboru powinien powrócić do pisania . Podobnie, jeśli wybrano opcję menu, powinna przejść do Edycja lub Archiwizacja . W tych stanach niektóre naciśnięcia klawiszy mogą mieć różne znaczenie. Procesor tekstu w końcu powraca do pisania , gdy dowolne polecenie menu zostanie zakończone. Ta maszyna stanów jest zaprojektowana i nieformalnie oznaczona różnymi działaniami, które powodują zmianę stanu.

Typy wejścia, pamięci i wyjścia dla maszyny najwyższego poziomu są teraz sformalizowane. Załóżmy, że typem pamięci prostego edytora tekstu jest typ Dokument zdefiniowany powyżej. Traktuje dokument jako łańcuch tekstowy, z dwiema pozycjami oznaczającymi możliwy wybór i flagą wskazującą modyfikację od ostatniego polecenia zapisu . Bardziej złożony edytor tekstu może obsługiwać edycję, której można cofnąć, z sekwencją stanów dokumentu: Document ::= ( Text × Selection )*, które są zwijane do jednego dokumentu za każdym razem, gdy wykonywane jest polecenie zapisu .

Załóżmy, że typem danych wejściowych maszyny jest: In ::= Polecenie × Znak × Pozycja . To rozpoznaje, że każda interakcja może być prostym wstawieniem znaku, poleceniem menu lub umieszczeniem kursora. Każda dana interakcja jest krotką 3, ale niektóre miejsca mogą być puste. Na przykład ( Insert , 'a', ε) oznaczałoby wpisanie znaku 'a'; while ( Position , ε, 32) oznaczałoby umieszczenie kursora między znakami 32 i 33; i ( Wybierz , ε, 32) oznaczałoby zaznaczenie tekstu pomiędzy bieżącą pozycją kursora a miejscem pomiędzy znakami 32 i 33.

Typ wyjścia dla maszyny jest tak zaprojektowany, aby na podstawie wyjścia można było określić, jaka funkcja przetwarzania została wykonana w odpowiedzi na dane wejście. Odnosi się to do opisanej poniżej właściwości rozróżnialności wyjścia .

Specyfikacja niskiego poziomu

Jeśli system jest złożony, najprawdopodobniej zostanie rozłożony na kilka Stream X-Machines . Najczęstszym rodzajem udoskonalania jest wzięcie każdej z głównych funkcji przetwarzania (które były etykietami na maszynie wysokiego poziomu) i traktowanie ich jako oddzielnych Stream X-Machines . W takim przypadku typy wejścia, pamięci i wyjścia dla maszyn niskiego poziomu będą inne niż te zdefiniowane dla maszyny wysokiego poziomu. Albo jest to traktowane jako rozszerzenie zestawów danych używanych na wysokim poziomie, albo następuje translacja z bardziej abstrakcyjnych zestawów danych na wysokim poziomie na bardziej szczegółowe zestawy danych na niższym poziomie. Na przykład polecenie Select na wysokim poziomie można rozłożyć na trzy zdarzenia: MouseDown , MouseMove , MouseUp na niższym poziomie.

Ipate i Holcombe wspominają o kilku rodzajach udoskonalenia, w tym udoskonaleniu funkcjonalnym , w którym zachowanie funkcji przetwarzających jest omówione bardziej szczegółowo, oraz udoskonaleniu stanu , w którym prosta przestrzeń stanów jest podzielona na bardziej złożoną przestrzeń stanów. Ipate dowodzi, że te dwa rodzaje wyrafinowania są ostatecznie równoważne

Inaczej systemy są specyfikowane aż do poziomu, na którym projektant jest gotowy zaufać prymitywnym operacjom wspieranym przez środowisko implementacyjne. Możliwe jest również wyczerpujące badanie małych jednostek za pomocą innych metod badawczych.

Warunki projektowe do testów

Metodologia (Stream) X-Machine wymaga od projektanta przestrzegania określonego projektu pod kątem warunków testowych. Zazwyczaj nie są one zbyt trudne do spełnienia. Dla każdego Stream X-Machine w specyfikacji musimy uzyskać:

• Minimalna specyfikacja : specyfikacja musi być minimalną maszyną skończoną . Oznacza to, że maszyna stanów nie powinna zawierać stanów zbędnych, to znaczy stanów, w których obserwowalne zachowanie przejścia jest identyczne z zachowaniem w innym stanie.
• Specyfikacja deterministyczna : Dla każdego stanu maszyny co najwyżej jedna z funkcji przetwarzania φ powinna być włączona dla bieżącej pamięci i następnej wartości wejściowej. Gwarantuje to, że wymagane zachowanie do przetestowania jest przewidywalne.
• Kompletność testu : Każda funkcja przetwarzania φ musi być wykonywalna dla co najmniej jednego wejścia, w odniesieniu do wszystkich stanów pamięci. Zapewnia to brak zakleszczeń, w których maszyna jest blokowana przez aktualny stan pamięci. Aby zapewnić kompletność testów, dziedzinę funkcji φ można rozszerzyć o specjalne wejścia testowe , które są używane tylko podczas testowania.
• Odróżnialność danych wyjściowych : Musi być możliwe rozróżnienie, która funkcja przetwarzania została wywołana, na podstawie samej wartości wyjściowej dla wszystkich par pamięć-wejściowa. Zapewnia to, że maszyna stanów może być oddzielona od funkcji przetwarzania. Aby zapewnić rozróżnialność danych wyjściowych, koddomena funkcji φ może zostać rozszerzona o specjalne wyniki testowe , które są istotne tylko podczas testowania.

Maszyna minimalna to maszyna z najmniejszą liczbą stanów i przejść dla określonego zachowania. Minimalizacja specyfikacji po prostu zapewnia, że ​​zestawy testowe są tak małe, jak to tylko możliwe. Deterministyczna maszyna jest wymagana dla systemów, które są przewidywalne. W przeciwnym razie implementacja mogłaby dokonać arbitralnego wyboru dotyczącego przejścia. Niektóre ostatnie prace złagodziły to założenie, aby umożliwić testowanie maszyn niedeterministycznych.

Kompletność testów jest potrzebna, aby upewnić się, że implementacja jest testowalna w możliwym do wykonania czasie. Na przykład, jeśli system ma odległe lub trudno dostępne stany, które są wprowadzane dopiero po osiągnięciu przez pamięć określonej wartości granicznej, wówczas należy dodać specjalne wejścia testowe, aby umożliwić ominięcie pamięci, zmuszając maszynę stanów do odległego państwo. Pozwala to na szybkie pokrycie wszystkich (abstrakcyjnych) stanów podczas testowania. Rozróżnialność wyników jest kluczową właściwością wspierającą skalowalną metodę testowania. Pozwala to testerowi traktować funkcje przetwarzania φ jako proste etykiety, których szczegółowe zachowanie można bezpiecznie zignorować podczas testowania maszyny stanów kolejnej warstwy integracji. Unikalne dane wyjściowe są wartościami świadków, które gwarantują, że została wywołana określona funkcja.

Metoda testowania

(Stream) X-Machine Testing Method zakłada, że ​​zarówno projekt, jak i implementacja mogą być traktowane jako (zbiór) Stream X-Machines . Dla każdej pary odpowiednich maszyn ( Spec , Imp ) celem testowania jest określenie, czy zachowanie Imp , maszyny implementacji, dokładnie odpowiada zachowaniu Spec , maszyny specyfikacji. Zauważ, że Imp nie musi być maszyną minimalną - może mieć więcej stanów i przejść niż Spec i nadal zachowywać się w identyczny sposób.

Aby przetestować wszystkie zachowania, musi być możliwe wprowadzenie maszyny we wszystkie jej stany, a następnie wypróbowanie wszystkich możliwych przejść (tych, które powinny się powieść i tych, które powinny zostać zablokowane), aby uzyskać pełne pozytywne i negatywne testy ( patrz wyżej ) . W przypadku pomyślnych przejść należy również zweryfikować stan docelowy. Zauważ, że jeśli Spec i Imp mają taką samą liczbę stanów, powyższe opisuje najmniejszy zestaw testów, który osiąga cel. Jeśli Imp ma więcej stanów i przejść niż Spec , potrzebne są dłuższe sekwencje testowe, aby zagwarantować, że nadmiarowe stany w Imp również zachowują się zgodnie z oczekiwaniami.

Testowanie wszystkich stanów

Podstawą strategii generowania testów jest W-Metoda Tsuna S. Chowa do testowania automatów skończonych, wybrana, ponieważ wspiera testowanie redundantnych implementacji. Metoda Chowa zakłada proste maszyny o skończonych stanach z obserwowalnymi wejściami i wyjściami, ale bez bezpośrednio obserwowalnych stanów. Aby odwzorować na formalizm Chowa, funkcje φ _i na przejściach Stream X-Machines są traktowane po prostu jako etykiety (dane wejściowe, w terminach Chowa), a wyróżniające wyjścia są używane bezpośrednio. (Później mapowanie z rzeczywistych danych wejściowych i pamięci ( mem , in ) jest wybierany do wyzwalania każdej funkcji φ, zgodnie z jej dziedziną).

Aby zidentyfikować określone stany w Imp , Chow wybiera zestaw charakterystyki W , najmniejszy zestaw sekwencji testowych, który jednoznacznie charakteryzuje każdy stan w Spec . Oznacza to, że rozpoczynając w danym stanie, wykonywanie sekwencji w W powinno przynieść co najmniej jedną zauważalną różnicę w porównaniu do rozpoczynania w jakimkolwiek innym stanie.

Aby osiągnąć każdy stan oczekiwany w Spec , tester konstruuje pokrycie stanu C , najmniejszy zestaw sekwencji testowych, który osiąga każdy stan. Można to skonstruować przez automatyczną eksplorację wszerz Spec . $gdzie$ testowy, który sprawdza wszystkie stany minimalnego $Impa$ to wtedy: oznacza połączony iloczyn zestawów Na przykład, jeśli C = { ⟨ a ⟩ , ⟨ b ⟩ ${\ Displaystyle C \ czasami W=\{\langle ac\rangle ,\langle ad\rangle ,\langle bc\rangle ,\langle bd\rangle \}}$ i W = { ⟨ do ⟩ , ⟨ re ⟩ }, a następnie .

Testowanie wszystkich przejść

Powyższy zestaw testów określa, czy minimalny Imp ma takie same stany jak Spec . Aby określić, czy minimalny chochlik ma takie samo zachowanie przejścia jak Spec , tester konstruuje osłonę przejścia K . Jest to najmniejszy zestaw sekwencji testowych, który osiąga każdy stan, a następnie raz podejmuje próbę każdego możliwego przejścia z tego stanu. Teraz alfabet wejściowy składa się z (etykiet) każdej funkcji φ w Φ. Skonstruujmy zbiór ciągów testowych o długości-1, składający się z pojedynczych funkcji wybranych z Φ i nazwijmy to Φ ₁ . Osłona przejściowa jest zdefiniowana jako $\ Displaystyle K: = C \ kubek C \ otimes \ Phi _ {1}$ }

Spowoduje to próbę każdego możliwego przejścia z każdego stanu. W przypadku tych, które się powiodą, musimy zweryfikować stany docelowe. Tak więc najmniejszy zestaw testów T ₁ , który całkowicie potwierdza zachowanie minimalnego chochlika , jest określony wzorem: ${\ Displaystyle T_ {1}:: = C \ otimes W\cup C\otimes \Phi _{1}\otimes W}$ . Formułę tę można przekształcić w następujący sposób:

${\ Displaystyle T_ {1}:: = C \ czasami \ lewo (\ Phi _ {0} \ kubek \ Phi _ {1} \ prawo) \ czasami W}$ ,

₀ gdzie Φ jest zbiorem zawierającym pustą sekwencję { ⟨⟩ }.

Jeśli Imp ma więcej stanów niż Spec , powyższy zestaw testów może nie być wystarczający do zagwarantowania zgodnego zachowania replikowanych stanów w Imp . Wybierane są więc zestawy dłuższych ciągów testowych, składające się ze wszystkich par funkcji Φ ₂ , wszystkich trójek funkcji Φ ₃ aż do pewnej granicy Φ _k , gdy tester jest przekonany, że Imp nie może zawierać łańcuchów zduplikowanych stanów dłuższych niż k -1 . Ostateczna formuła testu jest dana przez:

${\ Displaystyle T _ {\ operatorname {k}}:: = C \ otimes \ lewo (\ Phi _ {0} \ kubek \ Phi _ {1}\ldots \cup \Phi _{\mathrm {k} }\right)\otimes W}$ .

Ten zestaw testów całkowicie sprawdza zachowanie nieminimalnego chochlika , w którym oczekuje się, że łańcuchy zduplikowanych stanów nie będą dłuższe niż k -1. Z praktycznego punktu widzenia testowanie do k = 2 lub k = 3 jest dość wyczerpujące i ujawnia wszystkie błędy związane ze stanem w naprawdę słabych implementacjach.