Automatikus tesztgenerálás modell ellenőrzővel

Testing is an essential, but time and resource consuming activity in the software development process. Generating a short, but effective test suite usually needs a lot of manual work and expert knowledge. In a modelbased process, among other subtasks, test construction and test execution can also be partially automated. Based on the method suggested in [1], this paper presents a test generator tool, which can be used for test set generation in the development process of event-driven embedded systems. For a selected test coverage criterion and from the UML statechart model of the system the program generates test cases using the SPIN model checker. The test generator tool supports currently the test sequence construction on the basis of the “all states” and “all transitions” coverage criteria. The necessary model transformation [2] and requirement generation steps are performed automatically. The configuration of the model checker in the case of test generation, namely the settings required for constructing a short and minimal test suite, differs from the usual needs of classic model checking problems. The paper analyzes the possible settings of the model checker SPIN by measuring the efficiency of test construction in the case of different real-life statechart models, and introduces an optimized setting for test generation. The test generator is extended for real-time applications, in this case the model is available in the form of timed automata, and the model checker to be used is Uppaal [3]. A tesztelés a szoftverfejlesztés lényeges, ámde időés erőforrás-igényes része. Rövid, ugyanakkor hatékony tesztek generálása komoly tudást és rengeteg emberi munkát igényel. Modell-alapú fejlesztés esetén viszont, egyéb részfeladatok mellett, a tesztek előállítása és végrehajtása is részben automatizálható. A dolgozat bemutat egy tesztgeneráló eszközt, ami az [1] cikkben javasolt módszer alapján eseményvezérelt rendszerekhez készít tesztsorozatokat. A rendszer UML állapottérkép modelljéből kiindulva egy megadott fedési kritérium alapján a SPIN modell ellenőrző eszközt használja a teszt generáláshoz. Jelenleg a „minden állapot” és a „minden tranzíció” fedési kritériumok használhatóak, de az eszköz könnyedén bővíthető más, az irodalomban javasolt kritériummal is. A modell ellenőrző használatához szükséges modell transzformáció [2] és a követelmények temporális logikával való megfogalmazása automatikus. A modell ellenőrző azonban tesztgenerálás esetén más beállításokat igényel, mint a klasszikus verifikációs feladatoknál. Elég egy darab ellenpéldát találni, de az lehetőleg minél rövidebb legyen. A dolgozat megvizsgálja a SPIN modell ellenőrző különböző konfigurációs lehetőségeit, és valós életbeli állapottérképeken elvégzett mérések segítségével meghatároz egy optimalizált beállítást. Az eszköz kiterjeszthető valós-idejű alkalmazásokhoz is, ilyenkor az Uppaal [3] modell ellenőrzőt és időzített automatákat használ a tesztek generálásához.