Snaha minimalizovat výskyt chyb v počítačových programech je velmi aktuální téma, jak v komerční, tak v akademické sféře. Chyby, které se nepodaří najít a odstranit před jejich reálným nasazením, přitom mohou způsobit velké ekonomické ztráty, a dokonce i ztráty na lidských životech – příkladem mohou být dvě havárie letadla Boeing 737 MAX v letech 2018 a 2019, kde chyba v počítačovém systému způsobila špatnou ovladatelnost stroje a jeho pád.
Zájem o automatizované techniky odhalování chyb proto roste ve všech sférách průmyslu, což stimuluje intenzivní vývoj nových metod a nástrojů pro hledání chyb. „Verifikace a hledání chyb v pokročilém softwaru“ bylo i tématem projektu vědců pod vedením prof. Ing. Tomáše Vojnara, Ph.D., z Fakulty informačních technologií Vysokého učení technického v Brně a doc. RNDr. Jana Kofroně, Ph.D., z Matematicko-fyzikální fakulty Univerzity Karlovy. Projekt byl financován Grantovou agenturou České republiky.
„Automatické hledání chyb v programech je velmi těžký problém a v úplné obecnosti lze říci, že víme, že nemůže existovat automatický nástroj, který by v libovolném programu našel všechny chyby. V některých programech je hledat a případně nalézt chyby snazší, v jiných je to velmi těžké, a typicky se to odvíjí od složitosti a velikosti analyzovaného programu. Naším cílem je v tomto směru zejména (i když nejen) první zmíněný aspekt, tedy umožnit analyzování složitějších programů, než jaké bylo možné analyzovat doposud,“ vysvětluje profesor Tomáš Vojnar.
Záhadné chyby v programech
Vědci se ve svém projektu zabývali například analýzou a verifikací paralelních programů, které jsou v současné době velmi populární. Udržet „na uzdě“ řadu současně běžících výpočtů však není snadné a vznikají při tom „záhadné“ chyby, kdy program většinou běží správně a pak neočekávaně selže. „Najít takové chyby, respektive garantovat jejich absenci v reálných programech představuje jeden ze zvláště obtížných problémů pro automatickou verifikaci,“ říká profesor Tomáš Vojnar.
Další oblastí, kterou se vědci zabývali, byly programy s tzv. dynamickými datovými strukturami vázanými ukazateli. „V tomto případě je zapotřebí efektivně pracovat s nekonečnými množinami složitých grafových struktur neomezené velikosti. Pro takové a další podobné problémy, jako např. automatická analýza výkonnosti programů, bylo zapotřebí navrhnout nejen vhodné formální nástroje z oblastí automatů či logik, umožňující modelovat chování analyzovaných programů, ale také efektivní algoritmy pro práci s takovými modely. Tyto algoritmy následně prototypově implementovat a ověřit na vhodných případových studiích,“ uvádí doc. Jan Kofroň.
Při řešení projektu si výzkumníci mimo jiné „vlastnoručně“ ověřili, že velmi jednoduché techniky jsou mnohdy efektivnější než přístupy výrazně složitější. „V našem případě se to projevilo například u použití poměrně jednoduchých úprav formulí jedné z logik používaných při verifikaci před jejich dalším zpracováním,“ vysvětlil Vojnar.
Metody automatizovaného hledání chyb se zdokonalují, ale vyhráno není
V průběhu projektu se vědcům podařilo vyvinout a implementovat metody, které skutečně přispěly k rozšíření skupiny programů, které je možné analyzovat. Tyto metody byly implementovány v prototypech softwarových nástrojů, které je možno experimentálně nasadit i v praxi.
„Některé z našich metod vyvinutých v projektu byly implementovány v dynamickém analyzátoru ANaConDA určeném pro odhalování chyb v paralelních programech. Při experimentálním nasazení v jedné velké nadnárodní společnosti zabývající se vývojem vestavěných zařízení pak pomohly nalézt reálné chyby, o jejichž existenci společnost tušila, ale měla problém je konkrétně identifikovat,“ uvedl jako příklad z praxe profesor Tomáš Vojnar. Podle něj to ovšem neznamená, že by tímto byl problém hledání chyb v programech vyřešen. Výzkum v této oblasti nadále pokračuje a dochází k dalšímu vývoji a vylepšování existujících metod.
Projekt prof. Tomáše Vojnara a doc. Jana Kofroně byl řešen po dobu tří let a podílelo se na něm 12 výzkumných pracovníků ze dvou spolupracujících týmů (FIT VUT a MFF UK) a asi 20 studentů, převážně doktorských studijních programů. „Pro studenty je účast na projektu cennou zkušeností, kdy si mohou vyzkoušet vývoj prakticky použitelných prototypů, stejně jako vývoj nových, prakticky motivovaných metod analýzy programů,“ říká Jan Kofroň.
Publikace výsledků projektu získaly několik ocenění. Například článek o výše zmíněném nástroji ANaConDA, jehož hlavním vývojářem je Ing. Jan Fiedor, Ph.D., z projektového týmu z FIT VUT, získal cenu za nejlepší článek o nástroji na prestižní konferenci ISSTA 2018 (27th ACM SIGSOFT International Symposium on Software Testing and Analysis). Ocenění za nejlepší článek získali vědci také na významné konferenci CADE 2019 (27th International Conference on Automated Deduction), na kterém se významně podíleli Ing. Vojtěch Havlena, Ing. Ondřej Lengál, Ph.D. a Mgr. Lukáš Holík, Ph.D. rovněž z projektového týmu z FIT VUT.
Prof. Ing. Tomáš Vojnar, Ph.D.
Profesor Tomáš Vojnar působí na Fakultě informačních technologií Vysokého učení technického v Brně (FIT VUT), kde absolvoval inženýrské i doktorské studium a aktuálně zde působí jako proděkan pro vědu a výzkum. Po dokončení doktorského studia pobýval dva roky v laboratoři LIAFA (nyní IRIF) na Université Paris Diderot v Paříži. Zabývá se metodami automatizované statické i dynamické analýzy a verifikace, formální analýzy a verifikace a také souvisejícími aspekty teorie jazyků, automatů a logik. Na FIT VUT založil skupinu zabývající se automatizovanou analýzou a verifikací, jejíž členové pravidelně publikují na řadě špičkových mezinárodních konferencí a spolupracují s výzkumníky z řady zemí světa (např. Německo, Rakousko, Švédsko, Velká Británie, Tchaj-wan, USA či Francie).
Doc. RNDr. Jan Kofroň, Ph.D.
Docent Jan Kofroň je členem Katedry distribuovaných a spolehlivých systémů na Matematicko-fyzikální fakultě Univerzity Karlovy. Po absolvování doktorského studia strávil sedm měsíců v Německu ve Forschungzentrum Informatik Karlsruhe. Se svou skupinou se věnuje výzkumu a vývoji v oblasti metod pro symbolickou verifikaci software. Se členy skupiny pravidelně publikuje na mezinárodních konferencích a v impaktovaných časopisech a spolupracuje se zahraničními výzkumnými pracovišti.