---

Implementierter Verifikationsprozess

Im Rahmen der Dissertation von Andreas Both wurde eine Verifikationsprocess entwickelt. Dieser erlaubt die Überprüfung von nicht-funktionalen Eigenschaften in Form von Protokollen. Im Gegensatz zu anderen Arbeiten (z.B. behavioral protocols) ist dieser Ansatz grundsätzlich darauf ausgerichtet (konservative) Abstraktionen aus (industriellem) Quellcode zu erstellen. Somit ist sichergestellt, dass jede Aussage direkt auf den Quellcode bezogen werden kann und nicht wie sonst üblich nur die Spezifikation erfasst.

Zu diesem Zweck wurde eine Architektur entworfen die den Ansprüchen der Benutzer (Industriepartner) genügt. Ein wichtiges Kritierium dabei war, dass Quellcode nie außerhalb des Netzbereichs des Partners zugreifbar ist. Gleichzeitig sollten aber Kapazitäten flexibel eingebracht werden können. Aus diesem Grund wurde ein Komponenten-orientierte Architektur entworfen, die auch Charakterzüge einer Service-orientierten Architektur enthält.

Implementierte Architektur (SOA)

Der implementierte Prozess orientiert sich an den fünf Schritten in die der Verifikationsprozess zerlegt ist [BZ08c]. Im Einzelnen besitzen die implementierten Webservices die folgende Funktionalität:

• WSA: Erzeugen von Abstraktionen aus Quellcode. Nachfolgend wird die Komposition der Bausteine ausgewertet. Neben einer Python-Implementierung stehen alsbald auch PHP- und BPEL-WSA zur Verfügung.
• WSO: Dieser Web Service stellt Optimierungen von PRS zur Verfügung. Außerdem ist er dafür verantwortlich auf Anfrage Combined Abstractions zu erstellen (Schnitt von PRS und Finite State Machines (endliche Automaten)). Darüber hinaus besitzt der WSO einen einfachen Verzeichnisdienst und erlaubt so den transparenten Zugriff auf verschiedene WSA-Services.
• WSB: Hier ist ein Modellprüfer für PAN verborgen. Dieser wird genutzt um Gegenbeispiele bestimmen zu können [SP09].
• WSC: dieser Webservice schirmt die Benutzerinfrastruktur von den anderen Bereichen ab. Er startet und verwaltet Verifikationsaufträge (asynchron). Die angeschlossene grafische Benutzerschnittstelle (Mehrbenutzerbetrieb) erlaubt einen komfortablen Zugriff auf die Abstraktionen und die Erstellung von Verifikationsaufträgen. Die zur Verfügung gestellte API ermöglicht einen Zugriff über eine Python-Schnittstelle (für wiederkehrende/nächtliche Aufträge). [FB09,P2]

Screenshot des P2-Frontends

Zum Seitenanfang