Verifikation probabilistischer Modelle in interaktiven Theorembeweisern

• Antragsteller: Professor Dr. Tobias Nipkow, Ph.D.
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2013 bis 2016
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 226793109

Viele Systeme in der Natur und in der Informatik sind probabilistisch. Inder Informatik wird der Zufall sogar häufig dazu verwendet, Systeme robusteroder effizienter zu machen. Model Checking ist ein Methode, Systeme mitendlichem Zustandsraum automatisch zu analysieren (zu `verifizieren'). In denletzten 15 Jahren ist Model Checking für probabilistische Systeme zu einemeigenen, sehr aktiven Forschungsgebiet geworden.Die zweite wichtige Verifikationstechnik in der Informatik ist dieinteraktive Verifikation mit einem Theorembeweiser. Hier wurden in denletzten 10 Jahren große Fortschritte gemacht, die es inzwischen erlauben,z.B. Compiler und Betriebssystemkerne zu verifizieren. Gleichzeitig wurdenerste Grundlagen der Wahrscheinlichkeitstheorie in Theorembeweisernformalisiert. Als eine Anwendung wurde kürzlich erstmalig einprobabilistische Model Checking Verfahren interaktiv verifiziert. Ziel desAntrags ist es nun, die mathematische Basis probabilistischer Systeme ineinem Theorembeweiser zu formalisieren, um damit auch komplexe Algorithmenund Systeme verifizieren zu können, die sich nicht mehr automatisch behandelnlassen. Als konkrete Anwendungen werden wir eine Reihe parametrischerprobabilistischer Algorithmen für dezentrale Rechnernetze interaktivverifizieren.Die Motivation für die formale (egal ob automatische oder interaktive)Verifikation ist die extrem hohe Zuverlässigkeit. Dies ist insbesondere beiprobabilistischen Systemen relevant, da traditionelle Beweise vielfehleranfälliger sind als bei deterministischen Systemen, z.B. wegensubtiler Abhängigkeiten zwischen Zufallsvariablen. Bei der interaktivenVerifikation sind die mathematischen Grundlagen vollständig imTheorembeweiser verfügbar, was die Zuverlässigkeit und vor allem dieFlexibilität enorm erhöht, weshalb man z.B. auch parametrische Systemebehandeln kann. Aus diesen Gründen hat die Formalisierung wichtigerGrundlagen der Informatik in Theorembeweisern sich zu einem globalenProjekt entwickelt, in dem bisher z.B. Programmiersprachen und Compilerbesonders intensiv behandelt wurden. Das Ziel dieses Antrags ist es,probabilistische Systemmodelle (und, als Fallstudien, die zugehörigen ModelChecking Verfahren) vollständig in einem Theorembeweiser zu formalisieren:Sowohl um Anwendungen wie die Verifikation parametrischer Systeme zuermöglichen, als auch um die Formalisierung der mathematischen undinformatischen Grundlagen um dies sehr wichtige Gebiet zu bereichern. Diesist eine Investition in die Zuverlässigkeit von Informatik-Systemen.

• DFG-Verfahren: Sachbeihilfen