Test af tilstandsmaskiner
Indhold:
- Transition testing: FSM baseret test generering
- Fault models,
- Distinguishing Sequences
- Coverage: Transition, state,...
Litteratur
- Design and Validation of Computer Protocols
by Gerard J. Holzmann chapter
9 ( further backgropund
chapter 8)
Øvelser
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.
- 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).
- 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?
- 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?
- Lav en transitionstour for din abstrake E-FSM
- 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?
- Conformer flg "elevator" implementation (elevator.c,
elevator.h) med din specifikation?
Implementer og afprøv dine test cases.
- Lav modellen i Uppaal og brug den til at generere test suiter, der dække
hhv. states og transitioner i den abstrakte model.
Med Venlig Hilsen
Arne & Brian