05.12.2005
M.A. Valero Espada
aula
Faculteit der Exacte Wetenschappen
15:45
Modal Abstraction and Replication of Processes with Data
Promotor: prof.dr. W.J. Fokkink
Betere softwarekwaliteit met formele verificatietechnieken
De kwaliteit van softwarecomponenten kan verbeterd worden met formele verificatietechnieken. Dit is met name belangrijk voor software in kritische systemen, zoals luchtverkeerssystemen. Een kleine fout kan hier dramatische gevolgen hebben: er kunnen mensenlevens of enorme geldbedragen verloren gaan. Het doel van formele verificatie is aan te tonen dat zulke systemen zich altijd volgens verwachting zullen gedragen, zodat er geen onverwachte ongelukken gebeuren met onherstelbare schade als gevolg. Met verificatietechnieken kunnen fouten in de software al tijdens de ontwikkeling opgespoord worden. Hier is een grote wiskundige basis voor nodig. Het proefschrift van Miguel Valero bevat resultaten op het gebied van algebra en logica, die kunnen helpen om complexe kritische systemen te analyseren.
Valero ontwikkelde een methode om uit complexe en grootschalige systemen automatisch een klein kernsysteem te berekenen. Dit proces heet abstractie. Bovendien toonde Valero aan dat fouten in het kunstmatige, kleine systeem kunnen worden herleid tot vergelijkbare fouten in het echte systeem, en vice versa. Op deze wijze kunnen onderzoekers veel grootschaliger systemen controleren dan voorheen. Het proefschrift concentreert zich op abstractie van dynamische processen die gebruikt worden om de software van kritische systemen te beschrijven. Het onderzoek is uitgevoerd op het Centrum voor Wiskunde en Informatica (CWI) in Amsterdam, met financiële steun van NWO.
Voor meer informatie over activiteiten aan de VU:
dienst Communicatie, afdeling wetenschapsvoorlichting:
T 020 59 85666
E
Voor meer informatie over VUmc:
T 020 44 43444
E
Vrije Universiteit Amsterdam