Software components and formal methods from a computational viewpoint

Lambertz, Christian

Vorschau

PDF
lambertz.pdf - Veröffentlichte Version
Download (2MB)

URL:	https://madoc.bib.uni-mannheim.de/32889
URN:	urn:nbn:de:bsz:180-madoc-328894
Dokumenttyp:	Dissertation
Erscheinungsjahr:	2012
Ort der Veröffentlichung:	Mannheim
Hochschule:	Universität Mannheim
Gutachter:	Majster-Cederbaum, Mila
Datum der mündl. Prüfung:	31 Januar 2013
Sprache der Veröffentlichung:	Englisch
Einrichtung:	Fakultät für Wirtschaftsinformatik und Wirtschaftsmathematik > Praktische Informatik II (Majster-Cederbaum -2005, Em)
Fachgebiet:	004 Informatik
Fachklassifikation:	CCS: D.2.1 D.2.4 F.1.1 F.1.2 F.3.1,
Normierte Schlagwörter (SWD):	Formale Methode , Komponente <Software> , Transitionssystem , Nebenläufigkeit , Softwarearchitektur , Reduktion , Verklemmung , Verifikation
Freie Schlagwörter (Deutsch):	formale Methoden , komponentenbasierte Systeme , Interaktionssysteme , Nebenläufigkeit , Softwarearchitektur , Architektureinschränkungen , kompositionelle Reduktion , Verklemmungsfreiheit , Verifikation
Freie Schlagwörter (Englisch):	formal methods , component-based systems , interaction systems , concurrency , software architecture , architectural constraints , compositional reduction , deadlock-freedom , verification
Abstract:	Software components and the methodology of component-based development offer a promising approach to master the design complexity of huge software products because they separate the concerns of software architecture from individual component behavior and allow for reusability of components. In combination with formal methods, the specification of a formal component model of the later software product or system allows for establishing and verifying important system properties in an automatic and convenient way, which positively contributes to the overall correctness of the system. Here, we study such a combined approach. As similar approaches, we also face the so-called state space explosion problem which makes property verification computationally hard. In order to cope with this problem, we derive techniques that are guaranteed to work in polynomial time in the size of the specification of the system under analysis, i.e., we put an emphasis on the computational viewpoint of verification. As a consequence, we consider interesting subclasses of component-based systems that are amenable to such analysis. We are particularly interested in ideas that exploit the compositionality of the component model and refrain from understanding a system as a monolithic block. The assumptions that accompany the set of systems that are verifiable with our techniques can be interpreted as general design rules that forbid to build systems at will in order to gain efficient verification techniques. The compositional nature of software components thereby offers development strategies that lead to systems that are correct by construction. Moreover, this nature also facilitates compositional reduction techniques that allow to reduce a given model to the core that is relevant for verification. We consider properties specified in Computation Tree Logic and put an emphasis on the property of deadlock-freedom. We use the framework of interaction systems as the formal component model, but our results carry over to other formal models for component-based development. We include several examples and evaluate some ideas with respect to experiments with a prototype implementation.
Übersetzter Titel:	Softwarekomponenten und formale Methoden unter algorithmischen Gesichtspunkten (Deutsch)
Übersetzung des Abstracts:	Komponentenbasierte Softwareentwicklung ist ein vielversprechender Ansatz um die Entwurfskomplexität großer Softwareprodukte zu beherrschen, da die Anforderungen der Softwarearchitektur und des individuellen Komponentenverhaltens voneinander getrennt werden und die Wiederverwendbarkeit der Komponenten ermöglicht wird. In Kombination mit formalen Methoden wird durch die Spezifikation eines formalen Komponentenmodells des Softwareprodukts oder Systems die Prüfung und Verifikation von wichtigen Systemeigenschaften auf automatische Weise durchführbar, was positiv zur Korrektheit des Systems beiträgt. In dieser Arbeit untersuchen wir einen solchen kombinierten Ansatz. Wie vergleichbare Ansätze begegnen auch wir dem Problem der Zustandsraumexplosion, das die Verifikation von Eigenschaften algorithmisch schwer macht. Um dieses Problem zu bewältigen, betrachten wir Techniken, die eine Eigenschaftsprüfung in Polynomialzeit bezüglich der Spezifikation des zu analysierenden Systems garantieren, d. h. wir legen Wert auf die algorithmischen Gesichtspunkte der Verifikation. Als Konsequenz untersuchen wir Teilklassen von komponentenbasierten Systemen, die für eine solche Analyse zugänglich sind. Wir sind insbesondere an Techniken interessiert, welche die Kompositionalität des Komponentenmodells ausnutzen, und betrachten ein System nicht als monolithische Einheit. Die Annahmen, die durch die Menge der mit unseren Ansätzen verifizierbaren Systeme aufgestellt werden, können hierbei als allgemeine Entwurfsregeln verstanden werden, die es verbieten Systeme nach Belieben zu konstruieren um dafür effiziente Verifikationstechniken zu erhalten. Die kompositionelle Natur der Komponenten ermöglicht dabei Entwicklungsstrategien, die zu konstruktionsbedingt korrekten Systemen führen. Des Weiteren werden kompositionelle Reduktionstechniken begünstigt, die ein gegebenes Modell auf den für Verifikation relevanten Teil verkleinern. Wir betrachten in der Logik CTL spezifizierte Eigenschaften und legen einen Schwerpunkt auf Verklemmungsfreiheit. Wir benutzen Interaktionssysteme als formales Komponentenmodell, allerdings sind unsere Ergebnisse auch auf andere formale Modelle der komponentenbasierten Entwicklung übertragbar. Wir geben mehrere Beispiele an und evaluieren einige Ideen mittels einer Prototyp-Implementierung. (Deutsch)