TU Darmstadt / ULB / tuprints

Formale Anforderungsanalyse und Testunterstützung im Produktlinienkontext

Markert, Florian :
Formale Anforderungsanalyse und Testunterstützung im Produktlinienkontext.
Datentechnik, Darmstadt
[Ph.D. Thesis], (2012)

[img]
Preview
PDF
Dissertation_Markert_ULB.pdf
Available under Creative Commons Attribution Non-commercial No Derivatives.

Download (990Kb) | Preview
Item Type: Ph.D. Thesis
Title: Formale Anforderungsanalyse und Testunterstützung im Produktlinienkontext
Language: German
Abstract:

Eine aus Anforderungen bestehende Spezifikation stellt die Grundlage für Entwicklungsprojekte dar. Fehler, die in der Spezifikation enthalten sind, wirken sich auf den gesamten Entwicklungsprozess aus. Im schlimmsten Fall pflanzen sie sich durch den Entwicklungs- und Testprozess fort und werden erst beim Abnahmetest entdeckt. Die Vermeidung von Fehlern in Spezifikationen ist daher eine Grundvoraussetzung für eine zügige und kostengünstige Entwicklung. Handelt es sich um sicherheitskritische Systeme, dann können Fehler in der Spezifikation im Ernstfall Menschenleben gefährden oder großen finanziellen Schaden nach sich ziehen. Eine Überprüfung der Spezifikationen sollte daher nicht nur manuell, sondern auch formal sowie vollständig und so weit wie möglich automatisiert durchgeführt werden. Die immer stärkere Verbreitung von Produktlinien, die sich durch die Strukturierung von Variabilität und Gemeinsamkeiten verwandter Produkte mit dem Ziel der Wiederverwendung auszeichnen, steigert die Komplexität der Überprüfung der Spezifikationen im Entwicklungsprozess. Durch die Vielzahl von Produkten, die aus einer Produktlinie abgeleitet werden können, ist eine manuelle Überprüfung der Spezifikation kaum noch möglich. Handelt es sich um Spezifikationen eingebetteter Systeme, so wird die Überprüfung durch die Aufteilung in Soft- und Hardware weiter erschwert. Im Rahmen dieser Dissertation wird ein Verfahren vorgestellt, das Spezifikationen auf Widersprüche, Vollständigkeit und Redundanz überprüft. Dieses Verfahren ist sowohl für Spezifikationen einzelner Produkte also auch für solche, die Gemeinsamkeiten und Unterschiede von Produktlinien beschreiben, einsetzbar. Die Analyse der Spezifikationen basiert auf bekannten Algorithmen aus der formalen Verifikation von Hardwareschaltungen. Eine Anwendung dieser Algorithmen für Verhaltensbeschreibungen verschiedener Systeme sowie die Erweiterung durch Variabilität wird erläutert. Weiterhin wird auf die Generierung von „Orakeln“ eingegangen, die sich für die Voraussage von Testergebnissen eignen und ebenfalls auf Algorithmen aus der formalen Verifikation von Hardwareschaltungen basieren. Außerdem können auf einem „Orakel“ Annahmen über das Systemverhalten bewiesen werden. Zusätzlich wird ein Modell für die strukturierte Darstellung von Testfällen eingeführt. Die Testfälle können auf dem „Orakel“, einem weiteren Systemmodell oder auf dem System selbst ausgeführt werden. Die in dieser Dissertation vorgestellten Konzepte wurden an Beispielen aus dem universitären und dem industriellen Umfeld erprobt.

Alternative Abstract:
Alternative AbstractLanguage
A requirements specification forms the basis of all development projects. Faults incorporated in this initial specification put the entire project at risk. In the worst case, faults propagate through the development and test processes and are not recognized before acceptance testing. Therefore, the avoidance of faults in specifications is the basic prerequisite for efficient and competitive development. In case of safety critical systems faults may even jeopardize human life or result in a huge financial loss. Specification analysis should not rely exclusively on inspection or review meetings but should also be aided by automated formal methods. The use of product line engineering in the development of systems complicates the specification analysis even more. Product line engineering aims to reuse development and test fragments by structuring common and variable parts of a system. Due to the potentially huge number of products that can be derived from a product line, a manual analysis is barely possible. Further, the requirements analysis is even harder if the specification describes an embedded system due to the Software and Hardware layers. This thesis describes a method for analysing specifications with respect to contradictions, completeness, and redundancy. The method should be applicable both to specifications dealing with single products and to those dealing with product lines. Well understood algorithms from the field of the formal verification of hardware circuits are applied to the specification analysis. Further, these algorithms are extended using the variabilty information necessary to deal with product lines. Additionally, the thesis focuses on the generation of “oracles“ that can be utilized as predictors for test case results, building on algorithms taken from the field of the formal verification of hardware circuits. An “oracle“ may be used to prove assumptions that must be true according to the specification. Additionally, a model for structuring the test cases in the field of product line engineering is presented. These test cases may be executed by an “oracle“, another system model or by the system itself. All presented concepts are validated using examples related to academic work and to real world industrial problems.English
Place of Publication: Darmstadt
Uncontrolled Keywords: Anforderungsanalyse, Produktlinien, Testen, Qualitätssicherung, Formale Methoden, Vollständigkeit, Widerspruchsfreiheit
Classification DDC: 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
600 Technik, Medizin, angewandte Wissenschaften > 620 Ingenieurwissenschaften
Divisions: Fachbereich Elektrotechnik und Informationstechnik > Rechnersysteme
Date Deposited: 12 Jun 2012 13:51
Last Modified: 07 Dec 2012 12:05
URN: urn:nbn:de:tuda-tuprints-29995
License: Creative Commons: Attribution-Noncommercial-No Derivative Works 3.0
Referees: Eveking, Prof. Dr.- Hans and Schürr, Prof. Dr. Andy
Refereed: 6 June 2012
URI: http://tuprints.ulb.tu-darmstadt.de/id/eprint/2999
Export:

Actions (login required)

View Item View Item