Computergestützte Verifikation von Automatenkonstruktionen für Model Checking

点击翻译按钮获取中文摘要

Model Checking ist die in der Praxis wichtigste Methode zur Verifikation und Falsifikation von Hardware- und Softwaresystemen, d.h., zur Sicherstellung der Zuverlässigkeit dieser Systeme. Ziel des Projekts ist es, Implementierungen von Kernalgorithmen des Model Checking bereitzustellen, die mit Hilfe eines interaktiven Theorembeweisers als korrekt nachgewiesen wurden, um so die Zuverlässigkeit des Model Checking selbst signifikant zu erhöhen. Wir konzentrieren uns auf den sehr weit entwickelten automatentheoretischen Ansatz zum Model Checking. Daher sind sowohl die Verifikation wichtiger Algorithmen des Model Checking als auch die Formalisierung der Automatentheorie das Ziel — letzteres nicht nur als notwendige Basis, sondern als langfristige Investition in eine Theorie, die für die Informatik so grundlegend wie keine andere ist. Dieses Projekt ist Teil einer wachsenden weltweiten Bestrebung, die Trennung zwischen Theorie und implementierter Praxis der Informatik zu überwinden, indem Theorie und Programme simultan in einem Theorembeweiser formalisiert werden. Herausragende Ergebnisse waren bisher z.B. ein verifizierter C-Compiler und ein verifizierter Betriebssystemkern. Wir wollen erstmalig das Model Checking und die Automatentheorie in das Zentrum eines solchen Formalisierungsprojekts stellen.