PAUL PETTERSSON Yrke: Professor i realtidssystem vid Mälar­dalens högskola. Familj: Fru och barn. Bor: Stockholm. Hobby: Rockgitarr, löpning, Omega­klockor. Född: Kvinneby, ­Hjulsbro, Linköping.

En av Paul Petterssons kontakter på Linkedin tror att han renoverar armbandsur.

– Det vet jag inte om man kan påstå, skrattar han.

– Jag kan ta mig in i klockan för att göra rent och ta bort damm. Jag kan öppna och ta ut urverket. Och skulle kunna byta en urtavla.

Han har en vurm för Omega-klockor från 60-talet. Han samlar på dem.

– Du kan få tag på en gammal Omega ganska enkelt. Jag gillar armbandsur. De återspeglar sin tid. Under första halvan av 1900-talet skulle alla skaffa ett armbandsur – det blev en allemanssak. På 70-talet blev klockorna fyrkantiga som tv-apparater.

Finns det någon koppling mellan ­datavetenskap och urverk?

– Jag tror snarare det handlar om ett primalbehov av att jaga och samla.

Han disputerade i datorteknik på Uppsala universitet 1999. År 2006 blev han professor vid MDH. Åtta doktorander har han tagit till examen sedan 2000.

En ren universitetskarriär?

– Nej, jag var faktiskt 1,5 år på BT Industries i Mjölby efter gymnasiet. Jag pendlade dit från Linköping.

På kvällarna repade han med olika band. Musikintresset tog han upp igen för några år sedan.

Idag spelar han gitarr och sjunger i coverbandet The Revolving Gates. Namnet kommer från snurrdörrar på Ericsson som de var tvungna att kånka sin utrustning ­genom på sin första spelning.

– De andra tre medlemmarna ­jobbar på Ericsson. Vi spelar 70-talsrock – John Fogerty, Stones – sådant som fungerar på fester.

Han blev prorektor hösten 2012. Just nu leder han en forskningsutvärdering för Mälardalens högskola.

– Och så är jag bland annat involverad i våra verksamheter kring internationalisering och samverkan.

Som prorektor är han del av högskolans ledning och sitter dessutom som högskolans representant i ett antal styrelser och styr­grupper.

En prorektor är rektorns ställföreträdare.

– Trots att han också är en framgångsrik forskare tar han uppdraget som prorektor på stort allvar, säger rektor Karin Röding.

– Han bidrar med sin kompetens och med sin analytiska förmåga – men inte minst med glimten i ögat och det goda humöret – det är lätt att skratta med Paul.

Jobbet som forskare och lärare har fått maka på sig lite sedan han blev prorektor.

– Jag har fått bortprioritera ­vissa delar. Jag är huvudhandledare i mind­re utsträckning. Och några forskningsprojekt har fått flytta till andra personer.

Att döma av hans twitterflöde sitter han mest i möten. Men det är möjligen inte representativt.

– Jag är inte så aktiv på Twitter. På möten? Det är kanske ett sätt att informera om vad jag gör, skrattar han.

Något annat i twitterflödet är löpning.

– Nästa Stockholm Maraton blir min femte maraton.

Han är professor i realtidssystem – inbyggda datorsystem som har tider att passa.

– Modellerna vi jobbar med har tid som parameter – de måste vara korrekta tidsmässigt.

Närmare bestämt forskar han i modellering av dessa system, och analys av modellerna. Det är något som klassiska data­vetare inte är så bra på.

– Till skillnad från andra ingenjörsvetenskaper.

– Att analysera och använda matematiska modeller är egentligen inget konstigt. På BT var det en självklarhet att göra ritningar av det som skulle konstrueras och räkna på om det skulle hålla. Det är en parallell till vad vi gör i vår forskning – vi beskriver systemet och analyserar om det kommer att bete sig enligt hur det är tänkt.

– Det handlar oftast om programvara som styr någonting. Ju viktigare det är, det som styrs, desto mer kritiskt är det. Ett fel kanske kostar mycket pengar eller kan skada människor. Då bör man lägga ner energi på att se till att programmen blir korrekta.

Ett viktigt utvecklingsverktyg i Paul Pettersson analys heter Uppaal, efter Uppsala och Aalborg där utvecklingen startade.

Kim G. Larsen – professor i Aalborg – träffade Paul Pettersson för första gången när Paul fortfarande var doktorand.

– Tillsammans med Wang Yi skapade vi de första versionerna av det numera prisbelönta verktyget, berättar Kim G. Larsen.

Uppaal har beskrivits som världens ledande verktyg för verifiering av realtidssystem. I fjol fick de tre ett pris för verktyget av CAV – den ledande konferensen om datorstödd ­verifiering.

Samarbetet kring Uppaal fortsatte i Aalborg under Paul Petterssons post-doc där.

– Han var alltid engagerad i utvecklingen av verktyget och av att det skulle plockas upp och börja användas av verksamma ingenjörer, säger Kim G. Larsen.

– Det var ett mycket trevligt år vi hade tillsammans och jag är mycket glad över att kunna räkna honom som en vän.

I Uppaal kan man konstruera och simulera modeller i form av så kallade tidsautomater – tillståndsmaskiner med tidsvillkor på övergångarna – och beräkna deras egenskaper.

Uppaal har inte lett till någon ­avknoppning?

– Det finns ett företag, men vi som grundat det har fullt upp med annat.

– Den kommersiella möjligheten kanske också faller lite grand på att verktyget finns att ladda hem gratis?

Det har legat fritt tillgängligt på webben i snart 20 år.

– Det används i kurser på en lång rad universitet.

Därmed inte sagt att det inte kommer industrin till nytta. Nasa är användare, liksom Toyota och många andra.

Modellering används trots allt i industrin idag. Paul Pettersson har samarbetat i projekt med bland annat Volvo och Bombardier. Den senare modellerar i något som kallas Func­tion Block Diagram.

– Ofta gör de modeller för att ­kunna genera kod.

– Med våra metoder kan man analysera deras diagram. Vi kan till exempel automatiskt generera testfall.

Detta sparar inte bara in det manuella arbetet utan ger garanterat maximal täckning. En annan möjlighet är att generera testsviter som är optimerade på olika sätt, exempelvis att de utgör en minimal uppsättning.

– Metoderna kan också användas för att analysera och hitta fel. I det enklaste fallet  ett tillstånd i modellen som man inte borde kunna komma till, kanske ett feltillstånd.

Ännu är inte analysen integrerad i Bombardiers verksamhet. Att ta fram verktyg för detta är nästa steg i projektet.

Varför används inte formell analys i ännu större utsträckning?

– I programmering är det ofta väldigt kort steg från tanke till realisering – man programmerar sina idéer direkt och investerar inte i att göra modeller först.

Området hade dessutom en backlash på 90-talet.

– Det fanns nog en övertro på formella metoder – man trodde de skulle lösa mer än vad som var möjligt, som det ofta blir. När det visade sig att det inte var så spred sig besvikelsen.

– Men metoderna överlevde och letade sig in i andra sammanhang, utan att man kanske kallar dem formella. Mycket av den statiska analys som kompilatorer använder är sådant som man skulle kallat formella metoder på 90-talet.

– Fast nidbilden finns kvar av formell modellering – en matematiker som sitter och räknar på formler vid skrivbordet.