An die Entwicklung heutiger informationstechnischer Systeme werden aufgrund ihrer hohen Komplexität, strenger Rahmenbedingungen und vielfältiger geforderter Qualitätsmerkmale hohe Anforderungen gestellt. Insbesondere für Systeme oder Systemteile, deren Mängel zu erheblichen Schäden führen könnten, ist die Entwicklung mit Hilfe formaler Methoden ein Ansatz, diesen Anforderungen zu begegnen. Formale Methoden ermöglichen eine hohe Präzision in Spezifikationen und die akkurate Verifikation kritischer Systemeigenschaften. Die Verwendung formaler Methoden zielt üblicherweise ab auf den Nachweis der Abwesenheit von Fehlern in Systemen. Da ein formales Modell im allgemeinen aber eine Abstraktion des realen Systems darstellt, die daher potentielle, beispielsweise implementierungsbedingte Fehler nicht repräsentieren kann, beinhaltet Fehlerfreiheit im formalen Modell eine idealisierende Annahme. Diese Idealisierung ist für frühe Entwicklungsphasen zulässig, in denen die eigentliche, intendierte Kernfunktionalität des Systems im Vordergrund der Untersuchungen steht. Im Rahmen einer weiteren Systementwicklung sollte es aber möglich sein, Fehler als unerwünschten, aber dennoch unvermeidbaren Teil eines Systems explizit aufzunehmen und zu behandeln. In dieser Arbeit wird hierfür eine formale Unterstützung präsentiert. Die formale Methodik FOCUS wird dazu um Begriffe und Notationen erweitert, mit denen verschiedenste Klassen von Fehlern eines verteilten, reaktiven Systems sowohl in abstrakter, eigenschaftsorientierter Black-Box Sicht als auch im Kontext von Transitionssystemen als sogenannte Modifikationen explizit dargestellt werden können. Auf der Grundlage einer formalen Darstellung wird es möglich, präzise und nachweisbare Aussagen über Fehlertoleranz eines Systems und die Auswirkungen von Fehlern zu machen. Zur Unterstützung einer Systementwicklung wird die schrittweise, auch nachträgliche Einführung von Techniken zur Fehlererkennung, zur Generierung von Fehlermeldungen und zur Fehlerkorrektur in ein bestehendes System auf systematische Weise ermöglicht. Die Praktikabilität dieser Techniken wird durch begleitende Beispiele illustriert. Damit wird ein weiterer Schritt hin zu einer durchgängigen und praktischen Verwendbarkeit formaler Methoden geleistet.     «

An die Entwicklung heutiger informationstechnischer Systeme werden aufgrund ihrer hohen Komplexität, strenger Rahmenbedingungen und vielfältiger geforderter Qualitätsmerkmale hohe Anforderungen gestellt. Insbesondere für Systeme oder Systemteile, deren Mängel zu erheblichen Schäden führen könnten, ist die Entwicklung mit Hilfe formaler Methoden ein Ansatz, diesen Anforderungen zu begegnen. Formale Methoden ermöglichen eine hohe Präzision in Spezifikationen und die akkurate Verifikation kritische...     »

The development of today's systems for information technology has to meet several requirements with respect to the system's inherent complexity, strict development constraints and a diversity of additional quality attributes. The application of formal methods during their development is an approach to meeting these challenges, especially for systems or system parts whose failure could induce substantial damage. Formal methods enable high precision in specifications and the accurate verification of critical system properties. The application of formal methods usually aims at providing evidence for the absence of faults in systems. In general, however, a formal model represents an abstraction of a system, which, inherently, cannot include faults of an implementation; therefore, assuming the absence of faults is an idealization. This idealization is permissible during early development phases when the intended core functionality of a system is focused. However, during subsequent steps of system development it should be possible to explicitly address and treat faults as an undesirable yet unavoidable part of a system. This thesis provides formal support for this purpose. The formal methodology FOCUS is extended by notions and notations enabling the explicit representation of various classes of faults of a distributed, reactive system. These extensions address the representation of faults as so-called modifications in both an abstract, property-oriented black-box view, and within the context of transition systems. On the basis of a formal representation of faults it becomes possible to make precise and verifiable statements about fault-tolerance of a system and the effects of faults. The development process for systems is enriched by systematically enabling a stepwise, even supplementary introduction of techniques for fault detection, for generation of error messages, and for error correction. The practicality of these techniques is illustrated by means of accompanying examples. This accomplishes a further step forward towards the seamless and practical applicability of formal methods.     «

The development of today's systems for information technology has to meet several requirements with respect to the system's inherent complexity, strict development constraints and a diversity of additional quality attributes. The application of formal methods during their development is an approach to meeting these challenges, especially for systems or system parts whose failure could induce substantial damage. Formal methods enable high precision in specifications and the accurate verification...     »