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. / Companies of today put more and more trust into data warehouses that aggregates information from several sources and over time. These data warehouses are pivotal for decision making both for daily operational decisions and for long term strategic ones. Since information is a perishable it has become more and more important that the loading routines for the data warehouses works. This essay will look into the possibility to automatically transform the load procedures to use Promela and Spin as tools to validate that the data warehouse load.