Modellprüfung für Komponentensysteme

Softwaremodellprüfung ist ein Ansatz um bestimmte Eigenschaften (wie z.B. Schutz vor Angriffen, Sicherheit) von Software zuzusichern. Existierende Ansätze betrachten die zu prüfende Software als Ganzes. Ziel dieser Arbeit ist es, die Tauglichkeit dieser Ansätze für Komponentensysteme zu überprüfen und ggf. zu erweitern.

In dieser Arbeit werden Komponentenprotokolle betrachtet. Solche Protokolle definieren Mengen von zulässigen Reihenfolgen von Aufrufen der Funktionen der Komponentenschnittstelle. Diese Protokolle stellen einen Vertrag dar, der von Komponentenentwicklern  in der Komponentenschnittstelle zur Verfügung gestellt werden muss. Das Verhalten von Komponenten wird automatisch aus dem Quellcode erstellt und als sogenanntes Prozessersetzungssystem dargestellt. Es berücksichtigt sowohl unbeschränkte Parallelität als auch unbeschränkte  rekursive  Aufrufe. Mit Hilfe dieser Beschreibungen, die ebenfalls mit einer Komponente veröffentlicht werden, ist es gelungen automatisch die Einhaltung von Protokollen in Komponentensystemen zu prüfen, wobei wie in der Modellprüfung üblich, falsche Negativaussagen möglich sind. Derzeit beherrschen wir die Implementierungssprachen Python und PHP sowie die Geschäftsprozesssprache BPEL.  Die Programmiersprachen  C++ , Java und .NET sind aktuell in Bearbeitung.

Im Projekt wurden alle Arten von Komponentensystemen betrachtet, bei denen die Schnittstelle über eine Menge synchroner und asynchroner Prozeduren realisiert ist. So werden beispielsweise auch Webservices betrachtet. Ereignisbasierte Komponentenschnittstellen wurden nicht betrachtet.