Java alkalmazások hibatűrési tulajdonságainak vizsgálata Java Pathfinderrel

A Java Pathfinder (http://babelfish.arc.nasa.gov/trac/jpf) egy nyílt forráskódú, speciális JVM, mely lehetővé teszi Java alkalmazások (többek között) modellellenőrzését (http://en.wikipedia.org/wiki/Model_checking). Alkalmazások, illetve specifikációjuk helyességének ellenőrzésére ma már bevett gyakorlat modellellenőrzési technikák alkalmazása; jórészt nyílt kérdés azonban, hogy hogyan alkalmazhatjuk a modellellenőrzést a diagnosztikai modellezés támogatására és különböző hibatűrési mechanizmusok tervezésére. Az önálló feladat célja az eszközzel és képességeivel való megismerkedés, majd ezen kérdések vizsgálata az eszköz kontextusában.