Seminarium: Systemy Rozproszone
29 listopada 2007, godzina 12:15, sala 3120
Michał Kurzydłowski


Weryfikacja modelowa - BLAST



Wszyscy wiemy lub przynajmniej się domyślamy jak trudnym i niewdzięcznym zadaniem jest testowanie programów, szczególnie tych największych jakimi są np. sterowniki Linux'owe. Na szczęście istnieją narzędzia, które mają na celu (przynajmniej częściowe) wyręczenie programisty poprzez wyszukiwanie w kodzie źródłowym instrukcji, które mogą stanowić potencjalne zagrożenie systemu i to bez potrzeby kompilacji i uruchamiania samego oprogramowania.

W ramach prezentacji postaram się przedstawić metodę analizy kodu źródłowego, jakim jest weryfikacja modelowa oraz zaprezentować wyniki analizy przydatności popularnego narzędzia o nazwie BLAST, pisane z punktu widzenia programisty praktykanta (autora referowanego artykułu). Pokazują one jak dużo pozostaje jeszcze do zrobienia by rozwijane niekomercyjnie narzędzia do weryfikacji stały się na tyle wygodne by zachęcić do siebie deweloperów Linuxa.


Ważne linki:

Zapraszam.
Michał Kurzydłowski