Abstraktionstechniken zur Verifikation lokaler Eigenschaften großer paralleler Systeme

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

Zielsetzung dieses Projektes ist die Entwicklung von Abstraktionsverfahren, die die Verifikation (d.h. den formalen Nachweis der Korrektheit) lokaler Eigenschaften von parallelen Systemen erlauben. Basisidee des Abstraktionsverfahren ist die Annahme, dass die Verifikation lokaler Eigenschaften einzelner Komponenten nur Informationen über andere Komponenten in einem begrenzten Umfeld benötigt. Die Abstraktion kann die eigentlich zu verifizierende Komponente und das Restsystem in einem unterschiedlichen Grad repräsentieren und so den zu durchsuchenden Zustandsraum klein halten. Kernpunkt der Technik wird die Verwendung von mehrwertigen Logiken zur Darstellung partieller Strukturen sein, die Abstraktionen mit sehr präzisen Aussagen sowohl über universelle als auch existentielle Eigenschaften erlauben.