Formele verificatie van embedded software voor SIL-4 systemen

Bij Codewit Solutions specialiseren we ons in de formele verificatie van embedded software voor veiligheidskritische systemen, zoals spoorwegseinen en brugbedieningen. Onze aanpak garandeert dat besturingsalgoritmes foutloos functioneren onder alle denkbare omstandigheden, tot op het hoogste Safety Integrity Level (SIL-4).

De kern van onze methode ligt in statische code-analyse en wiskundige bewijsvoering. In plaats van te vertrouwen op traditionele testmethoden, modelleren we het systeemgedrag en bewijzen we de correctheid ervan met behulp van formele logica. Dit proces elimineert de onzekerheid die inherent is aan op steekproeven gebaseerd testen.

// Voorbeeld van een geverifieerde toestandsmachine
typedef enum {
    STATE_IDLE,
    STATE_ACTIVE,
    STATE_FAULT
} SystemState;

bool verifyTransition(SystemState current, SystemState next) {
    // Formele specificatie van toegestane overgangen
    return (current == STATE_IDLE && next == STATE_ACTIVE) ||
           (current == STATE_ACTIVE && next == STATE_IDLE) ||
           (current == STATE_ACTIVE && next == STATE_FAULT) ||
           (current == STATE_FAULT && next == STATE_IDLE);
}

Onze verificatiepijplijn omvat:

• Modelchecking: Exhaustieve verificatie van alle mogelijke systeemtoestanden.
• Theorem Proving: Wiskundig bewijs van algoritmische correctheid.
• Abstract Interpretation: Analyse van runtime-eigenschappen zonder uitvoering.

Het resultaat is software die voldoet aan de strengste normen, zoals EN 50128 voor spoorwegen en IEC 61508 voor industriële systemen. Door fouten in de ontwerpfase te elimineren, voorkomen we kostbare recalls en, belangrijker nog, potentieel gevaarlijke situaties.