Unit checking for Java IDE

Model checking programů představuje rychle se rozvíjejích oblast výzkumu. Bohužel tato technika zatím není kromě několika speciálních případů (např. veri fikace ovladačů pomocí nástroje SLAM) příliš rozšířena ve standardním procesu vývoje software. Věříme ovšem, že by mohla nastat změna, pokud by vývojáři měli možnost používat nástroje z oblasti techniky model checking podobným způsobem jako používají nástroje pro testování. Tato práce prezentuje nátroj UnitCheck, který doplňuje standardní testování Java tříd (unit testing) o metodu model checking. Vývojáři, kteří běžně využívají unit testování, mohou tento nástroj aplikovat na standardní testovací scénáře a díky části provádějící model checking (model checker) integrované v nástroji UnitCheck tak využít možnost průchodu celým stavovým prostorem daného testu. UnitCheck v sobě integruje dva dobře známé nástroje z oblasti programování v jazyce Java. JUnit je použit jako testovací framework, zatímco Java PathFinder umožňuje provádět model checking vstupních testů. Součástí celého nástroje je plugin pro prostředí Eclipse, který přehledně zobrazuje výsledky testů způsobem známým z unit testování a pokročilým uživatelům zároveň umožňuje prohlédnout si podrobnšjší informace. UnitCheck je také integrován do nástroje Ant, což umožňuje spouštět kontrolu testů (unit..