Abstrakt
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ů.