Automatiserad validering av funktionen hos ett datalager
en praktisk tillämpning av model checking
Företag förlitar sig ofta på datalager som aggregerar information från flera källor och över tiden. Dessa datalager är ofta centrala för beslutsfattande inom företagen, både kortsiktiga operativa beslut och långsiktiga strategiska. Eftersom information är en färskvara blir det allt viktigare att de dagliga laddningsrutinerna för datalagren fungerar. Denna rapport avser att analysera möjligheten att applicera principen model checking för en validering. Praktiskt avses att på ett automatiserat sätt använda Promela och Spin som verktyg för att validera att laddningsrutinerna för datalagret är korrekta.