Software Components and Formal Methods from a Computational Viewpoint


Lambertz, Christian


[img]
Preview
PDF
lambertz.pdf - Published

Download (2MB)

URL: https://ub-madoc.bib.uni-mannheim.de/32889
URN: urn:nbn:de:bsz:180-madoc-328894
Document Type: Doctoral dissertation
Year of publication: 2012
Place of publication: Mannheim
Publishing house: Universität Mannheim
University: Universität Mannheim
Evaluator: Majster-Cederbaum, Mila
Date of oral examination: 31 January 2013
Publication language: English
Institution: School of Business Informatics and Mathematics > Praktische Informatik II (Majster-Cederbaum Em)
Subject: 004 Computer science, internet
Classification: CCS: D.2.1 D.2.4 F.1.1 F.1.2 F.3.1,
Subject headings (SWD): Formale Methode , Komponente <Software> , Transitionssystem , Nebenläufigkeit , Softwarearchitektur , Reduktion , Verklemmung , Verifikation
Individual keywords (German): formale Methoden , komponentenbasierte Systeme , Interaktionssysteme , Nebenläufigkeit , Softwarearchitektur , Architektureinschränkungen , kompositionelle Reduktion , Verklemmungsfreiheit , Verifikation
Keywords (English): 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.
Translation of the title: Softwarekomponenten und formale Methoden unter algorithmischen Gesichtspunkten (German)
Translation of the abstract: 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. (German)

Das Dokument wird vom Publikationsserver der Universitätsbibliothek Mannheim bereitgestellt.




+ Citation Example and Export

Lambertz, Christian (2012) Software Components and Formal Methods from a Computational Viewpoint. Open Access Mannheim [Doctoral dissertation]
[img]
Preview


+ Search Authors in

+ Download Statistics

Downloads per month over past year

View more statistics



You have found an error? Please let us know about your desired correction here: E-Mail


Actions (login required)

Show item Show item