Abstrakt
Model checking kódu je rychle se vyvýjející výzkumné téma. Nicméně, kromě velice omezených scénářů (např. verifikace device driverů SLAMem), nástroje pro model checking kódu nejsou široce používány během skutečného vývojového procesu.
Věříme, že toto je možné změnit pokud by vývojáři mohli používat tyto nástroje stejně jako již běžně používají nástroje testovací. Představujeme nástroj UnitCheck , který obohacuje standardní unit testování Javy o model checking.
Vývojář zvyklý na unit testování může tento nástroj použít na standardní unit testy a těžit z vyčerpávajícího průchodu vykonaného model checkerem, použitého v UnitChecku. UnitCheck plugin pro Eclipse vizualizuje výsledky verifikace ve srozumitelné podobě známe z unit testování, ale nabízí také detailní výstup pro zkušené uživatele.