Ny teknik för kontroll av system

Datorprogram används i dag för att kontrollera system inom många områden, till exempel i styrsystem för tåg och flygplan. I sin avhandling presenterar Marcus Nilsson en ny automatisk teknik för att verifiera sådana datorprogram. Avhandlingen läggs fram vid Uppsala universitet den 2 mars. Marcus Nilsson Regular Model Checking ISBN: 91-554-6137-9 Abstract Datorprogram som används för att kontrollera system i sjukvården eller i styrsystemen för tåg och flygplan måste fungera som de ska. Ett fel kan snabbt leda till katastrof. För att hitta fel i system har forskare utvecklat metoder för verifiering av program genom att konstruera matematiska modeller som kan analyseras. På senare tid har också automatiska metoder utarbetats, där datorprogram används för att analysera andra datorprogram. När ett program kan ha ett oändligt antal tillstånd, till exempel program som innehåller heltalsvariabler, är det dock problematiskt att hitta lämpliga analystekniker. Forskare har föreslagit ett flertal olika tekniker, som är bra för olika typer av system. Det finns tekniker för att analysera program med heltalsvariabler och andra tekniker för att analysera program med listor. Marcus Nilsson presenterar en teknik där program kodas in som en sekvens av symboler, ett så kallat ord. Man antar alltså att programmets tillstånd kan representeras som ord, och därmed kan en och samma teknik användas för att analysera olika typer av program. Detta gör att man spar tid vid utveckling av verktyg för att verifiera program. Genom att orden tillåts vara godtyckligt långa kan man representera både heltal av godtycklig storlek och listor av godtycklig längd. - Idén har funnits tidigare, men vi har utvecklat en teknik som fungerar praktiskt, berättar Marcus Nilsson. Resultaten väntas i förlängningen leda till att fel i system upptäcks tidigare och till att utvecklingskostnaderna därmed sänks. Kontaktpersoner: Marcus Nilsson, tel: 018-471 57 15, mobil: 073-574 21 90, e-post: marcus.nilsson@it.uu.se Linda Nohrstedt