- På hårdvarusidan har formell verifiering gjort att många buggar hittats snabbare. Vi vill göra samma sak med programvara för inbyggda system, säger Jeremy Goulding på verktygstillverkaren I-Logix.

Företaget har därför presenterat två nya verktyg, utvecklade i samarbete med tyska OSC. Det ena gör modellkontroll, det vill säga verifierar automatiskt och formellt att en beskrivning av en systemmodell klarar alla möjliga tillstånd.

- På några minuter kan en modell med upp till 300 tillstånd analyseras till hundra procent, för samtliga möjliga indata, hävdar Werner Damm på OSC.

Det andra verktyget är en automatisk testvektorgenerator som utifrån den analyserade modellen alstrar vektorer med indata och förväntade utdata. Dessa används för att testa hela systemet, när programvaran körs på hårdvaran.