Test af tilstandsmaskiner og objekter

Indhold:

• Transition testing: FSM baseret test generering
• Fault models,
• Distinguishing Sequences
• Coverage: Transition, state,...
•  

Litteratur

1. Design and Validation of Computer Protocols by Gerard J. Holzmann chapter 8 and chapter 9 . (Essential)
2. ((From previous lectures
   • Holger Hermanns: Lecture notes on system validation using model-checking, chapter 1
   • Timed Automata: Semantics, Algorithms and Tools. [BW04].
   • Tutorial on Uppaal. Revised and extended version of [BDL04].  UppAal in A NutShell, Uppaal2k Tutorial
     ))

Øvelser

1. Betragt et simpel elevator kontrol system, det betjener et højhus med 5 etager 0-4, her implementeret som en simpel c++ klasse, har følgende interface:

class Elevator{ 

 public:

  Elevator();

  floor_t nextFloor();

  void request(floor_t floor);

	//test helpers

	ElevatorState status();

	void setState (ElevatorState s);

	void reset();

};

Brugeren kan requeste service på et kontrolpanel på en given etage eller i selve elevatoren. Begge dele resulterer i at elevatoren registrerer via request(floor) at den skal flytte sig til den pågældende etage.Elevatoren begynder (den præcise mekanisme udeladt) at servicere anmodningerne, når nextFloor kaldes. Den returnerer det etage som elevatoren har standset ved.  Elevatoren kan ikke i dette simple eksempel modtage nye requests mens den flytter sig. Elevatoren servicerer requests efter følgende algoritme:

• Elevatoren servicerer alle requests der er indløbet i retning af den nuværende bevægelses retning (op eller ned)
• Elevatoren vender bevægelsesretning, når der ikke er flere requests i nuværende retning, og der er udestående requests i modsatte retning.

1. Opskrive et antal scenarier (sekvenser af kald til request og next floor), evt som sekvensdiagram, du vil bruge til at teste implementationen med, og oversæt disse til unit test-cases (som kun bruger nextFloor og request metoderne).  
2. Hvilken tilstand vil du mene at en elevator implementation vil indeholde? Hvor stort er det totale tilstandsrum? Hvad hvis elevatoren havde 100 etager? Hvilket problem udgør dette hvis du skal lave en udtømmende test, der garanterer korrekt implementatiion?
3. Lav en abstrakt E-FSM model af elevatoren (først på papir/tavle). For at få modellen abstrakt er det vigtigt at abstrahere over antallet af etager. Prøv at bruge teknikkerne fra black-box testing og inddel tilstandsrummet for elevatoren i ækvivalensklasser. Hvilke abstrakte inputs skal der til? Hvordan kan de realiseres konkret?
4. Lav en transitionstour for din abstrake E-FSM
5. Lav transitionstest for din abstrakte E-FSM; dvs test hver transition for sig. Hvordan vil test-cases se ud uden brug af test-helper funktionerne, og med test-helper funktionerne?
6. Conformer flg "elevator" implementation (elevator.c, elevator.h) med din specifikation? Implementer og afprøv dine test cases.
7. Lav modellen i Uppaal og brug den til at generere test suiter, der dække hhv. states og transitioner i den abstrakte model. 

1. Find ved håndkraft en (gerne korteste) transitionsdækkende sekvens for denne udgave at speedControl componenten. Brug herefter UppAal til at finde den korteste!

Med Venlig Hilsen

Arne & Brian