Anmerkungen zum Prozess:

  - Im Falle der Naehe der konventionellen Formalisierung zu einem Muster
    kann man viel Zeit damit verbringen, die Problemspezifikation an das
    Muster anzupassen (statt umgekehrt).

  - Es fehlen ggf. Architekturbeschreibungsmoeglichkeiten in der Anforderungs-
    spezifikation. Oft werden solche Zuordnungen implizit ueber die Wahl des
    Praedikatnamens erledigt - das ist aber verlogen.
    Ersatzloesung: Mitschleifen des nicht-formalisierten Anteils pro 
    Anforderung
    Diese informelle Uebernahme von (vom Kunden gewuenschten)
    Komponenten, z.B. das Control panels, zur Formalisierung in spaeteren
    Entwurfsschritten, ist aber nur eine Notloesung. 

  - Der eingesetzte Qualitaets- und Kreativitaetsaufwand zur Erreichung einer
    "schoenen" Loesung kann den Aufwand zur Erreichung "einer" Loesung um
    Dimensionen uebertreffen. Evtl. waere es sinnvoll, Zeitschranken fuer
    die Formalisierung einer Anforderung festzulegen.

  - Patterns sollten ggf. problemorientierter sein (-> Katalog). Typischerweise
    greift man naemlich lieber auf die bereits instantiierte Version eines 
    Musters zurueck und aendert die Parametrierung: "Das ist doch dasselbe
    wie in Anforderung ..." und macht copy and paste!
    Praktischer ist also z.B. ein Pattern "Benutzerwarnung" als die nochmalige
    Instantiierung des DelayedEquivalence Patterns.

  - Was macht man mit Needs in der Problembeschreibung, bei denen der Kunde
    bereits eine systeminterne Groesse zur Beschreibung verwendet hat, z.B.
    "system malfunction implies userInformed" ? Die "system malfunction" ist
    i.a. eine systeminterne, sich spontan aendernde Groesse.
    Eine Verfeinerung durch Umweltgroessen ist schwierig, aber u.U. notwendig
    -> zusaetzlicher Prozessschritt?

  - Trennung in "interne" und "externe" Comments.

  - Erweiterung der Logik: z.B. Strictly sometimes in the past:
    Notation mit Intervallen im Index: \sometimesInThePast_(0,t]

  - Erweiterung der Logik: Domaenen fuer Terme

  - Praedikate oder andere Groessen muessen nicht sofort in der Umwelt 
    verankert werden. Dies bedeutet, dass man mit unvollstaendigen
    Spezifikationen arbeitet. Bsp.: "facility manager is informed" und
    "system malfunction" oder "hazardousCondition" koennen noch 
    nicht vollstaendig in der Umwelt verankert werden.

  - "Interne Groessen" widersprechen nicht dem Spezifikationsgedanken, wenn
    sie aus der Historie der Umweltgroessen ableitbar sind.

  - DelayedCopy definieren!

  - Die verwendete FDT sollte als Eingabedokument fuer den Anf.Spez.prozess 
    explizit eingefuehrt werden.

  - Es ist sinnvoll, in der gemeinsamen Deklaration von Praedikaten, Funktionen
    und Domains die angewandten Vorkommen mitanzugeben.

  - Abkuerzungen in Identifiern sind oft ein Hinweis auf weitere Strukturier-
    ungsmoeglichkeiten.

  - Bsp.: Room::Property U1 = fmLightOff \delImp lightOff
    Problem  : Rueckgriff auf eine Groesse, die nicht lokal im Room vorliegt.
    Vorteil  : Automatische Instanziierung fuer alle Raeume
    Nachteil : Notwendige Unifikation fmLightOff == fm.lightOff spaeter nicht
	       direkt umsetzbar. U1 spezifiert eben eine nicht-lokale 
	       Eigenschaft.

    Alternative: Nur lokale Groessen in Teil-Spezifikationen verwenden!
    Vorteil    : u.a. Evidenz der Globalitaet von Eigenschaften
    Nachteil   : U1 wird auf hoeherer (ausreichend lokaler) Ebene spezifiziert
		 und muss dabei durch \forall r \in ROOMS allquantifiziert
		 werden -> u.a. zusaetzl. Domaene ROOMS.

  - Wie umfangreich muss die Umweltbeschreibung ausfallen - wann ist sie
    vollstaendig? 
    Ein Kriterium ist die Frage, ob die Umwelt "schreibend" auf eine der
    betrachteten Umweltgroessen zugreift. Z.B. beeinflusst die Umwelt von sich
    aus die Groesse 'Raumtemperatur' durch den Waermefluss durch die 
    Aussenflaechen.

 - Kundenreview immer mit gemeinsamer Diskussion abschliessen. Schriftliches
   vom Kunden ist meist wertlos. D.h.: CustomerReq -> gemeinsam formuliertes
   CustomerResp -> gemeinsam formulierte Solution

 - ?? Behandlung dynamischer Zeitschranken, z.B. t vom Hausmeister einstellbar
   und irgendwo p \delImp_t q