Die modellbasierte Systementwicklung kann nur dann zu anforderungsgerechten Systemen fu¨hren, wenn die zugrundeliegenden Modelle die tatsa¨chlichen Anforderungen widerspiegeln. Zu den Anforderungen geho¨rt die existierende oder geplante Systemungebung (die reale Welt) sowie das gewu¨nschte Verhalten des Systems in dieser Umgebung. Die prozessorientiere Systementwicklung gibt sowohl fu¨r die Umgebung als auch fu¨r das Verhalten Prozesse und Prozesseigenschaften vor. In diesem Tutorium wird gezeigt, wie durch alternierende Anwendung von Validierungs- und Verifikationsschritten ein korrektes und valides Gesamtmodell der zu unterstu¨tzenden Prozesse erzeugt wird, das als formale Spezifikation fu¨r das zu implementierende System verwendet werden kann. Der Ansatz verwendet verschiedene Typen von Petrinetzen. Im folgenden Bild wir die unterschiedliche Rolle von Validierung und Verifikation dargestellt. Dabei ist Validierung stets als Gegenstu¨ck zu Formalisierung zu verstehen, wie auch Verifikation mit Spezifikation ein derartiges begriffliches Paar bildet. Die Evaluation des Systems betrifft die modellunabha¨ngige Bewertung des implementierten Systems (siehe fu¨r eine ausfu¨hrlichere Diskussion [De02]).
reale
Welt Evaluation
derungsspez.
Entwurfsspez.
Validierung Validierung
Verifikation Das Diagramm macht deutlich, dass Formalisierung und Validierung an verschiedenen Stellen auftreten; zum einen bei der Modellierung eines gegebenen Systems (der Umgebung bzw. der realen Welt), zum anderen bei der Modellierung des zu implementierenden Systems. Entsprechend spielt die Spezifikation und Verifikation sowohl bei dem Schritt von den Anforderungen zum Entwurf eine Rolle als auch bei dem Schritt vom Entwurf zur Implementierung. In dem hier dargestellten Ansatz werden Verifikationsverfahren außerdem bei der Validierung von Anforderungen eingesetzt.
Um formale Verfahren bei Validierung und Verifikation einsetzen zu ko¨nnen, beziehen wir uns auf formale Prozessmodelle, gegeben durch ho¨here Petrinetze. Diese haben eine graphische Darstellung, sind mathematisch definiert und sind ausfu¨hrbar (siehe die Diskussion in [DJ01]). Die graphische Darstellung unterstu¨tzt das intuitive Versta¨ndnis eines Petrinetz-Modells, unabha¨ngig von der genauen Petrinetz-Variante (insofern sind Petrinetze eine fru¨he UML fu¨r Prozessmodelle). Die Ausfu¨hrbarkeit erlaubt die Konstruktion von Simulatoren. Die mathematische Grundlage ist Voraussetzung fu¨r Analyseverfahren. Im Projekt VIP1 wurde ein simulationsbasierter Ansatz zur Validierung und Verifikation von Prozessmodellen entwickelt, der auf halbgeordneten Abla¨ufen von (ho¨heren) Petrinetz-Modellen von Systemen beruht [De00]. In folgenden wird dieser Ansatz skizziert. Die Grundannahme des Ansatzes ist, dass der Entwickler eine genaue Vorstellung von gu¨ltigen Abla¨ufen eines (existierenden oder zu konstruierenden) Systems besitzt. Ein Ablauf beschreibt Aktivita¨ten und ihren kausalen Zusammenhang, der durch die jeweiligen Vor- und Nachbedingungen gegeben ist. Jeder Ablauf la¨sst sich durch eine halbgeordnete Struktur bzw. durch ein spezielles Petrinetz, dessen Elemente Aktivita¨ten und Bedingungen repra¨sentieren, darstellen [DR98]. Zusa¨tzlich geho¨ren zur Systemspezifikation Eigenschaften, die fu¨r alle Abla¨ufe erfu¨llt sein mu¨ssen (die also durch eine Linear-Time Logik ausgedru¨ckt werden ko¨nnen). Diese werden in einer Petrinetz-angelehnten Syntax formuliert.
Bei dem Entwicklungsprozess eines Petrinetz-Modells werden durch Simulation Ablaufnetze generiert und visualisiert. Dies macht dem Entwickler deutlich, welches Systemverhalten er mit seinem Modell spezifiziert hat. Die generierten Abla¨ufe ko¨nnen bezu¨glich der zusa¨tzlichen logischen Spezifikationen automatisch untersucht werden (an dieser Stelle werden Verifikationsverfahren beim Validierungsprozess eingesetzt). Dies erlaubt die Validierung der Anforderungen; es wird genau deutlich, welche Abla¨ufe durch eine Anforderung ausgeschlossen werden und welche nicht.
Dieses Vorgehen kann zur schrittweisen Implementierung weiterer Spezifikationen wiederholt eingesetzt werden, bis schließlich eine Entwurfsspezifikation entstanden ist, die sowohl das Verhalten des (validierten) Umgebungsmodells respektiert als auch allen (validierten) Anforderungen entspricht. Die Implementierung einer Spezifikation erfolgt dabei halbautomatisch, erfordert aber im allgemeinen jeweils einen anschließenden Verifikationsschritt. Zudem ko¨nnen Spezifikationen nicht in beliebiger Reihenfolge implementiert werden, um fru¨here Spezifikationen durch Systemvera¨nderungen nicht zu verletzen. Zur Verifikation von Sicherheitseigenschaften bieten sich klassische Petrinetz-Techniken an, wie sie fu¨r elementare Netze z.B. in [De98a, De98b] beschrieben werden. Fu¨r Le1Verifikation von Informationssystemen durch Auswertung halbgeordneter Prozesse, gefo¨rdert durch die DFG Jo¨rg Desel. Petrinetze, lineare Algebra und lineare Programmierung. Teubner-Texte zur Informatik Band 26. Teubner, Stuttgart 1998 bendigkeitseigenschaften werden andere Verfahren beno¨ tigt, wie z.B. die fu¨ r Petrinetze adaptierte Proof-Graph Methode [DK98, DK01].
Erweiterungen des Ansatzes betreffen einerseits eine Validierung unter Beru¨ cksichtigung von zeitlichen Aspekten und von Kosten der unterstu¨ tzten Abla¨ufe [DE00a] und andererseits die Beru¨ cksichtigung flexibler Ablaufbeschreibungen im Rahmen von WorkflowSystemen [DE00b].
In der abschliessenden Literatursammlung sind aus Platzgru¨ nden nur Publikationen des Autors aufgefu¨ hrt, die im Tutorium angesprochen werden. Grundlagen und weitere Literaturangaben findet man in diesen Arbeiten.
Literatur [De98a] [DK98] [DR98] [De00]
Jo¨rg Desel und Ekkart Kindler. Proving correctness of distributed algorithms - a case study. In: Proceedings of the 1998 International Conference on Application of Concurrency to System Design (CSD’98), Fukushima, Japan, Ma¨rz 1998, pp.177-186, IEEE Computer Society Press (1998) [DJ01] [DK01] [De02] Jo¨rg Desel und Ekkart Kindler. Petri Nets and Components – Extending the DAWN Approach. In: Moldt, D. (ed.): Workshop on Modelling of Objects, Components. and Agents, Aarhus, Denmark, DAIMI PB–553 (2001) 21–36