Games and Scenarios for Real-Time System Validation

Denne afhandling omhandler forskning i validering af realtidsbaserede indlejrede software-systemer i forbindelse med modelbaseret udvikling. Afhandlingen præsenterer scenariebaserede og spilteoretiske tilgange til systemanalyse, verificering, syntese samt testning for derved at kunne håndtere de udfordringer, der opstår ved systemkarakteristika for ukontrollerbare miljøer, komplekse procesinteraktioner, kvantitative tidsrestriktioner, partiel observerbarhed og kombinationer heraf.

En udvidelse af live sequence charts (LSC) med tid præsenteres, således at indbyrdes procesadfærd og scenariebaserede krav til samtidige og kommunikerende realtidssystemer kan modelleres og specificeres i LSC. Ved at oversætte LSC til tidsautomater (TA), reduceres verifikation af konsistens af scenariebaserede modeller samt verifikation af egenskaber for disse til verifikation af CTL-egenskaber for realtidssystemer. Ligeledes reduceres syntese af eksekverbare systemer fra scenariebaserede modeller til at løse tidsafhængige spil. Ved at anvende vores prototypeoversætter i samspil med modelverifikationsværktøjet Uppaal og værktøjet Uppaal-Tiga, som anvendes til at finde løsninger til spil, påvises det, at disse metoder kan bidrage til at sikre korrekt interaktion for tidlige systemdesign, samt at disse opfylder eventuelle tidskrav.

Afhandlingen viser endvidere, at systematisk gennemprøvning (testning) af reaktive realtidssystemer kan ses som et tidsafhængigt spil mellem testudføreren og systemet som afprøves. Derfor præsenteres metoder, hvori vindende strategier anvendes som test-cases for black-box conformance testing. Disse metoder generaliseres til at imødekomme problemstillinger, der kun giver anledning til muligt vindende strategier. I disse tilfælde er den fortsatte afprøvning baseret på kooperative vindende strategier, der kræver samarbejde fra systemet tidligt i spillet. Endvidere tilpasses metoderne til tilfælde, hvor kun partiel observerbarhed haves, dvs. hvor kun ufuldstændige oplysninger fås fra systemet. Alle disse metoder bidrager til i højere grad at kunne teste for korrekt reaktion ved stimuli og rettidige reaktioner fra de pågældende systemer. Eksperimentelle evalueringer gennem case-studies indikerer, at de foreslåede metoder er realistiske -- både konceptuelt, algoritmisk og med hensyn til beregnelighed.