Méréstechnika és Információs Rendszerek Tanszék
Automatikus tesztgenerálás modell ellenőrző segítségével Micskei Zoltán műszaki informatika, V.
Konzulens: Dr. Majzik István
Tesztelés z z
z
Célja: a rendszerben lévő hibák megtalálása Módszer: reprezentatív tesztesetek futtatása, és az eredmények összevetése a tesztesetben eltárolt várt kimenettel Problémák a klasszikus tesztelési módszerekkel: z z z
Sok energia kézzel előállítani a teszteseteket. A kész kódhoz készített tesztek nem garantálják a követelményeknek megfelelő működést. Könnyű kihagyni lényeges teszteseteket. Automatikus tesztgenerálás modell ellenőrzővel
2
Modell alapú fejlesztés Modell Modellellenőrzés ellenőrzés
Rendszermodell Rendszermodell (specifikáció) (specifikáció)
Kódgenerálás Kódgenerálás
Tesztelés Tesztelés
Specifikációnak megfelelő tesztek Automatikus tesztgenerálás modell ellenőrzővel
3
Beágyazott rendszerek modellezése
z z z
Vezérlésorientált működés Esemény – válasz Állapottérkép használata a modellezéshez (UML, STATEMATE) Automatikus tesztgenerálás modell ellenőrzővel
4
Rendszerek ellenőrzése: modell ellenőrző eszközök z
z z
A rendszer állapotterének teljes bejárásával ellenőrzik bizonyos tulajdonságok meglétét A helyes működés bizonyítására szolgálnak Tipikus feladatok: z z
Élőség és holtpontmentesség vizsgálata Egyedi, rendszerspecifikus kritériumok megadása z z
Állapotok, események elérhetősége, sorrendje Általában temporális logikai formulákkal
Automatikus tesztgenerálás modell ellenőrzővel
5
Modell alapú tesztelési módszerek Rendszermodell Rendszermodell Fedés Fedésmeghatározása meghatározása Kritérium Kritérium
Generálás Generálás Konformancia Konformanciatesztelése tesztelése
Teszt Tesztorákulum orákulum
Automatikus tesztgenerálás modell ellenőrzővel
Implementáció Implementáció
6
Tesztgenerálás modell ellenőrzővel z
Az állapottér bejárása: z z
z
Szabványos fedési kritérium alapján Tesztelő által megadott kritérium alapján
Tipikus kritériumok: z z z
Állapotok, átmenetek lefedése Változó definiálások és felhasználások lefedése Be- és kimenő átmenet-párok lefedése egy-egy állapothoz Automatikus tesztgenerálás modell ellenőrzővel
7
Hogyan használható a modell ellenőrző teszt generálásra?
keyNo
LineOk Error
PoweOff keyYes
Ready
LineWeak
Automatikus tesztgenerálás modell ellenőrzővel
8
Hogyan használható a modell ellenőrző teszt generálásra?
keyNo
LineOk Error
PoweOff keyYes
LineWeak
Kritérium megadása: A LineWeak állapotot soha sem lehet Ready elérni. ! (F in_LineWeak)
Automatikus tesztgenerálás modell ellenőrzővel
9
Hogyan használható a modell ellenőrző teszt generálásra?
keyNo
LineOk Error
PoweOff keyYes
Kritérium ellenőrzése modell ellenőrzővel. Ready
LineWeak
Eredmény: a kifejezés nem igaz! Automatikus tesztgenerálás modell ellenőrzővel
10
Hogyan használható a modell ellenőrző teszt generálásra?
keyNo
LineOk Error
PoweOff keyYes
Az eszköz ezzel az ellenpéldával demonstrálja, hogy a tulajdonság nem teljesül, az állapot elérhető. Ready
LineWeak
Ez viszont pontosan egy, a LineWeak állapotot lefedő teszteset! Automatikus tesztgenerálás modell ellenőrzővel
11
Automatikus tesztgenerálás Mérnöki Mérnöki modell modell
Matematikai Matematikai modell modell Modell Modell ellenőrző ellenőrző
Tesztelési Tesztelési kritériumok kritériumok
Teszteset Teszteset
TL TLformula formula
Automatikus tesztgenerálás modell ellenőrzővel
12
A működés menete – I. Mérnöki Mérnöki modell modell
Matematikai Matematikai modell modell Modell Modell A rendszer modellj ét egy ellenőrző ellenőrző modell ellenőrző bemeneti nyelvére transzformáljuk.
Tesztelési Tesztelési kritériumok kritériumok
Teszteset Teszteset
TL TLformula formula
Automatikus tesztgenerálás modell ellenőrzővel
13
A működés menete – II. Mérnöki Mérnöki modell modell
Tesztelési Tesztelési kritériumok kritériumok
Matematikai MatematikaiA fedési kritériumokat modell modell temporális logikai formulákkal fogalmazzuk meg. Például: Legyen minden Modell Modell egyes állapot lefedve Teszteset Teszteset ellenőrző ellenőrző tesztek által. TL TLformula formula
Automatikus tesztgenerálás modell ellenőrzővel
14
A működés menete – III. Mérnöki Matematikai Mérnöki Matematikai Olyan fut á st modell modell modell modell akarunk, ahol teljesül a kritérium, ezért a formula Modell Modell negáltját ellenőrző ellenőrző ellenőriztetjük. Tesztelési Tesztelési kritériumok kritériumok
Teszteset Teszteset
TL TLformula formula
Automatikus tesztgenerálás modell ellenőrzővel
15
A működés menete – IV. Mérnöki Mérnöki modell modell
Matematikai Matematikai modell modell Modell Modell ellenőrző ellenőrző
Tesztelési Tesztelési kritériumok kritériumok
Teszteset Teszteset
TL TLformula formulaA kiadódó ellenpéldák egy-egy tesztesetet adnak meg. Automatikus tesztgenerálás modell ellenőrzővel
16
Implementáció z
Tesztgeneráló program készült: z z
z
A módszer működésének demonstrálása Hatékonyság vizsgálata
Működési lépései: z z
z z
TL kifejezések generálása a fedési kritériumból Rendszermodell transzformálása a modell ellenőrző bemeneti nyelvére Modell ellenőrző paraméterezése, kifejezések ellenőrzése Kimenet szűrése, és a tesztesetet leíró fájl előállítása
Automatikus tesztgenerálás modell ellenőrzővel
17
Implementált környezet UML UML állapottérkép állapottérkép
Promela Promela leírás leírás SPIN SPINmodell modell ellenőrző ellenőrző
Fedési Fedési kritériumok kritériumok
XML XML Teszteset Teszteset
LTL LTLformula formula
Automatikus tesztgenerálás modell ellenőrzővel
18
Tesztgenerátor osztálydiagram
Automatikus tesztgenerálás modell ellenőrzővel
19
Generált kimenet példa teszteset Megadja, hogy mit fed le a teszteset
A tesztesethez tartozó eseményszekvencia
Automatikus tesztgenerálás modell ellenőrzővel
20
Generált kimenet példa teszteset XSLT segítségével HTML formátumra alakítva
Automatikus tesztgenerálás modell ellenőrzővel
21
Optimalizáció z
z
A tesztgenerálás célja minél gyorsabban, minél rövidebb ellenpéldát találni → speciális beállítások szükségesek. Lehetőségek: z z z
SPIN-ben a felesleges ellenőrzések letiltása Megfelelő mélységkorlát definiálása Állapotokat tároló hash-tábla méretének helyes megadása Automatikus tesztgenerálás modell ellenőrzővel
22
Mobile példa: Teljes állapotfedésű tesztek z z
Mobiltelefon vezérlését leíró állapottérkép 10 darab állapot, 21 darab átmenet
Automatikus tesztgenerálás modell ellenőrzővel
23
Duál automatika példa z z z z
Valós protokoll 5 darab objektum, 31 állapot, 174 átmenet Komoly feladat, 2e+08 bejárandó állapot Más technikák is kellenek: z z z z
Állapottér tárolás tömörítve Közelítő módszer alkalmazása (bitstate hashing) Szűkítések a modellben: csatorna méret csökkentés Korábban lefedett kritériumok kihagyása Automatikus tesztgenerálás modell ellenőrzővel
24
Duál automatika példa – Teljes állapotfedésű tesztek
Automatikus tesztgenerálás modell ellenőrzővel
25
Kiterjesztések z
Tesztkészlet optimalizálás z
z
z
Legrövidebb/legkisebb tesztkészlet kiválasztása NP-teljes probléma További heurisztikák alkalmazása: „mélyen” fekvő állapotok előbb, állapottér levágása
Illesztés CASE eszközökhöz z
Teszt menedzselő és futtató keretrendszerek pl. Rational TestManager Automatikus tesztgenerálás modell ellenőrzővel
26
Valósidejű rendszerek
Speciális modell ellenőrző, Uppaal: • Időzített automaták használata Automatikus tesztgenerálás modell ellenőrzővel
27
Valósidejű rendszerek
Óra típusú változók: Valós időt, időzítési feltételeket modellezhetünk
Automatikus tesztgenerálás modell ellenőrzővel
28
Generált tesztek State: A teszt időzítési ( input.sending mobile.PowerOn mobile1.LineOK mobile2.CallWait ) viszonyok#depth=5 is t=0 inputEvent=28 outputEvent=14 in_PowerOn=1 Delay: 6
szerepelnek a generált tesztesetben
State: ( input.sending mobile.PowerOn mobile1.LineOK mobile2.CallWait ) t=6 inputEvent=28 outputEvent=14 in_PowerOn=1 #depth=5 Transitions: input.sending->input.sendInput { 1, inputChannel!, 1 } mobile2.CallWait->mobile2.VoiceMail { inputEvent == evKeyYes && t > 5 && in_PowerOn, inputChannel?, 1 } Automatikus tesztgenerálás modell ellenőrzővel
29
Eredmények összefoglalása z z
z z z z
Modell alapú tesztelés támogatása Automatikus tesztgeneráló eszköz eseményvezérelt, beágyazott rendszerekhez: tesztek (bejárási útvonalak) generálása Többféle teszt fedési kritérium figyelembe vétele Teszt időzítés automatikus generálása valósidejű rendszerek esetén Modell ellenőrző teszt-specifikus paraméterezése Méretkorlát: A modell ellenőrző képességei (kb. 108 állapot) Automatikus tesztgenerálás modell ellenőrzővel
30
Köszönöm a figyelmet!
Kérdések Automatikus tesztgenerálás modell ellenőrzővel
