In: Arbeitspapiere der GMD, No. 1029. November 1996. In German.
Abstract: Mit dem Begriffs- und Methodenapparat formaler Sprachen wird ein kompositionelles Verifikationsinstrumentarium für kooperierende Systeme entwickelt. Kooperierende Systeme sind solche verteilten Systeme, welche durch eine ``lose Kooplung'' und ``Entscheidungsfreiheiten'' ihrer Komponenten charakterisiert sind. Typische Beispiele hierfür sind Telephonsysteme, Chipkartensysteme, Kommunikationsprotokolle etc.
Das dynamische Verhalten eines solchen Systems wird durch die Menge aller möglichen ``Aktionsfolgen'', also durch eine formale Sprache dargestellt. Die Verifikationsmethode basiert auf einem Abstraktionsbegriff, welcher durch eine spezielle Klasse von Sprachhomomorphismen (schlichte Homomorphismen) formalisiert ist. Im Kontext kooperierender Systeme berücksichtigen diese Homomorphismen sowohl Sicherheits- als auch Lebendigkeitseigenschaften in adäquater Weise. Das Zusammenspiel der Komponenten eines kooperierenden Systems wird durch Kooperationsprodukte formaler Sprachen beschrieben. Diesem Konzept entsprechen auf automatentheoretischer Seite sogenannte asynchrone Produktautomaten. Zum Nachweis der Schlichtheit von Homomorphismen auf Kooperationsprodukten wird der Begriff der Kooperativität der Komponenten von Kooperationsprodukten eingeführt.
Mit der entwickelten Methode können in kompositioneller Weise homomorphe Bilder von Systemverhalten berechnet und die Schlichtheit der Homomorphismen überprüft werden. Dabei werden unnötige Nebenläufigkeiten vermieden, was bei wohlstrukturierten Systemspezifikationen zu erheblichen Komplexitätsreduktionen führt. Das Verfahren kann auch iterativ benutzt werden und ermöglicht bei parametrisierten Systemspezifikationen Induktionsbeweise.