Keywords: Paradigma der deduktiven Synthese zur Entwicklung ganzer verifizierter Systeme, einschließlich Hardware und Mechanik, angewendet werden kann

Using the synthesis approach of Manna and Waldinger, a formally specified and verified control circuitery for a production cell was developped. Building an appropriate formal language level, we could achieve a requirements specification to the informal description. We demonstrated that the paradigm of deductive synthesis can be applied to the development of complete verified systems, including hardware and mechanics. We defined two domain-specific logical operators that schematise frequent patterns in specification and proof and hence allow a more concise and expressive presentation. In [Bur95], an english short version of this paper, without appendices, can be found.

Einleitung

Die Fallstudie "Fertigungszelle" kommt aus dem Bereich Regeln und Steuern. Aufgabe ist die Entwicklung verifizierter Steuerungs-Software für ein Modell einer Anlage, wie sie bei einer metallverarbeitenden Firma in Karlsruhe steht. Sie bearbeitet Metallrohlinge, die auf einem Zuführförderband an eine Presse gelangen. Ein Roboter nimmt die Metallrohlinge vom Zuführförderband und legt sie in die Presse. Der Roboterarm verläßt die Presse, die Presse verarbeitet die Metallrohlinge und öffnet sich wieder. Der Roboter nimmt das verarbeitete Metallplättchen aus der Presse und legt es auf ein Ablageförderband.

Ziel der Bearbeitung der Fallstudie war vor allem zu untersuchen, wie weit der begriffliche Abstand zwischen vorgegebener informeller Anforderungsbeschreibung und formaler Spezifikation verringert werden kann. Durch die Erstellung einer geeigneten formalen Sprachebene unter starker Ausnutzung impliziter Spezifikationstechnik und unter Einbeziehung auch mechanischer Aspekte konnte erreicht werden, daß die Spezifikation lokal validierbar ist, d.h. durch eine satzweise " Übersetzung" der Anforderungsbeschreibung in formale Notation entstanden ist. Insbesondere ist das Spezifikationsziel die formale Entsprechung der Anforderung: "Wenn ein unbearbeitetes Werkstück auf dem Zuführförderband liegt, erscheint es später bearbeitet auf dem Ablageförderband". Mit dieser Herangehensweise kann das Problem der Vertrauenswürdigkeit einer Spezifikation weitgehend entschärft werden.

Die formale Spezifikation zeichnet sich durch folgende Merkmale aus:

-Spezifikation in Prädikatenlogik 1. Stufe, modular gegliedert, -Zeit als expliziter Parameter, -Einbeziehung auch mechanischer und geometrischer Aspekte, -Beschreibung der einzelnen Maschinen und ihrer Anordnung, nicht: Programmierung der Steuerung in einer Spezifikationssprache.

Daraus wurden mit Hilfe des Unterstützungswerkzeugs "Sysyfos" notwendige Zeitbedingungen für die Steuerung der Fertigungszelle hergeleitet und schließlich eine Ttl-artige digitale Hardware-Steuerschaltung konstruiert, die die Zeitbedingungen erfüllt.

Durch die Einbeziehung auch mechanischer und geometrischer Aspekte in die Modellierung konnte der Ansatz der deduktiven Synthese von der reinen Steuerungsentwicklung zu einem methodischen Rahmen für die integrierte Bearbeitung aller beim Entwurf der Fertigungszelle anfallenden ingenieurtechnischen Aspekte ausgeweitet werden. Zum Beispiel wurden auch notwendige Bedingungen an die Aufstellung der Maschinen (Abstände, Winkel, usw.) aus der Spezifikation hergeleitet.

Aufgrund der während der Entwicklung gemachten Erfahrungen wurden im Nachhinein zwei logische Operatoren definiert, die eine Schematisierung der in Spezifikation und Beweis häufig vorkommenden Aussagenmuster darstellen und mit deren Hilfe sich beide erheblich kürzer und klarer darstellen lassen. Beide Operatoren sind monoton bzw. anti-monoton in jeweils beiden Prädikatargumenten und konnten daher problemlos als benutzerdefinierte Junktoren in die verwendete polaritätsbasierte Nicht-Klausel-Resolution eingebaut werden. Zusammen mit einer Hintergrundtheorie über ihre wichtigsten Eigenschaften bilden sie eine Grundlage für die Bearbeitung zustandsorientierter Aspekte auf einem anwendungsnahen sprachlichen Niveau. Dieser grundlegende Ablauf wird durch weitere Mechanismen kompliziert:

Nach einer informellen

-Um eine bessere Auslastung der Presse zu erzielen, wurde der Roboter mit zwei Armen ausgestattet. So kann der zweite Arm während des Pressens bereits einen neuen Rohling aufnehmen. Beide Arme stehen im unveränderlichen Winkel von 90 • zueinander und können gemeinsam gedreht werden. Jeder der Arme kann horizontal ein-und ausgefahren werden. Die horizontale Beweglichkeit ist wegen der unterschiedlichen Abstände zum Drehzentrum des Roboters beim Be-und Entladen nötig. -Die beiden Roboterarme befinden sich nicht auf der gleichen Höhe. Außerdem sind sie nicht vertikal beweglich. Deshalb wurde im Anschluß an das Zuführförderband ein Hubdrehtisch (hub) eingefügt. Er hat die Aufgabe, die Metallplättchen auf die Höhe des ersten Roboterarmes anzuheben und um etwa 45 • zu drehen, so daß sie im richtigen Winkel von ihm aufgenommen und in die Presse gelegt werden können. Der Greifer des Roboterarms ist selbst nicht drehbar. -Ebenfalls wegen des unterschiedlichen Niveaus der Roboterarme hat die Presse nicht nur zwei, sondern drei Zustände: geöffnet zur Entladung durch den unteren Arm (2), geöffnet zur Beladung durch den oberen Arm (1), geschlossen (pressend). -Um das Modell bei Demonstrationen einsetzen zu können, soll der Fertigungsvorgang bedienungsunabhängig ablaufen können. Aus diesem Grund werden die "verarbeiteten" Metallplatten (von der Modell-Presse unverändert gelassen) vom Ablageförderband durch ein Handhabungsgerät (han) wieder zum Zuführförderband gebracht und der Gesamtvorgang dadurch zyklisch gemacht. Das Handhabungsgerät besitzt einen als Elektromagnet realisierten Greifer, der horizontal und vertikal beweglich ist. Die horizontale Beweglichkeit dient zur Bewältigung der Strecken zwischen den beiden Förderbändern, die vertikale Beweglichkeit ist notwendig, da die Bänder unterschiedlich hoch sind.

Der generelle Ablauf ist (sequentialisiert aus der Sicht eines Metallplättchens):

-Über das Zuführförderband gelangt das Metallplättchen auf den Hubdrehtisch.

-Der Hubdrehtisch wird in die dem aufnehmenden ersten Roboterarm angemessene Position gebracht. -Der erste Roboterarm nimmt das Metallplättchen auf.

-Der Roboter dreht sich, so daß Arm 1 in die geöffnete Presse zeigt, legt das Metallplättchen dort ab und verläßt die Presse. -Der Roboter nimmt mit seinem zweiten Arm das Metallplättchen auf, dreht sich weiter und legt das Metallplättchen auf das Ablageförderband.

-Über das Ablageförderband gelangt das Metallplättchen zum Handhabungsgerät.

-Das Handhabungsgerät nimmt das Metallplättchen auf, fährt zum Zuführförderband und legt das Metallplättchen dort wieder ab.

Dies ist eine vereinfachte Beschreibung. Dabei besteht die Vereinfachung zum einen in der groben Beschreibung der einzelnen Einheiten. Zum anderen ist die Anlage so ausgerichtet, daß mehrere Metallplatten gleichzeitig verarbeitet und transportiert werden; das soll gerade so geschehen, daß die Anlage optimal ausgenutzt ist. 

⇒ ⇒ ⇒ ⇓ ⇑ ⇓ ⇑ ⇓ ⇑ 1⇐ 1⇒ 12⇐ 12⇒ 12⇐ 12⇒ 2⇐ 2⇒ ⇑ ⇑ ⇓ ⇑ ⇑ ⇓ ⇑ ⇑ ⇓ ⇒ ⇒ ⇒ Fig. 3.

Paramodulation

In [START_REF] Manna | Special relations in automated deduction[END_REF] definieren Manna und Waldinger unter dem Namen "Relation Replacement" (rp in Abb. 4) eine Verallgemeinerung der Paramodulation, die erstens keine Klauselform voraussetzt und zweitens nicht nur bzgl. einer Äquivalenzrelation "=", sondern bzgl. beliebiger Relationen " " arbeitet, sofern die entsprechenden Funktionen und Prädikate monoton sind (Schritte 8 bis 10 in Abb. 5). Im Sysyfos-System wird zusätzlich gefordert, daß transitiv ist, dann dürfen in G auch mehrere Ersetzungen von s und t vorgenommen werden.

Assertions Goals

Resolution:

F [p m ] G[p -m ] F [¬m•G[(-m)•true]] rs(1,2) Beispiel: rob(R) ∧ T0 t T1 → drv(R, t) val(C7, T ) = 1 → drv(r(C7), T ) rob(r(C7)) ∧ T0 t T1 → ¬(val(C7, t) = 1 → ¬true) rs(4,5) rob(r(C7)) ∧ T0 t T1 → val(C7, t) = 1 simp(6)
Paramodulation: ¨$$ $ @ @ @ @ @ r r 

F [s t] G t + , s - ¬F [f alse] ∧ G s + , t - rp(8,9) Beispiel: ha1(R, S, T ) → win(S, T ) = wxy(x, ps1(R, T )) -90 win(s0, t) = 180 ¬(ha1(R, s0, t) → f alse) ∧ wxy(x,
∀[r, x, t, d] ( roboter(r, x) ∧ dist xy(x, pos1(r, t)) d maxlg1 → (∀[t1] (t t1 < tra1(r, d, t) → f aehrt aus1(r, t1)) → dist xy(x, pos1(r, tra1(r, d, t))) = d) ∧ ∀[t3] (t t3 < tra1(r, d, t) → dist xy(x, pos1(r, t3)) < d)) u21. ∀[r, x, t, t2] ( roboter(r, x) ∧ t t2 ∧ dist xy(x, pos1(r, t)) < dist xy(x, pos1(r, t2)) → ∃[t1] (t < t1 < t2 ∧ f aehrt aus1(r, t1))) u30. ∀[c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3, x, t] ( roboter(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), x) → (f aehrt aus1(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), t) ↔ val(c1, t) = 1) ∧ (f aehrt ein1(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), t) ↔ val(c2, t) = 1)
∧ (f aehrt aus2(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), t) ↔ val(c3, t) = 1) ∧ (f aehrt ein2(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), t) ↔ val(c4, t) = 1) ∧ (greif t1(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), t) ↔ val(c5, t) = 1) ∧ (greif t2(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), t) ↔ val(c6, t) = 1) ∧ (dreht vor(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), t) ↔ val(c7, t) = 1)

∧ (dreht zurueck(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), t) ↔ val(c8, t) = 1) ∧ (dist xy(x, pos1(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), t)) = val(s1, t)) ∧ (dist xy(x, pos2(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), t)) = val(s2, t)) ∧ (winkel xy(x, pos1(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), t)) = val(s3, t))) u47b. dist xy(d4, d3) maxlg1 u73. ∀[c, v, t] ( val(trigger(c, v), t) = 1 ↔ val(c, t) < v) r11.
roboter(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), d4) Beweis (Skolem-Funktionen markiert mit " $ "):

Vor: dist xy(d4, pos1(r0, t $ 0 )) d34
Beh: dist xy(d4, pos1(r0, t)) = d34 51 = u20 rs Vor , r11 , u47b:

( (t $ 0 t1 < t $ 2 → f aehrt aus1(r0, t1)) → dist xy(d4, pos1(r0, t $ 2 )) = d34) ∧ t $ 0 t3 < t $ 2 → dist xy(d4, pos1(r0, t3)) < d34 52 = sp 51: (t $ 0 t1 < t $ 2 → f aehrt aus1(r0, t1)) → dist xy(d4, pos1(r0, t $ 2 )) = d34 53 = sp 51: t $ 0 t3 < t $ 2 → dist xy(d4, pos1(r0, t3)) < d34 54 = 52 rs u30: (t $ 0 t1 < t $ 2 → val(c1, t1) = 1) → dist xy(d4, pos1(r0, t $ 2 )) = d34 55 = 54 rs u73: (t $ 0 t1 < t $ 2 → val(c, t1) < d34) → dist xy(d4, pos1(r0, t $ 2 )) = d34 mit r0 = r(trigger(c, d34), c2, c3, . . . , c8, s1, s2, s3) 56 = 55 rp u30: (t $ 0 t1 < t $ 2 → dist xy(d4, pos1(r0, t1)) < d34) → dist xy(d4, pos1(r0, t $
2 )) = d34 mit r0 = r(trigger(s1, d34), c2, c3, . . . , c8, s1, s2, s3) 57 = 56 rs 53:

dist xy(d4, pos1(r0, t $ 2 )) = d34 mit r0 = r(trigger(s1, d34), c2, c3, . . . , c8, s1, s2, s3) S d34 q q q q q q q q q q q q q Fig. 11 Jeder Knoten beginnt mit der Formelnummer, unmittelbar gefolgt von der Operation, aus der die Formel entstanden ist (siehe Abb. 4 für die verwendeten Abkürzungen). Für Axiome wurde dabei ihr eindeutiger Name angegeben; die Angabe "**" steht für eine bereits früher verwendete Formel. Schließlich folgt entweder "F , -" für Assertions oder "-, F " für Goals, wobei F die aktuelle Formel in Prolog-Notation ist (siehe Abb. 18). Ein "$" nach einem Namen deutet an, daß es sich um eine Skolemfunktion handelt, deren Argumente nicht angezeigt werden; ein "()" deutet an, daß die Argumente manuell entfernt wurden. Man beachte, daß Äquivalenzen vom System in Konjunktionen von Implikationen aufgelöst werden, um eindeutige Polaritäten zu erreichen.

Jede Formel ergibt sich aus der (bzw. den beiden) darüber liegenden um zwei Spalten nach rechts eingerückten Ausgangsformel(n), je nach Stelligkeit der angewendeten Operation. Weiter entfernte Ausgangsformeln werden durch senkrechte Striche verbunden.

Der Beweisbaum wird automatisch soweit als möglich linearisiert. Dazu werden in manchen Fällen die beiden Ausgangsformeln einer zweistelligen Operation vertauscht, was durch Großschreibung der entsprechenden Abkürzung angedeutet ist. Zum Beispiel ist die Formel 158 in Anhang C entstanden durch die Operation rp(114, 157). Man beachte, daß an der Wurzel des Beweisbaums die noch offene Rest-Beweisverpflichtung steht (Formel 325). 

= = (höchste Bindungsstärke) =< < < ~¬ . & ∧ . ! ∨ . -> → <- ← (niedrigste Bindungsstärke)

Verwendung höherer logischer Operatoren

Ein zweiter Ansatz verwendete die bisher gemachten Erfahrungen und identifizierte höhere Sprachkonzepte, die es erlaubten, sowohl die Spezifikation als auch den Verifikationsbeweis auf eine höhere Ausdrucksebene zu heben. Es wurden zwei neue dreistellige logische Operatoren definiert, indem sie auf eine eingeschränkte Form der Prädikatenlogik zweiter Ordnung zurückgeführt wurden, siehe Abb. 21.

unt(t0, P, Q) ⇔ ∀t1 : t1 < t0 ∨ (∃t : t0 t t1 ∧ Q(t)) ∨ P (t1) ldt(t0, P, Q) ⇔ ∃t1 : t0 t1 ∧ (∀t : (t0 t t1 → P (t)) → Q(t1))

∧ (∀t : t0 t t1 → ¬Q(t))

Fig. 21. Anwendungsspezifische logische Operatoren

Die Konzepte wurden von der Sprache Unity von Misra und Chandy [START_REF] Chandy | Parallel Program Design[END_REF] übernommen. Die Formel unt(t 0 , P, Q) besagt, daß ab dem Zeitpunkt t 0 das einstellige Prädikat Q solange wahr ist, bis das einstellige Prädikat P wahr wird, ggf. für immer ("P until Q"). Die Formel ldt(t 0 , P, Q) besagt, daß, wenn ab dem Zeitpunkt t 0 das Prädikat P nur lange genug gilt, Q irgendwann wahr wird, und daß es dafür einen frühesten Zeitpunkt t 1 gibt ("P leads to Q").

∀t0 : unt(t0, P, Q) ↔ ∀t : t0 t ∧ (∀t1 : t0 t1 < t → ¬Q(t1)) → P (t) ∀t0 : P (t0) → unt(t0, P, Q) ∀t0 : unt(t0, P, Q) → P (t0) ∀t0 : P (t0) ∨ Q(t0) ↔ unt(t0, P, Q) ∨ unt(t0, Q, P ) ∀t0 : unt(t0, P, ¬P ) ∀t0 : unt(t0, P, Q) ∨ unt(t0, ¬Q, ¬P ) ∀t0 : unt(t0, P, Q ∨ R) ↔ unt(t0, P, Q) ∨ unt(t0, P, R) ∀t0 : unt(t0, P, f alse) ↔ ∀t : (t0 t → P (t)) ∀t0 : unt(t0, P, Q) ∧ unt(t0, R, S) → unt(t0

, P ∨ R, Q ∧ S) ∀t0 : unt(t0, P, Q) ∧ unt(t0, R, S) → unt(t0, P ∧ R, Q ∨ S) ∀t0 : unt(t0, P, Q) ∧ unt(t0, R, ¬P ) → unt(t0, P ∧ R, Q) ∀t0 : unt(t0, true, Q) ∀t0 : unt(t0, f alse, Q) ↔ (∀t : t0 t → ∃t1 : t0 t1 < t ∧ Q(t1)) ∀t0 : (Q → ¬R) → (ldt(t0, P ∧ R, Q) ↔ ldt(t0, P, Q)) ∀t0 : t0 t2 ∧ Q(t2) → ldt(t0, true, Q) ∀t0 : ldt(t0, P, Q) ∧ (∀t : R(t)) → ldt(t0, P, Q ∧ R)
∀t0 : ldt(t0, true, P ) ↔ ∀t0 : ∃t1 : t0 t1 ∧ P (t1) ∀t0 : ldt(t0, ¬P, P ) → ∃t : t0 t ∧ P (t) ∀t0 : ldt(t0, P, Q) ∧ unt(t0, ¬R, Q) → ldt(t0, P, Q ∨ R) ∀t0 : ldt(t0, P ∧ Q, R) ∧ unt(t0, P, R) → ldt(t0, Q, R) ∀t0 : unt(t0, P, Q) ∧ t0 t1 ∧ ¬P (t1) → ldt(t0, P, Q) Man beachte, daß Ketten von ldts Zustandsübergänge wie bei endlichen Automaten modellieren können, Abb. 24 zeigt ein Beispiel. Innerhalb des Bmft-Projekts "Korrekte Software (Korso)" wurde die Fertigungszelle u.a. mit Hilfe der Sprache Lustre als eine Art endlicher Automat modelliert, so daß die wichtigsten Anforderungen vollautomatisch mit Hilfe von Binary Decision Diagrams verifiziert werden konnten [START_REF] Holenderski | A verified production cell controller specified in LUSTRE[END_REF]. Ein solcher Ansatz kann jedoch nur Aspekte behandeln, die sich als Automateneigenschaften darstellen lassen. Es wäre interessant zu untersuchen, ob sich durch den unt/ldt-Ansatz eine vertikale Dekomposition des Modells erreichen läßt in dem Sinne, daß auf der oberen Ebene nur Automateneigenschaften betrachtet werden müssen, während alle anderen Eigenschaften auf der unteren Ebene behandelt werden.

Bewertung

Modellierbare Eigenschaften

Der hier vorgestellte Ansatz macht es leicht, alle verlangten Lebendigkeits-und Sicherheitseigenschaften zu formulieren und nachzuweisen. Die Lebendigkeitseigenschaft besagt, daß jedes unbearbeitete Metallplättchen, das in die Fertigungszelle hineingegeben wird, sie irgendwann im bearbeiteten Zustand wieder verläßt; siehe die Diskussion am Ende des Abschnitts 4.1. Die Sicherheitseigenschaften können in der zusätzlichen Anforderung "Es darf nie zu Unfällen kommen" zusammengefaßt werden, wobei eine notwendige Bedingung für einen Unfall durch eine entsprechende Aufzählung aller kritischen Maschinenkombinationen (z.B. Roboter/Presse) beschrieben wird.

Ein Nachteil dieses Vorgehens besteht in dem Risiko, beim Schreiben der Spezifikation bestimmte mögliche Konfliktsituationen zu übersehen. So war z.B. in der ersten Version der informellen Beschreibung der Sicherheitsanforderungen nicht verlangt, daß das Zuführförderband nur dann Metallplättchen transportieren darf, wenn der Hubdrehtisch leer ist.

Jede der informellen Sicherheitsanforderungen aus Abschnitt 2.3 ergibt sich aus einem der folgenden Prinzipien:

-Maschinenkollisionen müssen vermieden werden (1, 2, 5, 6), die Beweglichkeitsbeschränkungen der Maschinen müssen respektiert werden (3, 4, 5), -Metallplättchen dürfen nicht aus großer Höhe herabfallen (7, 9), die Metallplättchen müssen genügend gut separiert bleiben (8, 10).

Es ist grundsätzlich möglich, die Sicherheitsanforderungen an die Fertigungszelle auf diese vier Prinzipien zu gründen. Eine Formalisierung des ersten Prinzips verlangt jedoch eine vollständige Beschreibung aller Maschinenabmessungen einschließlich ihrer Bewegungsbahnen und darüber hinaus für jedes der n • (n -1) Maschinenpaare einen Beweis, daß sie nicht zusammenstoßen können, unabhängig davon, wie weit sie tatsächlich voneinander entfernt stehen. Da beides sehr aufwendig ist, haben wir uns stattdessen dazu entschlossen, die möglichen Kollisionssituationen explizit anzugeben.

Explizitheitsgrad

Die Voraussetzungen über das Maschinenverhalten und über die Gesamtkonfiguration der Fertigungszelle sind in den entsprechenden Modulen der Spezifikation explizit aufgeführt. Darüber hinaus ist es möglich, während des Beweises weitere benötigte Anforderungen an Verhalten oder Konfiguration abzuleiten, siehe Abschnitt 4.2.

Statistik

Es ist schwierig, den Zeitaufwand für die Durchführung des Beweises abzuschätzen, da parallel dazu das Unterstützungswerkzeug Sysyfos weiterentwickelt werden mußte, um den Beweis überhaupt in den Griff zu bekommen. Als Nebenergebnis der Fallstudie wurde eine halbgraphische Benutzeroberfläche und ein Beweiswiederholungs-Mechanismus in das Werkzeug eingebaut; in der zweiten Phase erforderte die eingeschränkte Unifikation höherer Ordnung für unt und ldt einige Implementierungsarbeit. Unter diesen Vorbehalten kann der Aufwand für das Finden bzw. Verifizieren der Teilschaltung zum Transport eines Metallplättchens vom Hubdrehtisch in die Presse mit etwa 1 bis 2 Mannwochen angegeben werden. Dieser Teilbeweis besteht aus 210 Schritten ohne die Verwendung von unt und ldt und war der erste Teilbeweis innerhalb der Fallstudie. Ein später durchgeführter vergleichbar großer Teilbeweis benötigte größenordnungsmäßig nur noch 1 bis 2 Manntage, hauptsächlich aufgrund der vorhandenen Erfahrungen speziell bzgl. der in Abschnitt 4.3 diskutierten Stetigkeitsaspekte.

Wartung

Der Hauptaufwand für die Entwicklung einer Steuerung für eine geänderte, vergleichbare Fertigungszelle besteht im Führen eines neuen Beweises. Aufbauend auf der vorhandenen Terminologie sollte es leicht fallen, eine neue formale Spezifikation zu erstellen. Sofern der auf reiner Prädikatenlogik erster Ordnung basierende Ansatz verwendet wird, dürften nur wenige Teile des Originalbeweises wiederverwendbar sein, je nach dem Grad der Ähnlichkeit der beiden Spezifikationen. Im unt/ldt-Ansatz jedoch wurde ein großer Teil des Aufwandes in die Schematisierung von Steuerungswissen als Hintergrundtheoreme gesteckt, der beim zweiten Mal nicht wieder anfällt; siehe etwa Satz 61 in Abb. 23, der dort die zentrale Rolle im Beweis spielt. Wir würden erwarten, daß der verbleibende Beweisaufwand, um die Hintergrundtheoreme für die neue Situation geeignet zu instanziieren, eher gering ist. In jedem Fall ist jedoch der Aufwand, eine neue verifizierte Steuerungsschaltung zu erhalten, sehr viel größer als etwa der für die Rekonfiguration eines objektorientierten Steuerungsprogramms.

Effizienz

Das Paradigma der deduktiven Programmsynthese macht keine Aussagen über die Effizienz der konstruierten Programme. Darüber hinaus bedeutet Effizienz im Fall der Fertigungszelle nicht, kurze Software-Reaktionszeiten zu erreichen, sondern eine hohe Gesamtdurchsatzrate. Gemäß dem Ansatz, Software-Entwicklungsmethoden auch auf die Anwendung auf mechanische Probleme auszuweiten, könnte man die "algorithmische Komplexität" der gesamten Fertigungszelle abschätzen. Dazu wäre eine entsprechende Verallgemeinerung eines Komplexitätskalküls für reaktive Systeme notwendig. Da in der Fertigungszelle keine Rekursion auftritt, könnte die maximale Bearbeitungszeit für ein Metallplättchen exakt berechnet werden. Etwa aus dem Teilbeweis in Anhang C ergibt sich die Zeit zum Zurückfahren des ersten Roboteramrs von der Presse zum Hubdrehtisch als trv 1 (r(. . .), winkel xy(d 4 , d 5 ), t 0 ) -t 0 , vgl. Formel 325. Ein Beweis dafür, daß die gefundene Konfiguration und Steuerung der Zelle einen maximalen Durchsatz garantiert, scheint jedoch ebenso schwierig wie der Nachweis unterer Komplexitätsschranken für gewöhnliche algorithmische Probleme.

Mechanische Anforderungen

Wie bereits in Abschnitt 4.2 erwähnt, wurden während der Synthese eine Reihe zusätzlicher Anforderungen an die Konfiguration der Fertigungszelle hergeleitet. Sie verlangen meist, daß die Beweglichkeitsbeschränkungen der Maschinen es ihnen erlauben, die benötigten Punkte tatsächlich zu erreichen, etwa, daß der erste Roboterarm den Hubdrehtisch erreichen kann, vgl. Axiom Unsere Modellierung basiert auf der idealisierenden Annahme, daß alle geometrischen Abmessungen exakt sind. In der Praxis wird dies jedoch nicht der Fall sein, etwa das Zuführband wird nicht jedes Metallplättchen genau bis zur Mitte des Hubdrehtischs (Punkt d 3 in Abb. 2) transportieren. Ein Modell der Fertigungszelle, das diesen Ungenauigkeiten Rechnung trägt, müsste mit zulässigen Toleranzintervallen umgehen können. So würde man z.B. in der Spezifikation fordern, daß der Roboter jedes Metallplättchen, das im Bereich d 3 + x mit ||x|| < ε 3 liegt, noch sicher aufnimmt und zur Presse transportiert. Jede Maschine würde ihre eigene Ungenauigkeit zum Toleranzintervall hinzufügen, in manchen Fällen dieses Intervall aber auch durch gewisse Ausrichtungseffekte wieder verkleinern, etwa bei Lichtschranken. Es müßte dann zusätzlich verlangt werden, daß die Toleranzintervalle klein genug bleiben, um die problemlose Weiterverarbeitung zu ermöglichen. Das Toleranzintervall eines Metallplättchens in der Presse zum Beispiel enthält die Toleranzen des ersten Roboterarms, des Hubdrehtischs, des Zuführförderbands und dessen (externen) Beladungsgeräts, es muß sichergestellt sein, daß diese Abweichung klein genug bleibt, um das Metallplättchen zuverlässig pressen zu können.

Thesen

Unsere Erfahrungen mit der Fertigungszelle scheinen folgende Thesen zu bestätigen:

-Eine gute Spezifikation sollte aus einer Sammlung beinahe offensichtlicher Fakten in formaler Notation bestehen. Der Verzicht auf Ausführbarkeit garantiert die Freiheit, die formalen Anforderungen als eine möglichst direkte Übersetzung der natürlichsprachlichen Beschreibung aufzustellen. Erstere können lokal (d.h. Axiom für Axiom, ohne Berücksichtigung von Querverweisen) gegen letztere validiert werden.

-Module der Anforderungsspezifikation beschreiben verschiedene Aspekte der modellierten Realität, nicht der Implementierung. Im Unterschied zu Entwurfsspezifikationen können sie nicht in Implementierungsmodule verfeinert werden, stattdessen sind sie zu ihnen orthogonal.

-Prädikatenlogik kann als eine "Assemblersprache" für Spezifikationen angesehen werden. Es ist wünschenswert, höhere, auch anwendungsabhängige, Sprachkonstrukte darauf aufzubauen, um kürzere Spezifikationen und Beweise zu erhalten.

-Formale Beschreibungen können bereits auf der obersten Ebene eingesetzt werden, auf der nur rein technische Aspekte auftreten. u6. Motorsteuerung und Sensoren c 1 : +1 hebt, 0 steht c 2 : +1 senkt, 0 steht s 1 : +1 unten s 2 : +1 mitte s 3 : +1 oben ∀[c1, c2, s1, s2, s3, x, t] ( presse(p(c1, c2, s1, s2, s3), x) → (hebt(p(c1, c2, s1, s2, s3), t) ↔ val(c1, t) = 1) ∧ (senkt(p(c1, c2, s1, s2, s3), t) ↔ val(c2, t) = 1) ∧ (hoehe(proj xy(x), t) = zp unten ↔ val(s1, t) = 1) ∧ (hoehe(proj xy(x), t) = zp mitte ↔ val(s2, t) = 1) ∧ (hoehe(proj xy(x), t) = zp oben ↔ val(s3, t) = 1)) u13. Wenn der Roboter mit Arm 1 eine Schiene hält und dann direkt über einer freien Arbeitsfläche losläßt, bleibt sie darauf liegen

∀[t] ∃[t2] ∀[p, x] ( presse(p, x) → (∀[t1] (t t1 < t2 → hebt(p, t1)) → hoehe(proj xy(x), t2) = zp oben) ∧ ∀[t3] (t t3 < t2 → ¬hoehe(proj xy(x), t3) = zp oben))
∀[r, x, t2, s, x1] ( roboter(r, x) ∧ ∃[t] (t < t2 ∧ ∀[t1] (t t1 < t2 → haelt1(r, s, t1))) ∧ ∀[s1] (ort(s1, t2) = x1 → s1 = s) ∧ pos1(r, t2) = x1 ∧ ¬greif t1(r, t2) ∧ hoehe(proj xy(x1), t2) = proj z(x1) → ort(s, t2) = x1)
u14. Wenn der Roboter mit Arm 2 eine Schiene hält und dann direkt über einer freien Arbeitsfläche losläßt, bleibt sie darauf liegen u21. Nur wenn Arm 1 ausfährt, kann seine Länge größer werden

∀[r, x, t2, s, x1] ( roboter(r, x) ∧ ∃[t] (t < t2 ∧ ∀[t1] (t t1 < t2 → haelt2(r, s, t1))) ∧ pos2(r, t2) = x1 ∧ ¬greif t2(r,
∀[r, x, t, t2] ( roboter(r, x) ∧ t t2 ∧ dist xy(x, pos1(r, t)) < dist xy(x, pos1(r, t2)) → ∃[t1] (t < t1 < t2 ∧ f aehrt aus1(r, t1)))
u22. Wenn Arm 1 nur lange genug einfährt, kann er jede Länge zwischen der jetzigen und minlg erreichen

∀[r, x, t, d] ( roboter(r, x) ∧ minlg1 d dist xy(x, pos1(r, t)) → (∀[t1] (t t1 < tre1(r, d, t) → f aehrt ein1(r, t1)) → dist xy(x, pos1(r, tre1(r, d, t))) = d) ∧ ∀[t3] (t t3 < tre1(r, d, t) → d < dist xy(x, pos1(r, t3))))
u23. Nur wenn Arm 1 einfährt, kann seine Länge kleiner werden

∀[r, x, t, t2] ( roboter(r, x) ∧ t t2 ∧ dist xy(x, pos1(r, t2)) < dist xy(x, pos1(r, t)) → ∃[t1] (t < t1 < t2 ∧ f aehrt ein1(r, t1)))
u24. Wenn Arm 2 nur lange genug ausfährt, kann er jede Länge zwischen der jetzigen und maxlg erreichen

∀[r, x, t, d] ( roboter(r, x) ∧ dist xy(x, pos2(r, t)) d maxlg2 → (∀[t1] (t t1 < tra2(r, d, t) → f aehrt aus2(r, t1)) → dist xy(x, pos2(r, tra2(r, d, t))) = d) ∧ ∀[t3] (t t3 < tra2(r, d, t) → dist xy(x, pos2(r, t3)) < d))
u25. Wenn Arm 2 nur lange genug einfährt, kann er jede Länge zwischen der jetzigen und minlg erreichen ∀[c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3, x, t] ( roboter(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), x) → (f aehrt aus1(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), t) ↔ val(c1, t) = 1) ∧ (f aehrt ein1(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), t) ↔ val(c2, t) = 1) ∧ (f aehrt aus2(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), t) ↔ val(c3, t) = 1) ∧ (f aehrt ein2(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), t) ↔ val(c4, t) = 1) ∧ (greif t1(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), t) ↔ val(c5, t) = 1) ∧ (greif t2(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), t) ↔ val(c6, t) = 1) ∧ (dreht vor(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), t) ↔ val(c7, t) = 1) ∧ (dreht zurueck(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), t) ↔ val(c8, t) = 1) ∧ (dist xy(x, pos1(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), t)) = val(s1, t)) ∧ (dist xy(x, pos2(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), t)) = val(s2, t)) ∧ (winkel xy(x, pos1(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), t)) = val(s3, t))) Hubdrehtisch u32. Die Höhe einer auf dem Hubdrehtisch liegenden Schiene bleibt unverändert, solange er weder hebt noch senkt

∀[r, x, t, d] ( roboter(r, x) ∧ minlg2 d dist xy(x, pos2(r, t)) → (∀[t1] (t t1 < tre2(r, d, t) → f aehrt ein2(r, t1)) → dist xy(x, pos2(r, tre2(r, d, t))) = d) ∧ ∀[t3] (t t3 < tre2(r, d, t) → d < dist xy(x, pos2(r, t3))))
∀[h, t, x, s, t2] ( hubdrehtisch(h, x) ∧ proj xy(ort(s, t)) = proj xy(x) ∧ t t2 ∧ ∀[m, t1] (t t1 t2 ∧ bewegt(m, s, t1) → m = h) ∧ ∀[t1] (t t1 t2 → ¬hebt(h, t1) ∧ ¬senkt(h, t1)) → proj z(ort(s, t)) = proj z(ort(s, t2)))
u33. Der Winkel einer auf dem Hubdrehtisch liegenden Schiene bleibt unverändert, solange er sich nicht dreht

∀[h, t, x, s, t2] ( hubdrehtisch(h, x) ∧ proj xy(ort(s, t)) = proj xy(x) ∧ t t2 ∧ ∀[m, t1] (t t1 t2 ∧ bewegt(m, s, t1) → m = h) ∧ ∀[t1] (t t1 t2 → ¬dreht vor(h, t1) ∧ ¬dreht zurueck(h, t)) → winkel(s, t) = winkel(s, t2))
u34. Der Hubdrehtisch dreht eine auf ihm liegende Schiene entsprechend mit

∀[h, t, x, s, t2] ( hubdrehtisch(h, x) ∧ proj xy(ort(s, t)) = proj xy(x) ∧ t t2 ∧ ∀[m, t1] (t t1 t2 ∧ bewegt(m, s, t1) → m = h) → winkel(s, t2) -winkel(s, t) = winkel(h, t2) -winkel(h, t))
u35. Wenn sich der Hubdrehtisch nur lange genug vordreht, kann er jeden Winkel zwischen dem jetzigen und 360

• erreichen ∀[h, x, t, α] ∃[t2] ( hubdrehtisch(h, x) ∧ winkel(h, t) α 360 → (∀[t1] (t t1 < t2 → dreht vor(h, t1)) → winkel(h, t2) = α) ∧ ∀[t3] (t t3 < t2 → ¬winkel(h, t3) = α))
u36. Wenn sich der Hubdrehtisch nur lange genug zurückdreht, kann er jeden Winkel zwischen dem jetzigen und 0

• erreichen ∀[h, x, t, α] ∃[t2] ( hubdrehtisch(h, x) ∧ 0 α winkel(h, t) → (∀[t1] (t t1 < t2 → dreht zurueck(h, t1)) → winkel(h, t2) = α) ∧ ∀[t3] (t t3 < t2 → ¬winkel(h, t3) = α))
u37. Wenn sich der Hubdrehtisch nur lange genug hebt, erreicht er schließlich die obere Position

∀[t] ∃[t2] ∀[h, x] ( hubdrehtisch(h, x) → (∀[t1] (t t1 t2 → hebt(h, t1)) → hoehe(proj xy(x), t2) = zh oben) ∧ ∀[t3] (t t3 < t2 → ¬hoehe(proj xy(x), t3) = zh oben))
u38. Wenn sich der Hubdrehtisch nur lange genug senkt, erreicht er schließlich die untere Position ∀[c1, c2, c3, c4, s1, s2, s3, t, x] ( hubdrehtisch(h(c1, c2, c3, c4, s1, s2, s3), x) → (hebt(h(c1, c2, c3, c4, s1, s2, s3), t) ↔ val(c1, t) = 1) ∧ (senkt(h(c1, c2, c3, c4, s1, s2, s3), t) ↔ val(c2, t) = 1) ∧ (dreht vor(h(c1, c2, c3, c4, s1, s2, s3), t) ↔ val(c3, t) = 1) ∧ (dreht zurueck(h(c1, c2, c3, c4, s1, s2, s3), t) ↔ val(c4, t) = 1) ∧ (hoehe(proj xy(x), t) = zh unten ↔ val(s1, t) = 1) ∧ (hoehe(proj xy(x), t) = zh oben ↔ val(s2, t) = 1) ∧ (winkel(h(c1, c2, c3, c4, s1, s2, s3), t) = val(s3, t))) ∀[c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, x] ( f abrik(f a(c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11), x) ↔ f oerderband(f (c1, s1), x + d1, x + d2) ∧ hubdrehtisch(h(c2, c3, c4, c5, s2, s3, s4), x + d3) ∧ roboter(r(c6, c7, c8, c9, c10, c11, c12, c13, s5, s6, s7), x + d4) ∧ presse(p(c14, c15, s8, s9, s10), x + d5) ∧ f oerderband(f (c16, s11), x + d6, x + d7) ∧ ∀[s, t] ∃[t2] (ort(s, t) = x + d1 ∧ bearbeitungszustand(s, t) = unbearbeitet → ort(s, t2) = x + d7 ∧ bearbeitungszustand(s, t2) = bearbeitet)) ∀[c17, c18, c19, c20, c21, s12, s13, s14, x] ( verbraucher(v(c17, c18, c19, c20, c21, s12, s13, s14), x) ↔ handhabungsgeraet(ha(c17, c18, c19, c20, c21, s12, s13, s14), x + d8, x + d9) ∧ ∀[s, t] ∃[t2] (ort(s, t) = x + d9 ∧ bearbeitungszustand(s, t) = bearbeitet → ort(s, t2) = x + d8 ∧ bearbeitungszustand(s, t2) = unbearbeitet)) ∀[t, r] (t0 t trv1(r, 270, t0) → ¬val(cf a1, t) = 1 ∧ ¬val(cf e1, t) = 1 ∧ ¬val(cdrv, t) = 1 ∧ ¬val(cgr1, t) = 1) r11. roboter(r(c1, c2, c3, c4, c5, c6, c7, c8, s1, s2, s3), d4) r20. BEWEISZIEL: proj xy(pos1(r, t)) = proj xy(d5) ∧ ort(s0, t) = pos1(r, t) ∧ winkel(s0, t) = 180 ∧ up(co, t)

Fig. 1 .Fig. 2 .

 12 Fig. 1. Fzi-Spielzeugmodell der Fertigungszelle

Fig. 9 .

 9 Fig. 9. Spezifikation der einfachen Steuerungsschaltung

Fig. 10 .

 10 Fig. 10. Synthesebeweis der Schaltung aus Abb. 11

  Fig. 16. Formale Spezifikation des Moduls für Phase 1

Fig. 18 .

 18 Fig. 18. Prolog-Notation für Relationen und Junktoren

Fig. 22 .

 22 Fig. 22. Hintergrundtheorie zu unt und ldt

Fig. 23 .Fig. 24 .

 2324 Fig. 23. Synthesebeweis der Schaltung aus Abb. 11 unter Verwendung höherer logischer Operatoren

  u22 in Anhang B. Eine zweite Gruppe von Anforderungen betrifft die Kompatibilität von Abmessungen und Winkeln, etwa, daß die obere Position des Hubdrehtisches, der erste Roboterarm und die mittlere Position der Presse alle in derselben Höhe liegen müssen, vgl. Axiome u15 und u46. Einige weitere Bedingungen sind nicht unbedingt notwendig, führen aber zu einer vereinfachten Steuerungsschaltung Wenn z.B. bekannt ist, daß der Abstand vom. Drehzentrum des Roboters zum Hubdrehtisch größer ist als zur Presse, so genügt es, den ersten Arm auf dem Weg zur Presse einzufahren, während sonst die Schaltung zusätzlich die Möglichkeit des Ausfahrens vorsehen müßte; vgl. auch Axiom r6 in Anhang B. Wenn die Fertigungszelle offen, d.h. ohne das Handhabungsgerät, betrieben wird, fallen weitere Anforderungen über das Be-und Entladeverhalten an. Zum Beispiel darf das Zuführband nur beladen werden, wenn an seinem Anfang genügend Platz dafür frei ist. Diese Bedingung macht einen zusätzlichen Sensor notwendig, entweder am Anfang des Zuführbandes oder -was zu einer einfacheren und robusteren Steuerung führt -an dessen Ende.

u3.

  Wenn sich die Presse aus der unteren Position nur lange genug hebt, erreicht sie schließlich die mittlere Position∀[t] ∃[t2] ∀[p, x] ( presse(p, x) ∧ hoehe(proj xy(x), t) = zp unten → (∀[t1] (t t1 t2 → hebt(p, t1)) → hoehe(proj xy(x), t2) = zp mitte) ∧ ∀[t3] (t t3 < t2 → ¬hoehe(proj xy(x), t3) = zp mitte))u4. Wenn sich die Presse nur lange genug senkt, erreicht sie schließlich die untere Position∀[t] ∃[t2] ∀[p, x] ( presse(p, x) → (∀[t1] (t t1 t2 → senkt(p, t1)) → hoehe(proj xy(x), t2) = zp unten) ∧ ∀[t3] (t t3 < t2 → ¬hoehe(proj xy(x), t3) = zp unten)) u5. ∀[p, x,s, t] ( presse(p, x) → (proj xy(ort(s, t)) = proj xy(x) ∧ (hebt(p, t) ∨ senkt(p, t)) ↔ bewegt(p, s, t)))

  t2) ∧ hoehe(proj xy(x1), t2) = proj z(x1) → ort(s, t2) = x1) u15. Die Roboter-Arme haben feste Höhe ∀[r, x, t] ( roboter(r, x) → proj z(pos1(r, t)) = zp mitte ∧ proj z(pos2(r, t)) = zp unten) u16. Wenn sich der Roboter nur lange genug vordreht, kann er für Arm 1 jeden Winkel zwischen dem jetzigen und 270 • erreichen ∀[r, x, α, t] ( roboter(r, x) ∧ winkel xy(x, pos1(r, t)) α 270 → (∀[t1] (t t1 < trv1(r, α, t) → dreht vor(r, t1)) → winkel xy(x, pos1(r, trv1(r, α, t))) = α) ∧ ∀[t3] (t t3 < trv1(r, α, t) → winkel xy(x, pos1(r, t3)) < α)) u17. Wenn sich der Roboter nur lange genug zurückdreht, kann er für Arm 1 jeden Winkel zwischen dem jetzigen und 90 • erreichen ∀[r, x, α, t] ( roboter(r, x) ∧ 90 α winkel xy(x, pos1(r, t)) → (∀[t1] (t t1 < trz1(r, α, t) → dreht zurueck(r, t1)) → winkel xy(x, pos1(r, trz1(r, α, t))) = α) ∧ ∀[t3] (t t3 < trz1(r, α, t) → α < winkel xy(x, pos1(r, t3)))) u18. Wenn sich der Roboter nur lange genug vordreht, kann er für Arm 2 jeden Winkel zwischen dem jetzigen und 360 • erreichen ∀[r, x, α, t] ( roboter(r, x) ∧ winkel xy(x, pos2(r, t)) α 360 → (∀[t1] (t t1 < trv2(r, α, t) → dreht vor(r, t1)) → winkel xy(x, pos2(r, trv2(r, α, t))) = α) ∧ ∀[t3] (t t3 < trv2(r, α, t) → winkel xy(x, pos2(r, t3)) < α)) u19. Wenn sich der Roboter nur lange genug zurückdreht, kann er für Arm 2 jeden Winkel zwischen dem jetzigen und 180 • erreichen ∀[r, x, α, t] ( roboter(r, x) ∧ 180 α winkel xy(x, pos2(r, t)) → (∀[t1] (t t1 < trz2(r, α, t) → dreht zurueck(r, t1)) → winkel xy(x, pos2(r, trz2(r, α, t))) = α) ∧ ∀[t3] (t t3 < trz2(r, α, t) → α < winkel xy(x, pos2(r, t3)))) u20. Wenn Arm 1 nur lange genug ausfährt, kann er jede Länge zwischen der jetzigen und maxlg erreichen ∀[r, x, t, d] ( roboter(r, x) ∧ dist xy(x, pos1(r, t)) d maxlg1 → (∀[t1] (t t1 < tra1(r, d, t) → f aehrt aus1(r, t1)) → dist xy(x, pos1(r, tra1(r, d, t))) = d) ∧ ∀[t3] (t t3 < tra1(r, d, t) → dist xy(x, pos1(r, t3)) < d))

u26.

  Die Winkel der Arme bleiben unverändert, wenn sich der Roboter nicht dreht ∀[r, x, t, t2] ( roboter(r, x) ∧ ∀[t1] (t t1 t2 → ¬dreht vor(r, t1) ∧ ¬dreht zurueck(r, t1)) → winkel xy(x, pos1(r, t)) = winkel xy(x, pos1(r, t2)) ∧ winkel xy(x, pos2(r, t)) = winkel xy(x, pos2(r, t2))) u27. Die Länge von Arm 1 bleibt unverändert, wenn ihn der Roboter weder ein-noch ausfährt ∀[r, x, t, t2] ( roboter(r, x) ∧ ∀[t1] (t t1 t2 → ¬f aehrt aus1(r, t1) ∧ ¬f aehrt ein1(r, t1)) → dist xy(x, pos1(r, t)) = dist xy(x, pos1(r, t2))) u28. Die Länge von Arm 2 bleibt unverändert, wenn ihn der Roboter weder ein-noch ausfährt

∀

  [t] ∃[t2] ∀[h, x] ( hubdrehtisch(h, x) → (∀[t1] (t t1 t2 → senkt(h, t1)) → hoehe(proj xy(x), t2) = zh unten) ∧ ∀[t3] (t t3 < t2 → ¬hoehe(proj xy(x), t3) = zh unten))u39. Motorsteuerung und Sensoren c 1 : +1 hebt, 0 steht c 2 : +1 senkt, 0 steht c 3 : +1 dreht vor, 0 steht c 4 : +1 dreht zurück, 0 steht s 1 : +1 unten s 2 : +1 oben s 3 : Winkel

Förderband u40 .

 u40 Wenn das Förderband nur lange genug läuft, transportiert es eine auf ihm liegende Schiene vom Anfang zum Ende∀[f, s, t, x1, x2] ∃[t2] ( f oerderband(f, x1, x2) ∧ ort(s, t) = x1 → (∀[t1] (t t1 < t2 → laeuf t(f, t1)) → ort(s, t2) = x2) ∧ ∀[t3] (t t3 < t2 → ¬ort(s, t3) = x2)) u41. Motorsteuerung und Sensoren c 1 : 0 steht, +1 läuft s 1 : +1 Ende ∀[c1, s1, x1, x2, t] ( f oerderband(f (c1, s1), x1, x2) → (laeuf t(f (c1, s1), t) ↔ val(c1, t) = 1) ∧ ((∃[s] ort(s, t) = x2) ↔ val(s1, t) = 1))

u44.

  Nur die Presse bearbeitet Schienen, ∀[s, t, t2] ( bearbeitungszustand(s, t) = unbearbeitet ∧ bearbeitungszustand(s, t2) = bearbeitet → ∃[t1, p, x] (t t1 t2 ∧ presse(p, x) ∧ bewegt(p, s, t))) u45. Nur das Handhabungsgerät "verbraucht" Schienen ∀[s, t, t2] ( bearbeitungszustand(s, t) = bearbeitet ∧ bearbeitungszustand(s, t2) = unbearbeitet → ∃[t1, h, x1, x2] (t t1 t2 ∧ handhabungsgeraet(h, x1, x2) ∧ bewegt(h, s, t))) u46. Hubdrehtisch in oberer Position und Presse in unterer Position haben die gleiche Höhe zh oben = zp mitte u47. Roboter und Presse stehen im richtigen Winkel zueinander winkel xy(d4, d5) = 270 u47a. Roboterarm 1 kann schneller eingezogen werden als vom Hubdrehtisch zur Presse vorgedreht werden ∀[r, t] ( roboter(r, d4) ∧ pos1(r, t) = d3 → tre1(r, dist xy(d4, d5), t) < trv1(r, winkel xy(d4, d5), t))u47b. Roboter und Hubdrehtisch stehen nahe genug beieinanderdist xy(d4, d3) maxlg1 Physik u48. Schwerkraftgesetz ∀[s, t] ( proj z(ort(s, t)) = hoehe(proj xy(ort(s, t)), t)) u49. Zwei Dinge sind nicht gleichzeitig am selben Ort ∀[s1, s2, t] ( ort(s1, t) = ort(s2, t) → s1 = s2) u50. Kein Ding bewegt sich von selbst ∀[s, t, t2] ( t t2 ∧ (¬ort(s, t) = ort(s, t2) ∨ ¬winkel(s, t) = winkel(s, t2)) → ∃[m, t1] bewegt(m, s, t1)) Mathematik u51. Dreidimensionaler Raum ∀[x, x1] ( proj xy(x) = proj xy(x1) ∧ proj z(x) = proj z(x1) → x = x1) u62. Gleichheit∀[aa] (aa = aa) u66. Lineare Ordnungsrelation ∀[aa, bb] (¬bb aa ↔ aa < bb) u66b. ∀[aa, bb] (aa < bb → aa bb) u66c. ∀[aa, bb, cc] (aa < bb < cc → aa < cc) u66d. ∀[aa, bb, cc] (aa bb < cc → aa < cc) u66f. ∀[aa, bb, cc] (aa < bb cc → aa < cc) u66e. ∀[aa, bb, cc] (aa bb cc → aa cc) u61. Archimedischer Körper ∀[aa, bb] (aa * (-1) < bb * (-1) ↔ bb < aa) u67. Polarkoordinaten ∀[x, x1, x2] ( winkel xy(x2, x) = winkel xy(x2, x1) ∧ dist xy(x2, x) = dist xy(x2, x1) → proj xy(x) = proj xy(x1)) u69. Arithmetik 270 -90 = 180 u69a. Aussagenlogik aaa ∧ bbb → aaa u69c. aaa ∧ bbb → bbb u69d. aaa → (¬aaa → bbb) Steuerung u70. Steigende Flanke∀[c, t] ( up(c, t) ↔ val(c, t) = 1 ∧ ∃[t1] (t1 < t ∧ ∀[t2] (t1 < t2 < t → ¬val(c, t2) = 1))) u71. Flanken-getriggertes Flip-Flop ca ___------------___ cb ___________--_____ out ___--------_______ ∀[ca, cb, t2] ( val(df f (ca, cb), t2) = 1 ↔ ∃[t] (t t2 ∧ up(ca, t) ∧ ∀[t1] (t t1 < t2 → ¬up(cb, t1)))) , d, t] val(mf f (c, d), t + d) = val(c, d) --___---___ ∀[c, v, t] ( val(trigger(c, v), t) = 1 ↔ val(c, t) < v) u74. Inverter c ___---___--out ---___---___ ∀[c, t] ( val(neg(c), t) = 1 ↔ ¬val(c, t) = 1) u75. Oder-Gatter ca ______-----cb ___---___--out ___---------∀[ca, cb, t] ( val(or(ca, cb), t) = 1 ↔ val(ca, t) = 1 ∨ val(cb, t) = 1) u76. Und-Gatter ca ______-----cb ___---___--out _________---∀[ca, cb, t] ( val(and(ca, cb), t) = 1 ↔ val(ca, t) = 1 ∧ val(cb, t) = 1) u77. Verstärker ∀[c, v, t] (val(ampl(c, v), t) = val(c, t) * v)Modul 1 der Robotersteuerung r1. up(ci, t0) r2. ort(s0, t0) = d3 r3. pos1(r, t0) = d3 r4. winkel(s0, t0) = winkel xy(d4, d3) -90 r6. dist xy(d4, d5) dist xy(d4, pos1(r, t0)) r7. minlg1 dist xy(d4, d5) r8. winkel xy(d4, d5) 270 r9. winkel xy(d4, pos1(r, t0)) winkel xy(d4, d5) r10.

  

  Abschnitt 6 geht auf die Verwendung höherer logischer Operatoren ein. In Abschnitt 7 erfolgt eine Bewertung der Fallstudie nach verschiedenen Gesichtspunkten. Die Fallstudie "Fertigungszelle" 1 ist eine Fallstudie aus dem Bereich Regeln und Steuern. Aufgabe ist die Entwicklung von verifizierter Steuerungs-Software für ein Modell einer Anlage, wie sie bei einer metallverarbeitenden Firma in Karlsruhe steht. Am Forschungszetrum Informatik (Fzi) in Karlsruhe wurde ein Spielzeugmodell der Fertigungszelle mit Fischer-Technik realisiert, das über eine RS232-Schnittstelle angesteuert werden kann (Abb. 1). Die Fertigungszelle (vgl. Abb. 2) bearbeitet Metallrohlinge, die auf einem Zuführförderband (zfb) an eine Presse (prs) gelangen. Ein Roboter (rob) nimmt die Metallrohlinge vom Zuführförderband und legt sie in die Presse. Der Roboterarm verläßt die Presse, die Presse verarbeitet die Metallrohlinge und öffnet sich wieder. Der Roboter nimmt das verarbeitete Metallplättchen aus der Presse und legt es auf ein Ablageförderband (afb).

	2 Die Fallstudie "Fertigungszelle"

Aufgabenbeschreibung der Fertigungszelle in Abschnitt 2 und einem kurzen Überblick über die Methode der deduktiven Programmsynthese und das Unterstützungswerkzeug Sysyfos in Abschnitt 3 werden das Vorgehen und die Erfahrungen beim Entwurf der Steuerungsschaltung in Abschnitt 4 diskutiert. In Abschnitt 5 wird das Vorgehen anhand der Entwicklung der Robotersteuerung konkretisiert, ein typischer Teil des maschinengeführten formalen Beweises ist in Anhang C wiedergegeben.

  Abbildung 3 zeigt ein Zeitdiagramm für einen Durchlauf dreier Metallplättchen durch die Fertigungszelle, das Handhabungsgerät ist dabei weggelassen.

	Metall 1 Metall 2 Metall 3
	zfb
	hub
	rob
	prs
	afb

  Zeitdiagramm für den Durchlauf dreier Metallplättchen . Sämtliche Elektromotoren werden sofort gestoppt, wenn ein dadurch bewegtes Gerät an den Rand seiner Beweglichkeit gerät. Zum Beispiel wird das Handhabungsgerät in seiner horizontalen Bewegung gestoppt, sobald einer der beiden Schalter signalisiert, daß es über einem Band steht. 5. Der Hubdrehtisch wird nicht unter das Niveau des Förderbandes bewegt. Er wird in unteren Stellungen nicht gedreht. 6. Das Handhabungsgerät stößt nicht seitlich gegen ein Förderband. Dies geschieht zum Beispiel, wenn das Handhabungsgerät auf dem Niveau, auf dem es vom Ablageförderband aufnimmt, ohne vertikale Bewegung hin zum Zuführförderband fährt. Außerdem stößt das Handhabungsgerät nicht von oben gegen Zuführ-oder Ablageförderband. 7. Ein Elektromagnet wird nur deaktiviert, wenn der zugehörige Roboterarm bzw. Greifer in einer Position ist, in der gefahrlos abgeladen werden kann. Gefahrlos abgeladen werden kann über Förderbändern, in der Presse und über dem Hubdrehtisch, vorausgesetzt der Abstand zwischen Magnet und Ablagefläche ist genügend klein. 8. Das Ablageförderband transportiert höchstens dann, wenn sich kein Fertigteil im Aufnahmebereich des Handhabungsgeräts befindet. 9. Damit ein Metallteil vom Zuführförderband auf den Hubdrehtisch übergeht, muß der Tisch in entsprechender Position sein. 10. (Das Zuführförderband darf nur dann Metallplättchen transportieren, wenn der Hubdrehtisch leer ist.)

	2.1 Aktoren	Benutzerschnittstelle		
		Pretty Printing		
	Die Steuerung hat folgende Aktionsmöglichkeiten:		
	-Bewegung des unteren Teils der Presse (Elektromotor) E E rs		
	-Ein-und Ausfahren des Roboterarmes 1 (Elektromotor) E E rp		
	-Ein-und Ausfahren des Roboterarmes 2 (Elektromotor) E E rm/2		
	-Aufnehmen eines Metallteils durch Arm 1 (Elektromagnet) E E rm/1		
	-Aufnehmen eines Metallteils durch Arm 2 (Elektromagnet) E E un simp		
	-Drehung des Roboters (Elektromotor) E sp	E		
	-Drehung des Hubdrehtisches (Elektromotor) E tf	E		
	-Höhenverstellung des Hubdrehtisches (Elektromotor) -Vertikale Bewegung des Greifers des Handhabungsgerätes (Elektromotor) E T hy -Horizontale Bewegung des Greifers des Handhabungsgerätes (Elektromotor) E E T co	
	-Aufnehmen eines Metallplättchens durch den Greifer des Handhabungsgerätes (Elektromagnet) T
	Specs	Types	Tfms			©
	Nr • Assertions • Goals • Output • Orig	c	⇐⇒	Datei	©
	3 Deduktive Programmsynthese				
	Die seinerzeit von Robinson eingeführte Resolutionsmethode [Rob65] setzt voraus, daß die zu re-
	solvierenden Formeln in konjunktive Normalform und weiter in Klauselnormalform überführt wor-
	den sind. Demgegenüber geben Manna und Waldinger in [MW80] eine Form der Resolution an,
	die auf beliebigen Formeln arbeitet (Nicht-Klausel-Resolution). Dadurch wird die Lesbarkeit von
	Zwischenergebnissen im Beweis stark erhöht, was für ein interaktives System eine unbedingte
	Notwendigkeit ist. Die Lesbarkeit wird ebenfalls durch die Schreibweise in zwei Spalten (Assertions,
	Goals) gesteigert, wobei logisch gesehen die Formeln in der Goal-Spalte implizit negiert sind. Das
	Sysyfos-System arbeitet nicht mit der in [MW80] verwendeten Resolutionsregel, sondern mit der
	etwas leistungsfähigeren Regel von Schmerl [Sch88], die in [Haa92] entsprechend angepaßt wurde.
	Abbildung 5 zeigt in den Schritten 1 bis 3 und in den Schritten 4 bis 7 ein konkretes Beispiel der
	Nicht-Klausel-Resolution. Der dabei wie auch im folgenden verwendete Begriff der Polarität einer
	Teilformel p innerhalb einer Formel F [p] gibt an, ob p unter einer geraden (Polarität "+") oder
	ungeraden ("-") Anzahl von Negationen vorkommt. Die Multiplikation zweier Polaritäten sowie
	2.3 Sicherheitsanforderungen -Nicht-Klausel-Resolution (rs), einer Polarität mit einer Teilformel ist entsprechend definiert, vgl. [St60].	
	-Paramodulation bzw. allgemeiner: Relation Replacement (rp),			
	-E-Resolution bzw. allgemeiner: Relation Matching (rm/2 ), Die Steuerung soll verschiedenen Sicherheitsanforderungen genügen. Diese Sicherheitsanforderungen -Monotonie-Regel (rm/1 ), dienen unterschiedlichen Zwecken: zum einen gewährleisten sie, daß die Anlage sich nicht selbst zerstört (z.B. die Presse einen in ihr befindlichen Roboterarm), zum anderen schützen sie im Bereich -Unifikation zweier Teilformeln bzw. explizite Faktorisierung (un),
	der Anlage tätige Arbeiter.				

-Ein-und Ausschalten des Zuführförderbandes (Elektromotor) -Ein-und Ausschalten des Ablageförderbandes (Elektromotor) 2.2 Sensoren Die Steuerung erhält Informationen über folgende Sensoren: -Ist die Presse in unterer Position? (Schalter) -Ist die Presse in mittlerer Position? (Schalter) -Ist die Presse in oberer Position? (Schalter) -Wie weit ist Arm 1 ausgefahren? (Potentiometer) -Wie weit ist Arm 2 aufgefahren? (Potentiometer) -Wie weit ist der Roboter gedreht? (Potentiometer) -Ist der Hubdrehtisch in unterer Position? (Schalter) -Ist der Hubdrehtisch in oberer Position? (Schalter) -Wie weit ist der Hubdrehtisch gedreht? (Potentiometer) -Befindet sich das Handhabungsgerät über dem Zuführförderband? (Lichtschranke) -Befindet sich das Handhabungsgerät über dem Ablageförderband? (Lichtschranke) -In welcher vertikalen Position befindet sich der Greifer? (Potentiometer) -Befindet sich ein Metallteil am äußersten Ende des Ablageförderbandes? (Lichtschranke) Während Lichtschranken und Schalter ja/nein-Informationen liefern, besteht die Information eines Potentiometers aus einer Spannung, die im Beispiel der Drehung proportional zum Winkel ist. 1. Die Presse wird nur geschlossen, wenn sich keiner der Roboterarme in ihr befindet. 2. Ein Roboterarm wird nur vor die Presse gedreht, wenn der Arm eingefahren ist oder die Presse in oberer oder unterer Stellung ist. 3. Der Roboter wird nicht weiter als nötig nach links und rechts gedreht, da er sonst möglicherweise andere Teile der Anlage (z.B. den Hubdrehtisch) beschädigen könnte. 4In diesem Abschnitt wird die zur Entwicklung der Fertigungszelle verwendete formale Methode der deduktiven Programmsynthese nach Manna und Waldinger [MW80] kurz vorgestellt. Ihre grundlegende Vorgehensweise besteht darin, die Erfüllbarkeit einer gegebenen prädikatenlogischen Spezifikation konstruktiv zu beweisen. Dabei entsteht aus den auftretenden Antwort-Substitutionen gleichzeitig das zu synthetisierende funktionale Programm, das die Spezifikation erfüllt. Die Beweisregeln umfassen Resolution auch für Formeln, die nicht in Klausel-Normalform vorliegen, sowie die in [MW86] beschriebenen Verallgemeinerungen von E-Resolution und Paramodulation. Es gibt eine ∨-Split-Regel für Goals und eine ∧-Split-Regel für Assertions, aber nicht umgekehrt. Rekursive Programme lassen sich mit Hilfe struktureller Induktion erzeugen, wobei die Terminierungsordnung vom Benutzer angegeben werden muß. Es kann gezeigt werden, daß dieses Ableitungssystem für Logik erster Stufe vollständig ist. Das nach diesem Ansatz prototypisch in Prolog implementierte Sysyfos-System (siehe Abb. 4) arbeitet auf einer Datenbasis aus Formeln (Assertions, Goals), denen teilweise ein Term als Antwortsubstitution (Output) zugeordnet ist. Jede Formel ist eindeutig numeriert (Nr ). Unter Orig wird die Beweisoperation abgespeichert, aus der die Formel entstanden ist. Folgende Operationen sind auf dieser Datenbasis definiert: -Aufspalten in Teilformeln (sp), -Logische Transformationen (tf ), -Konkretisierung von Skolem-Konstanten entsprechend ihres Typs (co), -Generierung einer Induktionshypothese aus einer Spezifikation (hy). Das Ergebnis einer Operation wird von einem Formelvereinfacher (simp) auf eine möglichst einfache Form gebracht, bevor es in die Datenbasis abgespeichert wird. Im Folgenden werden die für die Fallstudie benötigten Operationen und Komponenten kurz erläutert.

Datenbasis

Fig. 4. Struktur des Sysyfos-Systems 3.1 Nicht-Klausel-Resolution

  In der vorliegenden Fallstudie haben wir versucht, einen Ansatz zu verfolgen, der dieses Problem so weit als möglich entschärft. Wir haben eine formale Sprachebene geschaffen, in der die informelle Beschreibung aus Abschnitt 2 quasi 1:1 ausgedrückt und dadurch leicht validiert werden kann. Die so erhaltene Spezifikation ist eine Anforderungs-Spezifikation, keine Entwurfsspezifikation. Durch ihren hohen Grad an Implizitheit gestattet sie weder ein "rapid prototyping" noch die unmittelbare schrittweise Verfeinerung in ausführbaren Code.Für den Korrektheitsbeweis der obigen Steuerschleife benötigen wir jedoch die Existenz eine frühesten Zeitpunkts, an dem die gewünschte Länge erreicht wird, um den Ausfahrmotor genau zu diesem Zeitpunkt anzuhalten. Es genügt daher nicht, die Zeit durch rationale Zahlen zu modellieren, da diese nicht abgeschlossen gegen Infima sind. Wenn z.B. die gewünschte Länge zufällig so gewählt ist, daß sie erreicht wird, wenn (t 2 -t 1 ) 2 = 2 ist, dann ist sie zu jedem Zeitpunkt t 2 > t 1 + √ 2 erreicht und überschritten, aber es gibt kein minimales (rationales) t 2 . Dieses Problem wurde umgangen, indem in den Spezifikationsaxiomen zusätzlich die Existenz frühester Zeitpunkte gefordert wurde, vgl. z.B. Axiom u16 in Anhang B.

	4 Entwurf	3.3 E-Resolution Sysyfos-System ändern kann (z.B. durch Umordnung der Axiome), bleibt ersterer stets gleich, was
		für das Beweis-Nachspielen unumgänglich ist. Weiterhin wurden neue, abgeleitete Beweisoperatio-
	Ebenfalls in [MW86] wird eine entsprechende Verallgemeinerung der E-Resolution auf Nicht-Klausel-Form und beliebige Relationen definiert und "Relation Replacement" genannt (rm/2 in nen definiert, die weniger empfindlich gegen Änderungen der Ausgangsformeln sind. So wurde z.B. die in [MW80] vorgesehene explizite Instanziierung einer Formel ersetzt durch die Unifikation zweier 4.1 Anforderungsspezifikation
	Abb. 4). Das Sysyfos-System arbeitet hier mit einer für E-Resolution modifizierten Version der Schmerl-Regel (Schritte 15 bis 17 in Abb. 5, vgl. [Bur89]). Daneben ist noch eine Operation zur Teilformeln, da letztere unempfindlich gegen gebundene Umbenennung ist, wie sie häufig durch die Es ist bekannt, daß der Übergang von einer informellen Anforderungsbeschreibung zu einer formalen Software automatisch erzeugten Variablennamen vorkommt. Spezifikation der bzgl. der Korrektheit problematischste Schritt innerhalb des formalen Vorgehens-Steuerung Anwendung der Monotonie-Regel definiert, ebenfalls für beliebige transitive Relationen (Schritte 22 bis 23 in Abb. 5). 3.4 Vereinfacher modells ist, da die formale Spezifikation naturgemäß nicht gegen die informelle Beschreibung veri-Motor Sensor c Hardware T fiziert werden kann. Roboterarm c T Mechanik
		Nach jedem Beweisschritt im System wird das Ergebnis durch einen Vereinfacher geschickt, wobei
		nicht nur die Idempotenz-, sondern auch die Absorptionsgesetze angewendet werden, um mehrfach Fig. 7. Steuerschleife mit mechanischer Rückkoppelung
	vorkommende Teilformeln zu vermeiden (Faktorisierung, vgl. [Sch88]). Zusätzlich kann der Benutzer Länge des Roboterarms 1:
	durch eine entsprechende Option die Überführung in eine linksassoziative Negationsnormalform ve-(Presse in oberer Position)
		ranlassen, was sich während der Fallstudie als positiv für die Lesbarkeit herausgestellt hat.
		In [Moh91] wurde als Anwendungsfallstudie mit Hilfe des Sysyfos-Systems ein Algorithmus zum
		Finden der gemeinsamen Teilterme eines Terms synthetisiert, der künftig als verifizierte Komponente
		innerhalb des Formelvereinfachers (Faktorisierung) des Systems selbst eingesetzt werden soll.
		3.5 Benutzeroberfläche
		ps1(R, t)) -90 = 180 rp(11,12)
		ha1(R, s0, t) ∧ wxy(x, ps1(R, t)) -90 = 180 Während der Bearbeitung der Fallstudie Fertigungszelle wurde parallel das Sysyfos-System weit-simp(13)
	E-Resolution: erentwickelt und u.a. um eine halbgraphische Benutzeroberfläche zur Darstellung von Formel-und
		F [P (s + ) m ] Beweisbäumen und Auswahl von Teilbäumen für Beweisoperationen ergänzt, die weitgehend un-
	G[P (t) -m ] abhängig vom unterliegenden Fenstersystem und vom eigentlichen Beweissystem verwendbar ist.
		F [¬m•G[(-m)•(t s)]] Sie erlaubt neben einer flexiblen Layout-Festlegung für Formelbäume die wahlweise Aus-und Ein-rm(15,16)
	Beispiel: blendung der Argumente von Skolemfunktionen, die Navigation innerhalb eines Formelbaums und
		rob ∧ win(s0, T ) = w0 die gezielte Suche in einer Menge von Formeln (z.B. Spezifikationsaxiomen).
	(T0 t t1 → drv(t)) → wxy(t1) = A Abbildung 6 zeigt als Beispiel die Sysyfos-Benutzeroberfläche während des ersten Resolutionss-rob ∧ ¬((T0 t t1 → drv(t)) → ¬win(s0, T ) = wxy(t1) rm(18,19) rob ∧ (T0 t t1 → drv(t)) ∧ win(s0, T ) = wxy(t1) chritts aus Anhang C. In den Fenstern "show1" und "show2" werden die aktuellen Elternformeln simp(20) in halbgraphischer Notation angezeigt, das Fenster "tab" zeigt eine Tabelle aller bisher abgeleiteten
	Monotonie-Regel: Formeln. Im Hauptfenster ("SYSYFOS") wurde der Resolutionsbefehl eingegeben, nachdem in den f (s + , t -) f (u + , v -) Fenstern "show1" und "show2" die zu resolvierenden Teilformeln durch entsprechende Navigation-
		s u ∧ v t skommandos ausgewählt wurden. Die Angaben in der Titelzeile des Fensters "show1" besagen, daß rm(22)
	Beispiel: die angezeigte Formel die Nummer 116 hat, eine Assertion ist, aus der Opration split 112, [2] ent-
		wxy(x1, x2) = wxy(x3, x4) standen ist, und daß in ihr die Teilformel 1.2 ausgewählt wurde (siehe auch die Cursor-Position
		x1 = x3 ∧ x2 = x4 im Fenster). Entsprechendes gilt für das Fenter "show2". Für die Formelsyntax siehe Abb. 18. Die rm(24)
	Dabei sei m bzw. -m die Polarität von p, angedeutet durch p m bzw. p -m . Für Terme s und t bedeute vorkommenden Variablennamen weichen von Anhang C ab, da letztere aus Darstellungsgründen
	G s + , t -, daß G bzgl. im ersten Argument monoton wachsend und im zweiten monoton fallend ist. In systematisch umnumeriert wurden.
	den Beispielen ist die Relation " " die Gleichheit. Großgeschriebene Namen bezeichenen Variablen,
	kleingeschriebene Konstanten. Die rechte Seite gibt an, wie die aktuelle Formel entstanden ist.
		3.6 Beweiswiederholung
		Fig. 5. Verwendete Beweisregeln
		Das Sysyfos-System verfügt über einen Mechanismus zum Nachspielen bereits gefundener Beweis-
		teile, der auch noch nach leichten Änderungen der Spezifkation verwendet werden kann. Beweisteile
		können als Terme abgespeichert werden, wobei jeder Beweisoperation aus Abb. 4 ein Funktion-
		ssymbol entspricht und jedem Axiom sein eindeutiger benutzerdefinierter Name als Konstante. Ab-
		bildung 12 zeigt die Termdarstellung des Beweises aus Abb. 10. Der Name eines Axioms ist von
		seiner Formelnummer zu unterscheiden: während sich letztere zwischen verschiedenen Sitzungen am

Zuerst wurde eine geeignete Terminologie, bestehend aus Prädikaten-und Funktionssymbolen und ihren informellen Bedeutungen, festgelegt (siehe Anhang A). Die Zeit wurde mit Hilfe expliziter Parameter modelliert, um innerhalb der Prädikatenlogik erster Ordnung zu bleiben und um explizite Aussagen über Zeitpunkte machen zu können. Der Raum wurde durch dreidimensionale kartesische Koordinatenvektoren modelliert, wobei Transformationen von und nach Polarkoordinaten soweit als notwendig axiomatisiert wurden. Das gewünschte "Programm" soll aus einer asynchronen Hardware-Schaltung bestehen. Sie wird aus Ttl-artigen Komponenten aufgebaut, die formal durch zeitabhängige Funktionen dargestellt sind, wobei die Schaltzeiten ignoriert werden. Explizite Rückkoppelungen in der Schaltung sind nicht erlaubt, da sie auf der formalen Seite zu unendlichen Termen führen würden, die vom Beweiswerkzeug nicht unterstützt werden. Stattdessen wurden die notwendigen Rückkoppelungen in Bauelementen wie Flip-Flops eingekapselt.

Auf dieser Grundlage konnte in einem nächsten Schritt eine Sammlung offensichtlicher Fakten über das Verhalten der einzelnen Maschinen formalisiert werden, siehe Anhang B. Diese formale Spezifikation besteht aus vier Teilen:

der von jedem einzelnen Maschinentyp verlangten Verhaltensbeschreibung, der Verhaltensbeschreibung der einzelnen Hardware-Bauelemente, den benötigten Hintergrundfakten aus Geometrie, Arithmetik und Physik und der eigentlichen Spezifikation der Aufgabe der Fertigungszelle.

Die Spezifikation ist lokal verstehbar in dem Sinne, daß es zur Validation eines Axioms genügt, nur dieses eine Axiom mit Hilfe der Terminologiedefinitionen gegen seine informelle Beschreibung zu überprüfen.

Die Spezifikation wurde in der naheliegenden Weise modularisiert. Für jeden Maschinentyp existiert ein Modul, das das von ihm verlangte Verhalten formal beschreibt, daneben gibt es drei weitere Spezifikationsmodule, in denen das Verhalten der Hardware-Bauelemente, der Gesamtaufbau der Fertigungszelle sowie die benötigten Hintergrundfakten aus Mathematik und Physik enthalten sind. Man beachte, daß keines dieser Module zu einem Teil der Implementierung korrespondiert in dem Sinne, daß letzterer durch eine Folge von Entwicklungsschritten aus ersterem gewonnen werden könnte. Die Spezifikationsmodule beschreiben verschiedene Aspekte der modellierten Realität, nicht der Implementierung.

Diese Herangehensweise machte auch formal die Sinnlosigkeit einer "Fertigungs"-Zelle deutlich, deren einziger Zweck darin besteht, Metallplättchen in einem Kreis zu bewegen, da es nicht möglich war, eine Spezifikationsformel dafür anzugeben, die nicht auch von einer leeren Zelle ohne alle Maschinen erfüllt worden wäre. Daher versahen wir das Handhabungsgerät mit der zusätzlichen Fähigkeit, Metallplättchen zu konsumieren, d.h. sie in den unbearbeiteten Zustand zurück zu überführen, und stellten zwei separate Spezifikationsformeln auf: eine für den Konsumenten, das Handhabungsgerät, und eine für den Produzenten, den Rest der Fertigungszelle. Letztere besteht in einer formalen Übersetzung der Anforderung: "Wenn ein unbearbeitetes Metallplättchen auf dem Zuführförderband liegt, erscheit es irgendwann später in bearbeitetem Zustand auf dem Ablageförderband."

4.2 Einbeziehung der Mechanik

Die Verwendung von Prädikatenlogik mit expliziter Zeit als Spezifikationssprache erlaubt es, die vorgegebenen technisch-physikalischen Anforderungen mit in die Spezifikation einzubeziehen und dadurch auch Systeme mit Rückkoppelungsschleifen zu behandeln, die teilweise außerhalb des Bereichs der Hardware bzw. Software liegen. Zum Beispiel fährt die Robotersteuerung in einigen Situationen einen der Arme soweit aus, bis er eine bestimmte Länge erreicht, siehe Abb. 7. Es ist unmöglich zu beweisen, daß der Roboterarm tatsächlich die gewünschte Länge erreichen und dann anhalten wird, ohne die mechanischen Eigenschaften des Arms miteinzubeziehen. Das Gleiche gilt für die gesamte Fertigungszelle: um das oberste Spezifikationsziel zu beweisen, daß sie bearbeitete Metallplättchen aus unbearbeiteten produziert, ist die formale Behandlung ihres mechanichen Verhaltens im Beweis notwendig; es genügt nicht, den Beweis auf die reinen Software-bzw. Hardware-Aspekte zu beschränken.

Darüber hinaus ist es möglich, notwendige Bedingungen formal herzuleiten, die die Konfiguration außerhalb des Hardware/Software-Bereichs betreffen. So wurde z.B. gezeigt, daß der vom Anfangspunkt des Ablagebands, dem Drehzentrum des Roboters und der Presse gebildete Winkel notwendig 90 • betragen muß, damit die bearbeiteten Metallplättchen in der richtigen Ausrichtung auf dem Band abgelegt werden. Der deduktive Ansatz konnte somit zu einem methodischen Rahmen für die Entwicklung der gesamten Fertigungszelle, einschließlich mechanischer Aspekte, erweitert werden. Es ist denkbar, daß ein Ingenieur in Zukunft eine formale Anforderungsbeschreibung der gewünschten Fertigungszelle vom Auftraggeber erhält und eine formale Verhaltensbeschreibung der Maschinen von deren Hersteller. Daraus könnte er dann einen verifizierten Gesamtentwurf der Zelle erstellen, einschließlich ihrer Steuerungs-Software und ihres mechanischen Aufbaus. Die deduktive Synthese dient dabei als der Rahmen, innerhalb dessen klassischer mechanischer Entwurf und Software-Entwurf integriert wird.

4.3 Zeitmodellierung

Schließlich soll eine eher überraschende Erfahrung mit der Zeitmodellierung erwähnt werden, die zeigt, wieviel Sorgfalt die Formalisierung des Hintergrundwissens für die Anforderungsspezifikation erfordert. Wir beziehen uns wieder auf die Steuerschleife aus Abb. 7. An einer bestimmten Stelle im Beweis ist es notwendig zu zeigen, daß es einen Zeitpunkt t 2 gibt, an dem der Roboterarm die gewünschte Länge erreicht, sofern seine Länge zu einem gegebenen Zeitpunkt t 1 kleiner war. Aus der formalen Verhaltensbeschreibung des Roboters wissen wir, daß der Arm irgendwann jede vorgegebene Länge (innerhalb seiner Grenzen) erreichen wird, wenn der Ausfahrmotor nur lange genug läuft.

  . Einfache Steuerungsschaltung hier als Beispiel für einen Synthesebeweis die stark vereinfachte fiktive Aufgabe aus Abb. 7 dienen, einen Roboterarm auf eine bestimmte Länge auszufahren. Abbildung 9 faßt die dafür benötigten Spezifikationsaxiome aus Anhang B zusammen, Abb. 10 zeigt den Synthesebeweis, Abb. 11 zeigt die synthetisierte Schaltung selbst.In Abschnitt 5 wird die formale Entwicklung der Robotersteuerung gezeigt. In Abschnitt 6 wird der zweite Ansatz vorgestellt, der aufgrund der gemachten Erfahrungen mit der Modellierung des Anwendungsgebiets neue logische Operatoren definierte und dadurch Spezifikation und Beweis kürzer und übersichtlicher zu gestalten erlaubte.Im folgenden soll das Vorgehen beim Entwurf anhand der Steuerung des Roboters erläutert werden, die wegen der Koordinationsprobleme der beiden Arme die schwierigste von allen vorkommenden Maschinensteuerungen darstellt. Beim Roboter lassen sich vier teilweise ineinander verzahnte Bewegungsphasen unterscheiden: 1. Arm 1 nimmt ein Metallplättchen vom Hubdrehtisch auf und transportiert es in die Presse. 2. Arm 2 nimmt ein bearbeitetes Metallplättchen von der Presse auf und transportiert es auf das Ablageförderband. 3. Arm 1 fährt von der Presse (leer) zurück zum Hubdrehtisch. 4. Arm 2 fährt vom Ablageförderband (leer) zurück zur Presse. Aufgrund der Konstruktion des Roboters können die Phasen 1. und 2. sowie die Phasen 3. und 4. immer nur gleichzeitig ablaufen. Abbildung 13 zeigt die Bewegungsphasen des Roboters schematisch. Man sieht, daß die Voraussetzungen für die Phasen 1. und 2. bzw. 3. und 4. jeweils einzeln oder für gemeinsam erfüllt sein können. Die Steuerung muß sicherstellen, daß Vor-und Rücklaufphasen des Roboters nie gleichzeitig ablaufen. Während des Ablaufs von Phase 4. (Rücklauf von Arm 2 zur Presse) kann der Fall eintreten, daß auf dem Hubdrehtisch ein neues unbearbeitetes Metallplättchen ankommt. In diesem Fall soll Phase 3. zugeschaltet werden, so daß der Roboter seinen Arm 1 zunächst bis zum Hubdrehtisch zurückfährt, dort das Metallplättchen aufnimmt (Phase 1.) und unterwegs Phase 2. zuschaltet, um die Presse durch Arm 2 zu leeren. Der Grobentwurf der Steuerung teilt diese in Module für die einzelnen Bewegungsphasen auf. Sie lassen sich, wie in Abb. 14 gezeigt, informell beschreiben, die Ein-und Ausgabekanäle sind in Abb. 15 gezeigt. Die Steuerung wird als Ttl-ähnliche Digitalschaltung konzipiert. Es muß sichergestellt werden, daß Ablauf der Phase 1. durch einen eventuellen gleichzeitigen Ablauf der Phase 2. nicht gestört wird und umgekehrt; analog für die Phase 3. und 4. Dazu wird die Spezifikation z.B. des Moduls für Phase 1. so ausgelegt, daß keine Voraussetzungen gemacht werden, die durch die gleichzeitige Aktivierung von Phase 2. ungültig werden. Es wird nur vorausgesetzt, daß in Phase 1. nicht gleichzeitig die Steuerung für das Zurückdrehen des Roboters oder für das Ausfahren seines ersten Armes aktiviert wird, was beides in Phase 2. nicht erfolgt. Dadurch können die von mehreren Modulen gemeinsam beeinflußten Ausgaben jeweils durch ein Oder-Gatter zusammengefaßt werden. Abbildung 16 zeigt die formale Spezifikation des Moduls für Phase 1. Die verwendeten Bezeichner sind in Anhang A informell erläutert und in Anhang B formal definiert.

	5 Entwicklung der Robotersteuerung
	1. Aufgabe:	transportiere ein Metallplättchen vom Hubdrehtisch in die Presse
	Voraussetzungen: Roboterarm 1 in Position über dem Hubdrehtisch (150,240)
		Hubdrehtisch in oberer Position im richtigen Winkel
		unbearbeitetes Metallplättchen liegt auf dem Hubdrehtisch
	2. Aufgabe:	transportiere ein Metallplättchen von der Presse auf das Ablageförderband
	Voraussetzungen: Roboterarm 2 in Position in der Presse (180,270)
		Presse in unterer Position
		rs(rp(rs(rs( sp(lab(l1, rs(rs(rs(user(u20), user(r11)), user(V or)), user(u47b)))), bearbeitetes Metallplättchen liegt in der Presse
	3. Aufgabe:	user(u30) ), user(u73) ), user(u30) ), sp(ref (l1)) ) fahre Arm 1 zurück zum Hubdrehtisch
	Voraussetzungen: Roboterarm 1 in Position in der Presse (270,360)
		oder Phase 4 läuft bereits Fig. 12. Termdarstellung des Beweises aus Abb. 10 unbearbeitetes Metallplättchen liegt auf dem Hubdrehtisch
	Ph Beginn 4. Aufgabe: fahre Arm 2 zurück zur Presse Ende Rob.bewegung
	Rob Hub Prs Voraussetzungen: Roboterarm 2 über dem Ablageförderband (270,360) Rob Prs Afb
		1. 150,240 o r Metallplättchen (bearbeitet oder unbearbeitet) in der Presse 270,360 m -
		o -		m r
		2. 180,270	u b 270,360 Fig. 14. Bewegungsphasen des Roboters -
			u -	b
		3. 270,360 r		150,240
		4. 270,360	b,r 180,270
				Modul/Phase	1. 2. 3. 4.
		Abkürzungen: Roboter Arm 1 Länge	*	*
		o obere Position	Roboter Arm 2 Länge	*	*
		m mittlere Position Roboter Winkel	* * * *
		u untere Position	Presse unten	* *
		b bearbeitetes Metallplättchen Presse mitte	*	* *
		r unbearbeitetes Metallplättchen Ablageförderband frei	*
		-leer		Roboter Arm 1 ausfahren	*
	Fig. 13. Bewegungsphasen des Roboters (schematisch) Roboter Arm 1 einfahren *
				Roboter Arm 1 greifen	*
				Roboter Arm 2 ausfahren	*
				Roboter Arm 2 einfahren	*
				Roboter Arm 2 greifen	*
				Roboter vor drehen	+ +
				Roboter zurück drehen	+ +

Die obere Zeile zu jeder Phase enthält ihre Vorbedingungen, die untere ihre Resultate. Die Position des Roboters wird durch die Winkel seiner beiden Arme angegeben (vgl. Abb. 2). (Die mit "+" gekennzeichneten Ausgaben werden von mehreren Modulen beeinflußt.) Fig. 15. Steuerungsmodule mit Ein-und Ausgabekanälen

  Es scheint keinen Grund zu geben, sie erst ab der Ebene der Software-Entwicklung einzusetzen, logik-basierte Methoden können im Gegenteil als ein Integrationsrahmen für eine verifizierte Entwicklung des Gesamtsystems, einschließlich klassischer Mechanik, dienen. Dies wurde durch unsere Behandlung der Fallstudie Fertigungszelle demonstriert, die gänzlich im rein technischen Bereich liegt und deren Spezifikation das Hauptziel (Fertigung bearbeiteter Metallplättchen) beinhaltet. Wenn das Hauptziel andererseits nichttechnischer Natur ist, wie z.B. in einem medizinischen Informationssystem, ist dieser Ansatz nicht voll anwendbar. war, ist sie für zeitkritische Anwendungen unvermeidbar, etwa im Bereich von Fahrzeugsteuerungssystemen, wo Aussagen über Beschleunigungs-und Bremszeiten lebenswichtig sind. Anhang Anhang A zeigt die informelle Beschreibung der in der Spezifikation der Fertigungszelle verwendeten Bezeichner. Abbildung 25 zeigt die Variablenkonventionen, Abb. 26 die Prädikate, Abb. 27 die Funktionen, Abb. 28 die Konstanten und Abb. 29 die expliziten Skolemfunktionen. In der rechten Spalte sind jeweils die in Anhang C verwendeten Kurzbezeichner aufgeführt. Anhang B zeigt die formale Anforderungsspezifikation der Fertigungszelle unter Verwendung der in Anhang A definierten Sprachebene (Axiome u1 bis u77). Die Axiome für Sicherheitsanforderungen sind weggelassen. Der Text wurde aus einer Web-artigen Darstellung [Knu84] gewonnen, die sich andererseits auch direkt in die Prolog-Eingabe für Sysyfos transformieren läßt. Im Anschluß daran sind die für die Synthese von Modul 1 benötigten Axiome und das Beweisziel aufgeführt (Axiome r1 bis r11, Beweisziel r20). Anhang C zeigt den Beweisbaum für den Hauptteil der Verifikation des Moduls 1 aus Abschnitt 5. Wenn sich die Presse nur lange genug hebt, erreicht sie schließlich die obere Position

			A Informelle Beschreibung der verwendeten Bezeichner B Formale Spezifikation der Fertigungszelle
	bearbeitet	=	möglicher Zustand eines Metallplättchens	bbt
	unbearbeitet =	möglicher Zustand eines Metallplättchens	ubt
	d1 d2 d3 presse(p, x) roboter(r, x) greif t1(r, t) greif t2(r, t) haelt1(r, s, t) haelt2(r, s, t) d4 d5 d6 d7 maxlg1 maxlg2 minlg1 minlg2 zh oben zh unten zp oben	= = = = = = = = = = = = = =	Anfangspunkt des Zuführförderbands (kartesischer Koordinatenvektor) p :Presse Endpunkt des Zuführförderbands (kartesischer Koordinatenvektor) x :Raumkoordinaten Mittelpunkt des Hubdrehtischs (kartesischer Koordinatenvektor) Presse t :Zeitpunkt s :Schiene (Metallplättchen) r :Zweiarmiger Roboter h :Hubdrehtisch f :Förderband α :Winkel Fig. 25. Informelle Beschreibung der verwendeten Variablenkonventionen d1 d2 d3 ⇔ p ist eine Presse und steht am Ort x prs ⇔ r ist ein zweiarmiger Roboter und steht am Ort x rob ⇔ Der erste Arm des Roboters r greift zum Zeitpunkt t (d.h. Magnet ein) gr1 ⇔ Der zweite Arm des Roboters r greift zum Zeitpunkt t gr2 ⇔ Der erste Arm des Roboters r hält zum Zeitpunkt t die Schiene s fest (d.h. magnetisch angezogen) ha1 ⇔ Der zweite Arm von r hält zum Zeitpunkt t die Schiene s fest ha2 ort(s, t) = Raumkoordinaten des Ortes, an dem sich die Schiene s zum Zeitpunkt t befindet bearbeitungszustand(s, t) = der Bearbeitungszustand der Schiene s zum Zeitpunkt t (∈ {bearbeitet, unbearbeitet}) pos1(r, t) = Koordinaten des Greifers des ersten Arms des Roboters r Drehzentrum des Roboters (kartesischer Koordinatenvektor) d4 Mittelpunkt der Presse (kartesischer Koordinatenvektor) u1. Die Presse preßt in oberer Position eine in ihr liegende unbearbeitete Schiene d5 Anfangspunkt des Ablageförderbands (kartesischer Koordinatenvektor) ∀[p, x, s, t, t2] ( d6 Endpunkt des Ablageförderbands (kartesischer Koordinatenvektor) presse(p, x) d7 maximale Länge von Roboterarm 1 ∧ bearbeitungszustand(s, t) = unbearbeitet mx1 maximale Länge von Roboterarm 2 ∧ proj xy(ort(s, t)) = proj xy(x) mx2 minimale Länge von Roboterarm 1 ∧ winkel(s, t) = 180 mn1 minimale Länge von Roboterarm 2 ∧ ∃[t1] (t t1 t2 ∧ hoehe(proj xy(x), t1) = zp oben) mn2 Höhe der oberen Position des Hubdrehtischs (z-Koordinate) → bearbeitungszustand(s, t2) = bearbeitet zho Höhe der unteren Position des Hubdrehtischs (z-Koordinate) ∧ proj xy(ort(s, t2)) = proj xy(x) zhu Höhe der oberen Position der Presse (z-Koordinate) ∧ winkel(s, t2) = 180) zpo u2.	ort btz
	dreht zurueck(r, t) zp mitte = Höhe der mittleren Position der Presse (z-Koordinate) ⇔ Der Roboter r dreht sich zum Zeitpunkt t gegen den zum Zeitpunkt t	zpm	ps1
	zp unten	=	mathematischen Drehsinn (d.h. im Uhrzeigersinn) = Projektion der Raumkoordinaten x auf die Bodenebene drz Höhe der unteren Position der Presse (z-Koordinate) proj xy(x) zpu	pxy
	dreht vor(r, t)	hoehe(x, t)	⇔	Der Roboter r dreht sich zum Zeitpunkt t im mathematischen = Höhe der Arbeitsfläche über dem Boden am Punkt
	Drehsinn (d.h. gegen den Uhrzeigersinn) mit den Planarkoordinaten x zum Zeitpunkt t (Für die Synthese von Modul 1 der Robotersteuerung:)	drv	hoe
	f aehrt aus1(r, t) t0 =	⇔ winkel xy(x, x1) Startzeitpunkt von Phase 1 Der Roboter r fährt zur Zeit t seinen ersten Arm nach außen = Winkel zwischen der Strecke x, x1 und der ausgezeichneten f a1 t0
	f aehrt ein1(r, t) s0 =	⇔ transportiertes Metallplättchen Der Roboter r fährt zur Zeit t seinen ersten Arm nach innen 0-Richtung (x,x1: Planarkoordinaten)	f e1 s0	wxy
	f aehrt aus2(r, t) ci =	⇔ winkel(h, t) Eingangsstartsignal (zeitabhängige Funktion) Der Roboter r fährt zur Zeit t seinen zweiten Arm nach außen = Aktueller Winkel des Hubdrehtisches h zum Zeitpunkt t f a2 ci	win
	f aehrt ein2(r, t) cdrv =	⇔ sensor1(h, t) externes Steuerungssignal zum Vordrehen des Roboters (zeitabhängige Funktion) Der Roboter r fährt zur Zeit t seinen zweiten Arm nach innen = Wert des unteren Sensors des Hubdrehtisches h zum Zeitpunkt t f e2 cdrv	ss1
	hubdrehtisch(h, x) cf a1 = externes Steuerungssignal zum Ausfahren von Arm 1 (zeitabhängige Funktion) ⇔ h ist ein Hubdrehtisch und steht am Ort x sensor2(h, t) = Wert des oberen Sensors des Hubdrehtisches h zum Zeitpunkt t hub cf a1	ss2
	hebt(h, t) cf e1	=	⇔ dist xy(x, x1) externes Steuerungssignal zum Einfahren von Arm 1 (zeitabhängige Funktion) Der Hubdrehtisch h fährt zum Zeitpunkt t nach oben = Abstand der XY-Projektionen von x und x1	hbt cf e1	dxy
	senkt(h, t) cgr1	=	⇔ winkel(s, t) externes Steuerungssignal zum Greifen von Arm 1 (zeitabhängige Funktion) Der Hubdrehtisch h fährt zum Zeitpunkt t nach unten = Aktueller Winkel der Schiene s zum Zeitpunkt t	snk cgr1	win
	dreht vor(h, t)	val(c, t)	⇔	Der Hubdrehtisch h dreht sich zum Zeitpunkt t im = Wert der zeitabhängigen Funktion c zum Zeitpunkt t	val
			mathematischen Drehsinn (d.h. gegen den Uhrzeigersinn) = liefert neue zeitabhängige Funktion, der Wert von trigger(c, v) ist 1 drv Fig. 28. Informelle Beschreibung der verwendeten Konstanten trigger(c, v)
	dreht zurueck(h, t)	⇔	Der Hubdrehtisch h dreht sich zum Zeitpunkt t gegen den gdw. der Wert von c ist kleiner als v	trg
			ampl(c, v)		mathematischen Drehsinn (d.h. im Uhrzeigersinn) = liefert neue zeitabhängige Funktion mit v-fach verstärktem Wert drz	amp
	f oerderband(f, x1, x2) neg(c) trv1(r, α, t) = Zeitpunkt, zu dem sich der Roboter r so weit vor gedreht hat, ⇔ f ist ein Förderband und läuft vom Punkt x1 zum Punkt x2 = Inverter (liefert neue zeitabhängige Funktion)	f or	neg
	laeuf t(f, t)		⇔ daß Arm1 den Winkel α hat, wenn er sich seit Zeitpunkt t vor dreht Das Förderband ist zum Zeitpunkt t in Bewegung and(c1, c2) = Und-Gatter (liefert neue zeitabhängige Funktion) trv1	lf t	and
	handhabungsgeraet(h, x1, x2) ⇔ or(c1, c2) trv2(r, α, t) = Zeitpunkt, zu dem sich der Roboter r so weit vor gedreht hat, h ist ein Handhabungsgerät und läuft zwischen x1 (links) = Oder-Gatter (liefert neue zeitabhängige Funktion)	or
			und x2 (rechts) = D-Flip-Flop (liefert neue zeitabhängige Funktion) daß Arm2 den Winkel α hat, wenn er sich seit Zeitpunkt t vor dreht df f (c1, c2) trv2	han	df f
	f abrik(f ) trz1(r, α, t) =	⇔ Zeitpunkt, zu dem sich der Roboter r so weit zurück gedreht hat, f ist eine wie im Modellschema beschrieben konfigurierte Fabrik mf f (c, d) = Zeitverzögerung um d Einheiten (liefert neue zeitabh. Funktion) f ab	mf f
	bewegt(m, s, t)	⇔ daß Arm1 den Winkel α hat, wenn er sich seit Zeitpunkt t zurück dreht Maschine m bewegt zum Zeitpunkt t die Schiene s	trz1	bw
	up(c, t) trz2(r, α, t) =	⇔ Zeitpunkt, zu dem sich der Roboter r so weit zurück gedreht hat, Die zeitabhängige Funktion springt zum Zeitpunkt t auf 1 Fig. 27. Informelle Beschreibung der verwendeten Funktionen
			(steigende Flanke) daß Arm2 den Winkel α hat, wenn er sich seit Zeitpunkt t zurück dreht	trz2	up
	tra1(r, d, t) =	Zeitpunkt, zu dem der Roboter r Arm1 bis zur Länge d ausgefahren hat,
			Fig. 26. Informelle Beschreibung der verwendeten Prädikate wenn er ihn seit Zeitpunkt t ausfährt	tra1
	tra2(r, d, t) =	Zeitpunkt, zu dem der Roboter r Arm2 bis zur Länge d ausgefahren hat,
			wenn er ihn seit Zeitpunkt t ausfährt	tra2
	tre1(r, d, t) =	Zeitpunkt, zu dem der Roboter r Arm1 bis zur Länge d eingefahren hat,
			wenn er ihn seit Zeitpunkt t einfährt	tre1
	tre2(r, d, t) =	Zeitpunkt, zu dem der Roboter r Arm2 bis zur Länge d eingefahren hat,
			wenn er ihn seit Zeitpunkt t einfährt	tre2
		Fig. 29. Informelle Beschreibung der verwendeten expliziten Skolemfunktionen

-Es gibt nur wenige adäquate Beschreibungsebenen. Unsere Erfahrung hat gezeigt, daß die Entscheidung, die Zeit nicht-diskret zu modellieren, notwendigerweise eine auf reellwertiger Zeit und stetigen Funktionen basierende Modellierung zur Folge hat, dazwischen scheint es keine adäquate Ebene mehr zu geben (etwa rationalwertige Zeit und beliebige Funktionen). Ein realistischeres Vorgehen wäre die Benutzung differenzierbarer Funktionen, um Aussagen über Beschleunigungen und Startgeschwindigkeiten machen zu können. Während eine solche Beschreibungsebene für die Fertigungszelle nicht unbedingt notwendig

  Wenn der Roboter mit Arm 1 zugreift, hält er eine Schiene, die sich im richtigen Winkel unter Arm 1 befindet Der Roboter hält eine einmal gegriffene Schiene mit Arm 1 fest, bis er sie wieder losläßt

	u7. ∀[r, x, t, s, x1] (
	roboter(r, x)
	∧ pos1(r, t) = x1
	∧ ort(s, t) = x1
	∧ winkel(s, t) = winkel xy(x, x1) -90
	∧ greif t1(r, t)
	→ haelt1(r, s, t))
	u8. Wenn der Roboter mit Arm 2 zugreift, hält er eine Schiene, die sich im richtigen Winkel unter
	Arm 2 befindet
	∀[r, x, t, s, x1] (
	roboter(r, x)
	∧ pos2(r, t) = x1
	∧ ort(s, t) = x1
	∧ winkel(s, t) = winkel xy(x, x1) -90
	∧ greif t2(r, t)
	→ haelt2(r, s, t))
	u9. ∀[r, x, s, t, t2] (
	roboter(r, x)
	∧ haelt1(r, s, t)
	∧ ∀[t1] (t t1 t2 → greif t1(r, t1))
	→ haelt1(r, s, t2)
	∧ bearbeitungszustand(s, t2) = bearbeitungszustand(s, t0))
	u10. Der Roboter hält eine einmal gegriffene Schiene mit Arm 2 fest, bis er sie wieder losläßt
	∀[r, x, s, t, t2] (
	roboter(r, x)
	∧ haelt2(r, s, t)
	∧ ∀[t1] (t t1 t2 → greif t2(r, t1))
	→ haelt2(r, s, t2)
	∧ bearbeitungszustand(s, t2) = bearbeitungszustand(s, t0))
	u11. Der Roboter bewegt eine gehaltene Schiene mit seinem Arm 1 mit
	∀[r, x, s, t] (
	roboter(r, x)
	∧ haelt1(r, s, t)
	→ ort(s, t) = pos1(r, t)
	∧ winkel(s, t) = winkel xy(x, pos1(r, t)) -90)
	u12. Der Roboter bewegt eine gehaltene Schiene mit seinem Arm 2 mit
	∀[r, x, s, t] (
	roboter(r, x)
	∧ haelt2(r, s, t)
	→ ort(s, t) = pos2(r, t)
	∧ winkel(s, t) = winkel xy(x, pos2(r, t) -90))
	Zweiarmiger Roboter

  Zuführförderband laufen c 2 Hubdrehtisch heben c 3 Hubdrehtisch senken c 4 Hubdrehtisch vor drehen c 5 Hubdrehtisch zurück drehen c 6 Roboter Arm 1 aus c 7 Roboter Arm 1 ein c 8 Roboter Arm 2 aus c 9 Roboter Arm 2 ein c 10 Roboter Arm 1 greifen c 11 Roboter Arm 2 greifen c 12 Roboter vor drehen c 13 Roboter zurück drehen c 14 Presse heben c 15 Presse senken c 16 Ablageförderband laufen s 1 Zuführförderband (1:Ende) s 2 Hubdrehtisch Vertikal (1:unten) s 3 Hubdrehtisch Vertikal (1:oben) s 4 Hubdrehtisch Drehung (Winkel) s 5 Roboter Arm 1 (Länge) s 6 Roboter Arm 2 (Länge) s 7 Roboter Drehung (Winkel Arm 1) s 8 Presse (1:unten) s 9 Presse (1:mitte) s 10 Presse (1:oben) s 11 Ablageförderband (1:Ende) d 1 Standort Zuführförderband Anfang d 2 Standort Zuführförderband Ende d 3 Standort Hubdrehtisch d 4 Standort Roboter d 5 Standort Presse d 6 Standort Ablageförderband Anfang d 7 Standort Ablageförderband Ende

	Gesamte Fabrik
	u42. Konfiguration der Fabrik
	c 1

  u43. Das Handhabungsgerät "verbraucht" die Schienen beim Zurückführen, um einen geschlossenen Kreislauf zu ermöglichen c 17 Handhabungsgerät links c 18 Handhabungsgerät rechts c 19 Handhabungsgerät heben c 20 Handhabungsgerät senken c 21 Handhabungsgerät greifen s 12 Handhabungsgerät Horizontal (1:links) s 13 Handhabungsgerät Horizontal (1:rechts) s 14 Handhabungsgerät Vertikal (Höhe) d 8 Standort Handhabungsgerät Ende (links) d 9 Standort Handhabungsgerät Anfang (rechts)

Dieser Abschnitt entspricht der deutschen Fassung des zweiten Kapitels von[START_REF] Lewerentz | Formal Development of Reactive Systems -Case Study Production Cell[END_REF] und wurde mir freundlicherweise von Thomas Lindner zur Verfügung gestellt.

& (t0 =< t5$ & t5$ =< trv1(r(),wxy(d4,d5),t0)

|

-> val(or(ca1,and(dff(ci,neg(or(trg(ampl(s8,-1),bb6*-1), | trg(s10,wxy(d4,d5))))),cb2)),t34) = 1 , -| 139** wxy(d4,ps1(r(),t20)) = val(s7,t20) , -| 153** val(c25,t32) < v -> val(trg(c25,v),t32) = 1 , -182rp wxy(d4,ps1(r(),t20)) < v -> val(trg(s7,v),t20) = 1 , -183re val(ca1,t34) = 1 ! t0 =< t34 & t34 < trv1(r(),wxy(d4,d5),t0) & wxy(d4,ps1(r(),t34)) < v -> val(or(ca1,and(dff(ci,neg(or(trg(ampl(s8,-1),bb6*-1), trg(s10,wxy(d4,d5))))),trg(s7,v))),t34) = 1 , -172** t0 =< t9 & t9 < trv1(r(),wxy(d4,d5),t0) -> wxy(d4,ps1(r(),t9)) < wxy(d4,d5) , -184re val(ca1,t34) = 1 ! t0 =< t34 & t34 < trv1(r(),wxy(d4,d5),t0) & t34 < trv1(r(),wxy(d4,d5),t0) -> val(or(ca1,and(dff(ci,neg(or(trg(ampl(s8,-1),bb6*-1), trg(s10,wxy(d4,d5))))),trg(s7,wxy(d4,d5)))),t34) = 1 , -185un val(ca1,t34) = 1 ! t0 =< t34 | & t34 < trv1( r(c29,c30,c31,c32,c33,c34,c35,c36,s22,s23,s10) ,wxy(d4,d5),t0) | -> val(or(ca1,and(dff(ci,neg(or(trg(ampl(s8,-1),bb6*-1), | trg(s10,wxy(d4,d5))))),trg(s10,wxy(d4,d5 -> up(co,trv1(r(),wxy(d4,d5),t0))) 317un -, (tre1(r(),dxy(d4,d5),t0)=<t18$&t18$=<trv1(r(),wxy(d4,d5),t0) -> ~val(cfa1,t18$)=1) & (t0 =< t8$ & t8$ < trv1(r(),wxy(d4,d5),t0) -> val(c21,t8$) = 1) & (ort(s0,trv1(r(),wxy(d4,d5),t0)) = ps1(r(),trv1(r(),wxy(d4,d5),t0)) -> up(co,trv1(r(),wxy(d4,d5),t0))) 318re -, (tre1(r(),dxy(d4,d5),t0)=<t18$ & t18$=<trv1(r(),wxy(d4,d5),t0) -> ~val(cfa1,t18$)=1) & (t0 =< t8$ & t8$ < trv1(r(),wxy(d4,d5),t0) -> val(ca1,t8$) = 1 ! t8$ < trv1(r(),wxy(d4,d5),t0)) & (ort(s0,trv1(r(),wxy(d4,d5),t0)) = ps1(r(),trv1(r(),wxy(d4,d5),t0)) -> up(co,trv1(r(),wxy(d4,d5),t0))) 319un -, (tre1(r(),dxy(d4,d5),t0) =< t18$ & t18$=<trv1(r(),wxy(d4,d5),t0) -> ~val(cfa1,t18$)=1) & (ort(s0,trv1(r(),wxy(d4,d5),t0)) = ps1(r(),trv1(r(),wxy(d4,d5),t0)) -> up(co,trv1(r(),wxy(d4,d5),t0))) 9** 320re -, (tre1(r(),dxy(d4,d5),t0) =< t18$ & t18$ =< trv1(r(),wxy(d4,d5),t0) -> t0 =< t18$ & t18$ =< trv1(r,270,t0)) & (ort(s0,trv1(r(),wxy(d4,d5),t0)) = ps1(r(),trv1(r(),wxy(d4,d5),t0)) -> up(co,trv1(r(),wxy(d4,d5),t0))) 88u47 wxy(d4,d5) = 270 , -321RP -, (tre1(r(),dxy(d4,d5),t0) =< t18$ & t18$ =< trv1(r(),wxy(d4,d5),t0) -> t0 =< t18$ & t18$ =< trv1(r,wxy(d4,d5),t0)) & (ort(s0,trv1(r(),wxy(d4,d5),t0)) = ps1(r(),trv1(r(),wxy(d4,d5),t0)) -> up(co,trv1(r(),wxy(d4,d5),t0))) 322un -, (tre1(r(),dxy(d4,d5),t0) =< t18$ & t18$ =< trv1(r(),wxy(d4,d5),t0) -> t0 =< t18$) & (ort(s0,trv1(r(),wxy(d4,d5),t0)) = ps1(r(),trv1(r(),wxy(d4,d5),t0)) -> up(co,trv1(r(),wxy(d4,d5),t0))) 100** aa6 =< bb5 & bb5 =< cc3 -> aa6 =< cc3 , -323re -, (tre1(r(),dxy(d4,d5),t0) =< t18$ & t18$ =< trv1(r(),wxy(d4,d5),t0) -> t0 =< bb5 & bb5 =< t18$) & (ort(s0,trv1(r(),wxy(d4,d5),t0)) = ps1(r(),trv1(r(),wxy(d4,d5),t0)) -> up(co,trv1(r(),wxy(d4,d5),t0))) 253** t19 =< tre1(r8,d10,t19) , -324re -, (tre1(r(),dxy(d4,d5),t0) =< t18$ & t18$ =< trv1(r(),wxy(d4,d5),t0) -> tre1(r8,d10,t0) =< t18$) & (ort(s0,trv1(r(),wxy(d4,d5),t0)) = ps1(r(),trv1(r(),wxy(d4,d5),t0)) -> up(co,trv1(r(),wxy(d4,d5),t0))) 325un -, ort(s0,trv1( r( cfa1, or(cfe1, and(dff(ci,neg(or(trg(ampl(s22,-1),dxy(d4,d5)*-1),trg(s10,wxy(d4,d5))))), trg(ampl(s22,-1),dxy(d4,d5)*-1) )

), c31, c32, or(cgr1,dff(ci,neg(or(trg(ampl(s22,-1),dxy(d4,d5)*-1),trg(s10,wxy(d4,d5)))))), c34, or(cdrv, and(dff(ci,neg(or(trg(ampl(s22,-1),dxy(d4,d5)*-1),trg(s10,wxy(d4,d5))))), trg(s10,wxy(d4,d5)) )

), c36, s22, s23, s10 ), wxy(d4,d5),t0)) = ps1(r(),trv1(r(),wxy(d4,d5),t0)) -> up(co,trv1(r(),wxy(d4,d5),t0))