Praktisk Verifiering av Tillståndsfull Säkerhetskritisk Inbäddad C kod med hjälp av Ändliga Automater och VCC

Mathias Lindgren
mathial@kth.se

Sammanfattning

Fordon under 2000-talet blir mer och mer beroende av inbäddade programvarusystem för navigering, systemkontroll, sensorer, och underhållning. Tillverkare av bilar har också under åren ställts under fler och fler regleringar gällande säkerhet och mer resurser har lagts på rigorösa tillförlitlighetstester.

Vissa biltillverkare har undersökt användandet av formell verifiering som en strategi för att säkerställa tillförlitlighet och säkerhet. Tidigare arbete har utvecklat tekniker och metoder för automatiserad formell verifiering för att hjälpa till i denna strävan. En kodegenskap i inbäddade system är tillståndsfullhet, hur programmets minne förändras över tid.

För att tackla problemet med att beskriva krav med en tillståndsfull karaktär, föreslås en ny modell för att beskriva säkerhetskrav som Ändliga Automater. En fallstudie som tittar på verkliga krav på tillståndsfull c-kod utfördes. Verifiering med olika verktyg var framgångsrik när kraven skrevs i denna nya stil. Framtida möjliga förbättringar och brister identifieras.