Model checking softwéru je poslední dobou velmi aktivní téma výzkumu. Řada model checkerů byla vyvinuta pro různé programovací jazyky, např. SLAM, BLAST a Java PathFinder.
Použitelnost těchto nástrojů v praxi je však ještě třeba prokázat. V tomto příspěvku předkládáme výsledky experimentu, ve kterém jsme aplikovali BLAST (state-of-the-art model checker programů v jazyce C) v průmyslovém prostředí.
C implementace protokolu OPC UA byla verifikována proti množině formalizovaných vlastností. Odhalili jsme řadu dosud neznámých chyb v kódu.
Zároveň jsme však též narazili na hranice nástroje samotného. Tento experiment je cennou pomůckou pro v ývojáře nástrojů na analýzu kódu ale také pro vývojáře softwéru, kteří se potřebují rozhodnout zda je tento druh technik připraven k použití a vhodný pro dosažení jejich konkrétních cílů.