Java Atomicity Violation Detector & Healer

Nástroj pro detekci a opravu chyb v atomicitě programů

software

K využití výsledku jiným subjektem je vždy nutné nabytí licence

Poskytovatel licence na výsledek nepožaduje licenční poplatek

Letko Zdeněk, Ing., Ph.D. (CK-SZZ)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Křena Bohuslav, Ing., Ph.D. (UITS)

Atomicity Violation, Data Races, Detector, Healer, Java

Java Race Detector & Healer (http://www.fit.vutbr.cz/research/groups/verifit/tools/racedetect/) je počítačový software vytvořený v programovacím jazyce Java. Využitím nástroje pro statickou analýzu  (http://pmd.sourceforge.net/)FindBugs (http://findbugs.sourceforge.net/) detekuje části kódu, které mají být vykonávány atomicky. Prostřednictvím nástroje IBM ConTest (http://www.haifa.il.ibm.com/projects/verification/contest/index.html) následně monitoruje aplikaci a detekuje porušení atomicity i časově závislé chyby. Pro některé typy chyb je schopen automaticky vložit do běhu uživatelské aplikace synchronizační prostředky, které zabrání projevu této chyby.  Pro svůj běh vyžaduje prostředí Java 5 a nástroj IBM ConTest.

Nástroj i dokumentaci lze získat na URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/racedetect/

Licenční podmínky pro užití nástroje jsou dosupné na URL nástroje:

Metody a nástroje pro automatizované odhalování softwarových chyb, GAČR, Postdoktorandské granty, GP102/06/P076, 2006-2008, ukončen
Pokročilé formální přístupy v návrhu a automatické verifikaci počítačových systémů, GAČR, Standardní projekty, GA102/07/0322, 2007-2009, ukončen
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, 2007-2013, řešení

Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)

Ústav inteligentních systémů (UITS)