Eine Methode zur Konstruktion zuverlässiger Software-Systeme für den Einsatz im Produktionsbereich

Files
13833_000_Friedl_web2.pdf (84.23 MB)
Diss. Reihe Fertigungstechnik, Band 0

Language
de
Document Type
Doctoral Thesis
Issue Date
2020-06-03
Issue Year
1984
Authors
Friedl, Anton
Editor
Abstract

Due to the increasing spread of electronic data processing, the ongoing drop in hardware prices and the solution of increasingly complex problems with program systems, the software has become more and more important in the last decade. During this period, the ratio of software to hardware costs for DV installations shifted continuously in favor of the software, and the proportion of software in complex applications today is of the order of 90%. Surprisingly, up until a few years ago, this growing importance of software was countered by a procedure in the creation of software that could neither be described as methodical nor as rational. The consequence of this was the much-cited software crisis with poor quality programs and often terrifyingly high costs for their creation. The real costs for the software were often up to 100% higher than the calculated ones. A large proportion of these cost increases accounted for work that only occurred after the programs had actually been completed, especially in the test and commissioning phase. Even conceptual errors were discovered in these phases. Necessary corrections, changes or additions to software components also had a particularly catastrophic effect, since large systems were often difficult to survey. In particular, the interaction of the individual components and the behavior of the system in extreme situations was not predictable. Against the background of these developments, the first approaches to solving these problems arose under the term software engineering from the early 1970s. It had been recognized that only an engineering, i.e. methodical and rational approach in the creation of software could bring improvements. Especially for the phases before the actual programming, tools had to be made available that made it possible to exactly describe the requirements for a software system, to convert this requirement description into a processing-oriented form, and to document the software design process adequately. To date, numerous tools and methods have been developed to support SW design, which were primarily designed for use in commercial applications that are characterized by purely sequential processing. On the other hand, if one does not consider sequential systems, most of the design methods that have arisen can no longer be used because of the much more complex requirements. For example, Systems for data processing, automation software or dialog systems require mechanisms for synchronization and priority-controlled processing of the individual, parallel running system components. Another important aspect is the protection of shared resources or data from unauthorized access, destruction or modification. This also applies to the processing of personal data, e.g. protection in medical applications or in the human resources of a manufacturing company, protection against unauthorized disclosure. For these applications in particular, methods that enable the design of reliable software that is as verifiable as possible are of particular interest. On the one hand, the construction of non-sequential systems is generally a very difficult area, so that the possibilities of error compared to commercial applications are much greater and errors are much more difficult to identify and to correct, since they often only occur in certain system constellations and are not reproducible. On the other hand, software errors often have a catastrophic effect here. Consider, for example, the control and monitoring of production lines, a flexible manufacturing system or even a nuclear power plant. The aim of this work is therefore the development of tools for the construction of reliable software systems, taking into account parallel processes and protection requirements. The methodology presented here offers a uniform approach for the specification and implementation of protected, asynchronous systems, whereby an essential property of the selected specification constructs is a simple derivation option for the associated implementation. Finally, verification conditions can be specified to prove reliability. A formal mathematical model that defines the semantics of the methodology serves as the basis for the specification and implementation methodology for asynchronous, protected systems specified in this work. The path via a formal model was chosen for reasons of generality of the approach. Another advantage of using the formal model is the ability to answer application-related questions such as the compatibility of asynchronous activities to formulate or clarify in the formal model. Finally, the basis of the model for the specification as well as the implementation decisively promotes the uniformity of the approach, the simple derivation of the implementation from the specification and the easy verifiability of the correctness of the implementation. At this point it should be mentioned that three dissertations (, , ) were written last year at the Institute for Mathematical Machines and Data Processing at the University of Erlangen-Nuremberg, which deal with tasks that are involved in this work goal are partially related. However, each of these papers looks at the broad subject area of developing methods for the construction of reliable software systems with a different focus, so that the present work and these dissertations complement each other: While recovery measures to increase reliability are mainly examined in , limited Mackert in on asynchronous systems without protection requirements. Finally, protection aspects are taken into account in , but the approach chosen there is purely linguistic. In contrast to the present work, there is no formal modeling as the basis of the specification and implementation concept. In addition, the definition of protection chosen there does not take into account the dynamics of calculations or problems arising in connection with semantic querying and changes. In the following, an overview of the focal points dealt with in this work will be given. The work begins with an overview of the specifics of software systems for real-time applications in production. Based on a presentation of typical tasks, the requirements for hardware and software in these applications are explained. The most basic requirement is the reliability of the components and software modules used. For software development, this means the need to use software engineering methods. Finally, the necessary extensions compared to existing methods are explained. In Chapter 3 of the thesis, principles and methods for the construction of reliable software systems are presented. It starts with a description of the characteristics and quality characteristics of the product software - in contrast to other, conventional technical products. The following explanation of the SW life cycle, i.e. of the individual phases within the software development, then leads to an overview of various software design principles. Here, among other things the terms abstraction, modularization, structuring, locality, specification and verifiability explained. The implementation of these principles then shows (more or less) in the existing methods for software engineering, which are to be briefly presented. The most suitable method for program design turns out to be the concept of abstract data types, since it automatically fulfills all the design principles explained. It is therefore used in this work as a basic concept for the formal model to be developed, the specification method and the implementation. Abstract data types provide the designer of a system with a basis for procedural and data abstraction and, per se, define a consistent model for objects. Finally, the object management mechanisms to be integrated into the ADT concept, such as synchronization of access to objects and protection aspects, are briefly explained. In Chapter 4 of the thesis, the existing methods for implementing protection and security mechanisms are presented in detail. The necessity for this arises from the requirement to integrate protective mechanisms into the ADT concept. The chapter begins with the presentation of pure access protection models, e.g. the Harrison model or the Take Grant models. Military security models, such as the Bell LaPadula model and the Feiertag model, are then presented. In information flow models, both purely syntactic approaches (Denning) and semantic (Cohen) are taken into account. All of these models are limited to a very specific sub-aspect of the overall protection area and are therefore not complete. The Goguen and Stoughton models attempt to avoid this deficiency, since both access protection and information flow aspects are taken into account here. Finally, all models presented are compared with each other and measured in particular against the requirements that were made of a formal model for object management in Chapter 5. Finally, the requirements that arise from the point of view of the area of protection for our general property management model are summarized. Chapter 5 then deals with the creation of the formal model for object management. The basis for this is the so-called operating system machine , a general formal model for operating systems. This model is expanded in two steps here: Protective constructs are first integrated into the original operating system machine and various options for defining query and changing a variable through an operation are discussed - as the basis for protection and synchronization questions. The concept of abstract data types is then integrated into the extended operating system machine as the basis for procedural and data abstraction. A formal definition of abstract data types and the associated object management mechanism, the so-called abstract object management machine, forms the basis for further investigations. The options for defining protection strategies (policies) are discussed in detail in the model and the concept of the security of an ADT, which is fundamental for the reliability of a system, is defined. Building on this formal model, a specification and implementation concept for synchronized, protected abstract data types is finally presented in Chapter 6 of the work. After classifying the concept and explaining the relationship between the formal model, the specification and implementation concept, the specification constructs are first specified. The syntax defined in is essentially adopted and expanded to include language constructs for the protection mechanisms introduced. Finally, verification rules and examples are given for the verification of the security of synchronized, protected ADTs at the specification level and the correct implementation of specifications. Chapter 7 concludes with the specification of a larger example from the field of automation. Here the applicability of the presented language constructs in practice and the necessity of design support for software systems for real-time applications in production are clearly demonstrated again.

Abstract

Durch die zunehmende Ausbreitung der elektronischen Datenverarbeitung, den laufenden Preisverfall bei der Hardware und die Lösung immer komplexerer Probleme durch Programmsysteme gewann die Software im letzten Jahrzehnt immer mehr an Bedeutung. So verschob sich in diesem Zeitraum das Verhältnis der Software- zu Hardwarekosten bei DV-Installationen kontinuierlich zugunsten der Software, und der Anteil der Software liegt heute bei komplexeren Anwendungen in Größenordnungen von 90 %. Erstaunlicherweise stand dieser wachsenden Bedeutung der Software bis vor wenigen Jahren ein Vorgehen bei der Erstellung von Software gegenüber, das weder als methodisch, noch als rationell zu bezeichnen war. Die Konsequenz daraus war die vielzitierte SW-Krise mit qualitativ schlechten Programmen und oftmals erschreckend hohen Kosten für deren Erstellung. Die realen Kosten für die Software lagen häufig um bis zu 100 % höher als die kalkulierten. Einen großen Anteil an diesen Kostensteigerungen machten hier Arbeiten aus, die erst nach der eigentlichen Fertigstellung der Programme, vor allem in der Test- und Inbetriebnahmephase anfielen. Selbst konzeptionelle Fehler wurden noch in diesen Phasen entdeckt. Besonders katastrophal wirkten sich auch notwendige Korrekturen, Änderungen oder Ergänzungen von SW-Komponenten aus, da große Systeme oftmals nicht überblickbar waren. Insbesondere war das Zusammenspiel der Einzelkomponenten und das Verhalten des Systems in Extremsituationen nicht vorhersehbar. Vor dem Hintergrund dieser Entwicklungen entstanden dann ab Anfang der 70er Jahre unter dem Begriff Software- Engineering erste Ansätze zur Lösung dieser Probleme. Man hatte erkannt, daß nur ein ingenieurmäßiges, d.h. methodisches und rationelles Vorgehen bei der Erstellung von Software Verbesserungen bringen konnte. Besonders für die Phasen vor der eigentlichen Programmierung mußten Hilfs2 mittel zur Verfügung gestellt werden, die es ermöglichten, die Anforderungen an ein SW-System exakt zu beschreiben, diese Anforderungsbeschreibung in eine verarbeitungsorientierte Form umzusetzen, und den SW-Entwurfsvorgang ausreichend zu dokumentieren. Bis heute entstanden so zahlreiche Werkzeuge und Methoden zur Unterstützung des SW-Entwurfs, die vor allem für den Einsatz bei kommerziellen Anwendungen, die durch eine rein sequentielle Verarbeitung gekennzeichnet sind, konzipiert waren. Betrachtet man dagegen nicht sequentielle Systeme, so sind die meisten der entstandenen Entwurfsmethoden wegen der wesentlich komplexeren Anforderungen nicht mehr einsetzbar. So erfordern z.B. Systeme zur Prozeßdatenverarbeitung, Automatisierungssoftware oder Dialogsysteme Mechanismen zur Synchronisation und prioritätengesteuerten Verarbeitung der einzelnen, parallel ablaufenden Systemkomponenten. Ein weiterer wichtiger Gesichtspunkt ist der Schutz gemeinsam genutzter Ressourcen oder Daten vor unerlaubtem Zugriff, Zerstörung oder Modifikation. Hierzu kommt bei einer Verarbeitung personenbezogener Daten, wie sie z.B. bei medizinischen Anwendungen oder im Personalwesen eines Fertigungsbetriebs vorkommt, noch ein Schutz vor unerlaubter Enthüllung. Gerade für diese Einsatzfälle sind nun aber Methoden, die den Entwurf zuverlässiger, möglichst verifizierbarer Software ermöglichen, von besonderem Interesse. Zum einen ist die Konstruktion nicht sequentieller Systeme ein im allgemeinen sehr schwieriges Gebiet, so daß die Fehlermöglichkeiten gegenüber kommerziellen Anwendungen wesentlich größer sind und Fehler wesentlich schwieriger zu erkennen und zu beheben sind, da sie oftmals nur bei bestimmten Systemkonstellationen auftreten und nicht reproduzierbar sind. Zum anderen wirken sich gerade hier Softwarefehler häufig katastrophal aus. Man denke beispielsweise an die Steuerung und Überwachung von Produktionslinien, eines flexiblen Fertigungssystems oder gar eines Kernkraftwerks. Ziel dieser Arbeit ist deshalb die Entwicklung von Hilfsmitteln zur Konstruktion zuverlässiger SW-Systeme unter Berücksichtigung paralleler Abläufe und Schutzanforderungen. Die hier präsentierte Methodik bietet dabei einen einheitlichen Ansatz für die Spezifikation und Implementierung geschützter, asynchroner Systeme, wobei eine wesentliche Eigenschaft der gewählten Spezifikationskonstrukte eine einfache Ableitungsmöglichkeit der zugehörigen Implementierung ist. Zum Nachweis der Zuverlässigkeit können schließlich Verifikationsbedingungen angegeben werden. Als Basis für die in dieser Arbeit angegebene Spezifikations- und Implementierungsmethodik für asynchrone, geschützte Systeme dient ein formales mathematisches Modell, das die Semantik der Methodik festlegt. Der Weg über ein formales Modell wurde dabei aus Gründen der Allgemeinheit des Ansatzes gewählt. Ein weiterer Vorteil, der sich durch die Zugrundelegung des formalen Modells ergibt, ist die Möglichkeit, anwendungsbezogene Fragen, wie z.B. die Verträglichkeit asynchroner Aktivitäten, bereits im formalen Modell zu formulieren bzw. zu klären. Schließlich wird durch die Zugrundelegung des Modells sowohl für die Spezifikation als auch Implementierung die Einheitlichkeit des Ansatzes, die einfache Ableitung der Implementierung aus der Spezifikation und die leichte Verifizierbarkeit der Korrektheit der Implementierung entscheidend gefördert. An dieser Stelle sei erwähnt, daß im letzten Jahr am Institut für Mathematische Maschinen und Datenverarbeitung der Universität Erlangen-Nürnberg drei Dissertationen (, , ) entstanden, die sich mit Aufgabenstellungen befassen, die dem in dieser Arbeit gesteckten Ziel teilweise verwandt sind. Jede dieser Arbeiten betrachtet jedoch das breite Themengebiet der Entwicklung von Methoden zur Konstruktion zuverlässiger SW-Systeme mit anderen Schwerpunkten, so daß sich die vorliegende Arbeit und diese Dissertationen gegenseitig ergänzen: Während in schwerpunktmäßig Recovery-Maßnahmen zur Zuverlässigkeitssteigerung untersucht werden, beschränkt sich Mackert in auf asynchrone Systeme ohne Schutzanforderungen. In schließlich werden zwar Schutzaspekte berücksichtigt, jedoch ist der dort gewählte Ansatz rein sprachlich. Es fehlt also im Gegensatz zur vorliegenden Arbeit eine formale Modellierung als Basis des Spezifikations- und Implement ierungskonfcepts. Zudem berücksichtigt die dort gewählte Definition von Schutz weder die Dynamik von Berechnungen noch im Zusammenhang mit semantischer Abfrage und Veränderung sich ergebende Probleme. Im folgenden soll nun eine überblicksartige Darstellung der in dieser Arbeit behandelten Schwerpunkte gegeben werden. Den Einstieg in die Arbeit bildet ein Überblick über die Spezifika von SW-Systemen für Echtzeitanwendungen in der Produktion. Ausgehend von einer Darstellung typischer Aufgabenstellungen werden die Anforderungen an Hardware und Software bei diesen Anwendungen erläutert. Grundlegendste Voraussetzung ist hierbei die Zuverlässigkeit der eingesetzten Komponenten und SW-Module. Für die SW-Erste1lung bedeutet dies die Notwendigkeit des Einsatzes von Methoden zum SW-Engineering. Abschließend werden die erforderlichen Erweiterungen gegenüber existierenden Methoden erläutert. Im Kapitel 3 der Arbeit werden dann Prinzipien und Methoden zur Konstruktion zuverlässiger SW-Systeme vorgestellt. Den Anfang bildet eine Darlegung der Charakteristika und Qualitätsmerkmale des Produkts Software - im Gegensatz zu anderen, herkömmlichen technischen Produkten. Die anschließende Erläuterung des SW-Life-Cycle, d.h. der einzelnen Phasen innerhalb der SW-Entwicklung, leitet dann über zu einem Überblick über verschiedene SW-Entwurfsprinzipien. Hier werden u.a. die Begriffe Abstraktion, Modularisierung, Strukturierung, Lokalität, Spezifikation und Verifizierbarkeit erläutert. Die Verwirklichung dieser Prinzipien zeigt sich dann (mehr oder weniger) in den existierenden Methoden für das SW-Engineering, die kurz vorgestellt werden sollen. Als geeignetste Methode für den Programmentwurf stellt sich hierbei das Konzept der Abstrakten Datentypen heraus, da es alle erläuterten Entwurfsprinzipien automatisch erfüllt. Es wird deshalb in dieser Arbeit als Basiskonzept für das zu entwickelnde formale Modell, die Spezifikationsmethode und die Implementierung verwendet. Abstrakte Datentypen stellen dem Designer eines Systems eine Basis für prozedurale und Datenabstraktion zur Verfügung und definieren per se ein konsistenzerhaltendes Modell für Objekte. Die darüber hinaus noch in das ADT-Konzept zu integrierenden Objektverwaltungsmechanismen, wie Synchronisation der Zugriffe auf Objekte und Schutzaspekte, werden abschließend kurz erläutert. Im Kapitel 4 der Arbeit werden ausführlich die existierenden Methoden zur Realisierung von Schutz- und Sicherungsmechanismen vorgestellt. Die Notwendigkeit hierfür ergibt sich dabei aus der Forderung der Integration von Schutzmechanismen in das ADT-Konzept. Den Einstieg in das Kapitel bildet die Vorstellung reiner Zugriffsschutzmodelle, wie z.B. das Modell von Harrison oder die Take-Grant-Modelle. Anschließend werden Modelle für militärische Sicherheit, wie das Bell-LaPadula-Modell oder das Modell von Feiertag präsentiert. Bei Informationsflußmodellen werden, sowohl rein syntaktische Ansätze (Denning), als auch semantische (Cohen) berücksichtigt. Alle diese Modelle beschränken sich auf einen ganz bestimmten Teilaspekt des Gesamtgebiets Schutz, sind also nicht vollständig. Dieser Mangel wird bei den Modellen von Goguen und Stoughton zu vermeiden versucht, da hier sowohl Zugriffsschutz- als auch Informationsflußaspekte berücksichtigt werden. Abschließend werden alle präsentierten Modelle miteinander verglichen und insbesondere an den Anforderungen, die in Kapitel 5 an ein formales Modell zur Objektverwaltung gestellt wurden, gemessen. Schließlich werden die Forderungen, die sich aus der Sicht, des Gebiets Schutz an unser allgemeines Objektverwaltungsmodell stellen, zusammenfassend dargelegt. Gegenstand des Kapitels 5 ist dann die Erstellung des formalen Modells zur Objektverwaltung. Basis hierfür ist die sogenannte Betriebssystemmaschine , ein allgemeines formales Modell für Betriebssysteme. Dieses Modell wird hier in zwei Schritten erweitert: Zunächst werden in die ursprüngliche Betriebssystemmaschine Schutzkonstrukte integriert und verschiedene Möglichkeiten der Definition von Abfrage und Veränderung einer Variablen durch eine Operation - als Basis für Schutz- und Synchronisationsfragen - diskutiert. Anschließend wird das Konzept der Abstrakten Datentypen als Grundlage für prozedurale und Datenabstraktion in die erweiterte Betriebssystemmaschine integriert. Eine formale Definiton Abstrakter Datentypen und des zugehörigen Objektverwaltungsmechanismus, der sogenannten abstrakten Objektverwaltungsmaschine, bildet die Grundlage für die weiteren Untersuchungen. So werden ausführlich die Möglichkeiten zur Definition von Schutzstrategien (policies) im Modell diskutiert und der für die Zuverlässigkeit eines Systems grundlegende Begriff der Sicherheit eines ADT's definiert. Aufbauend auf diesem formalen Modell wird schließlich in Kapitel 6 der Arbeit ein Spezifikations- und Implementierungskonzept für synchronisierte, geschützte Abstrakte Datentypen präsentiert. Nach einer Einordnung des Konzepts und der Erläuterung des Zusammenhangs zwischen formalem Modell, Spezifikations- und Implementierungskonzept werden zuerst die Spezifikationskonstrukte angegeben. Hierbei wird die in definierte Syntax im wesentlichen übernommen und um Sprachkonstrukte für die eingeführten Schutzmechanismen erweitert. Für die Verifikation der Sicherheit synchronisierter, geschützter ADTs auf Spezifikationsebene und die korrekte Implementierung von Spezifikationen werden schließlich Verifikationsregeln und Beispiele angegeben. Den Abschluß der Arbeit bildet in Kapitel 7 die Spezifikation eines größeren Beispiels aus dem Bereich der Automatisierung. Hier wird die Anwendbarkeit der präsentierten Sprachkonstrukte in der Praxis und auch die Notwendigkeit der Entwurfsunterstützung bei SW-Systemen für Echtzeitanwendungen in der Produktion noch einmal deutlich dargelegt.

Series
Fertigungstechnik - Erlangen
Series Nr.
[0]
Notes
Nach Genehmigung durch den Autor digitalisiert und online gestellt durch Geschäftsstelle Maschinenbau und Universitätsbibliothek der FAU im Jahr 2020. Koordination der Reihe: Dr.-Ing. Oliver Kreis. Für weitere Informationen zur Gesamtreihe siehe https://mb.fau.de/diss
Faculties & Collections
Zugehörige ORCIDs