Dansk forsker vil udrydde softwarefejl

Software fylder mere og mere i vores liv. Vores infrastruktur, såsom metro og tog, fly og elnet, afhænger af den. IT-problemer kan lægge en arbejdsplads ned i timevis.

Computere og printere holder gerne op med at virke, lige før eksamensopgaven eller morgendagens præsentation til arbejdet skal printes ud. Telefonskærmen fryser, når man har mest brug for den.

Men på trods af hvor afhængige vi er blevet af software i vores samfund, findes der ikke nogen metode, der kan garantere, at der ikke er softwarefejl, som pludselig kan få den til at holde op med at virke. Det skal et nyt dansk forskningsprojekt nu prøve at lave om på.

»Vi vil gerne udvikle nogle metoder, så vi kan skrive software uden fejl,« siger Kasper Svendsen, der er postdoc på Institut for Datalogi på Aarhus Universitet.

Med støtte fra Det Frie Forskningsråd starter han i september et forskningsprojekt, hvor han over to år skal udvikle en matematisk metode, der kan give en garanti for, at et computerprogram fungerer korrekt. Det skal han blandt andet i samarbejde med University of Cambridge.

»Det lidt fjollede er, at computere er designet af mennesker, og vi ved præcis, hvad de gør. Men på trods af det, så indeholder de fleste programmer mange fejl - det har vi alle sammen oplevet. Vi har endnu ikke nogle effektive metoder til at garantere, at software ikke indeholder fejl,« siger Kasper Svendsen.

Matematik skal udrydde fejl

Fejl i computerkoder har altid været en udfordring. Siden slutningen af 1960'erne har forskere arbejdet med at opbygge matematiske metoder til at forhindre dem.

Kasper Svendsen skal bygge videre på en metode, der benytter såkaldt separationslogik, hvor man udleder sande udsagn fra sande udsagn. Og ultimativt udleder, at koden virker korrekt.

»Idéen er næsten så gammel, som computere er, men det har ofte vist sig at være for tidskrævende at foretage den slags beviser for software,« siger Kasper Svendsen.

Der er tidligere udviklet metoder, der kan verificere programkoder på op mod 10.000 linjer, men mange avancerede programmer har koder på millioner af linjer. Derfor er der behov for at videreudvikle metoderne.

Kasper Svendsen skal udvikle en metode, der matematisk kan bevise, at der ikke opstår fejl i software-kode, når koden skal kompileres, eller der skal foretages parallelle beregninger (se faktaboks).

I dag må man nøjes med at teste programmerne manuelt, og det er langt fra grundigt nok, siger Kasper Svendsen.

»Man kan ikke teste alle input, så man kan ikke garantere, at der ikke er fejl. Når kodebasen bliver større, bliver problemet med at teste software også meget større. Man kan simpelthen ikke blive ved med at være afhængig af testning som den eneste måde at kvalitetsteste. Det er ikke holdbart i det lange løb. Vi er nødt til at udvikle bedre metoder til at sikre, at vores software ikke indeholder fejl. Vi vil bruge matematik til at bevise, at programmerne fungerer korrekt,« siger han.

Oversættelse kan skabe fejl

Når der ofte sniger sig fejl ind i software, skyldes det, at programmører af software er fanget mellem to modsatrettede hensyn:

På den ene side skal koden virke korrekt. På den anden side skal den køre så hurtigt, at brugeren ikke bliver frustreret over langsomme beregninger.

For at øge hastigheden skærer man ofte nogle hjørner, som gør, at hastigheden på beregningerne kan mangedobles – men som samtidig øger risikoen for, at koden ikke fungerer som forventet.

Mens programmøren selv vælger (eller fravælger) nogle af hjørnerne, skæres andre automatisk fra. Kasper Svendsen skal særligt se på konsekvenserne af:

• De hjørner, der automatisk bliver skåret, når koden kompileres.
  
• De hjørner, der skæres, når processoren skal foretage parallelle beregninger.

Han skal derefter finde beviser for, hvornår koden alligevel fungerer korrekt i de to situationer.

Når koden kompileres – altså oversættes fra det kodesprog, programmøren forstår, til det maskinsprog af 1'er og 0'er, som computeren forstår – sker der nemlig automatisk en række optimeringer, der øger hastigheden. For eksempel kan der blive byttet rundt på rækkefølgen, to instruktioner skal gennemkøres i.

»Vi har ikke særlig god forståelse af, hvad konsekvenserne af de her automatiske kompileroptimeringer er. En stor del af forskningsprojektet bliver at forstå, hvad konsekvensen er af de ændringer,« siger Kasper Svendsen.

Skal undgå koks i parallelle beregninger

Kasper Svendsen påpeger, at ændrede instruktioner også kan påvirke parallelle beregninger i processoren, der afvikler programmerne på computere.

En processor har en række kerner, der hver kan foretage én beregning eller udføre én instruks ad gangen. Ved at dele sin kode op, så forskellige dele bliver beregnet sideløbende – altså parallelt – i forskellige kerner, kan man mangedoble hastigheden.

Opdelingen er afgørende for at sikre, at programmer kan køre hurtigt på vores computer eller smartphone. Men samspillet mellem parallelle beregninger kan samtidig være årsag til softwarefejl.

»Det er ret svært at skrive kode, som sikrer, at kommunikationen mellem parallelle beregninger er korrekt, uden at forsinke beregningen unødvendigt,« siger Kasper Svendsen.

For eksempel kunne man som programmør godt antage, at hvis man har to kerner til at foretage sine udregninger, og man beder kernerne om samtidig at læse en værdi fra en delt hukommelse, så læser de nok også samme værdi. Men det garanterer producenterne af processorerne ifølge Kasper Svendsen ikke.

»Så hvis korrektheden i ens program er afhængig af, at værdien er den samme, så er man nødt til at indsætte nogle ekstra instruktioner. Og det forsinker eksekveringen. For hastigheden gør det en ret stor forskel, om der er indsat lidt for mange instruktioner, så man vil helst indsætte så få instruktioner som muligt og stadig garantere, at ens program er korrekt. Det er det, som mit forskningsprojekt handler om at gøre matematisk,« siger Kasper Svendsen.

Mens forskningsresultatet bliver ren matematik, kan metoden i princippet efterfølgende puttes ind i en computer, der kan gennemgå softwarekode og give koden et kvalitetsstempel, der garanterer, at et computerprogram ikke indeholder fejl.

Softwareudviklere mangler ingeniørviden

På IT-Universitetet i København mener lektor Jesper Bengtson, der forsker i program-verifikation, at det er vigtigt at udvikle matematiske metoder, der kan supplere den omfattende testning af software, der finder sted i dag – for testning af software kan naturligvis kun bevise, at der er fejl i et program, ikke at der ikke er fejl, påpeger han.

»Software bliver brugt over alt. Det kan godt være, at man mest tænker på computeren på skrivebordet eller ens telefon, når man tænker på software, men størstedelen af alle computere er små og indbygget i ting som biler, fly og medicinalt udstyr. En moderne bil har mere end 100 små computere, der styrer airbagen, brændstoftilførslen og bremserne. Hvis man kan garantere, at de aldrig vil fejle, vil det være meget betydningsfuldt, og noget virksomheder uden tvivl vil være interesseret i,« siger Jesper Bengtson.

Jesper Bengtson påpeger, at forskningen i de matematiske metoder endnu er i en tidlig fase, hvor det er for tidligt at forvente, at virksomheder vil satse store summer på at udvikle matematiske softwaregarantier.

Men han forventer, at Kasper Svendsens forskningsprojekt vil bringe feltet videre.

»Software-udvikling er et relativt nyt felt, for vi har kun gjort det i omkring 70 år. Vi mangler de ingeniørstandarder, man ville følge, hvis man skulle bygge en bro. Så ville man lave en arbejdstegning og bruge en masse matematik for at sikre, at broen ikke kollapser under sin egen vægt, når det første tog kører over. Vi har ikke den slags teknikker inden for software – endnu,« siger Jesper Bengtson.

»Lige nu minder en software-udvikler mere om en tømrer end om en ingeniør. Med det mener jeg, at det er et håndværk og det kræver dygtighed, men vi mangler nogle af de ingeniørstandarder, der findes i andre fag. Det, Kasper Svendsen gør, er at forsøge at tilføre dette til software-udvikling,« siger Jesper Bengtson.