Autoren: Stefanie Rinderle, Manfred Reichert, Peter Dadam

Sollen Workflow-Management-Systeme (WfMS) in umfassender Weise für die rechnerbasierte Verwaltung und Steuerung von Geschäftsprozessen einsetzbar sein, müssen die von ihnen verwalteten Workflow-Schemata und -Instanzen bei Bedarf rasch anpassbar sein. Dabei müssen die auf Basis eines (alten) Workflow-Schemas erzeugten Workflow-Instanzen auch nach dessen Änderung ungestört weiterlaufen können, etwa durch Bereitstellung geeigneter Versionskonzepte. Sehr viel schwieriger wird es, wenn die angewandten Schemaänderungen - wo gewünscht und semantisch möglich - auch auf die bereits (vielleicht in großer Zahl) laufenden Workflow-Instanzen übertragen werden sollen. Dies bei Bedarf zu können - und zwar ohne Inkonsistenzen oder Fehler zu verursachen - ist aber ungemein wichtig, wenn WfMS breit und umfassend einsetzbar sein sollen. In diesem Beitrag wird erstmals ein Ansatz zur effizienten Prüfung auf Migrierbarkeit von WF-Instanzen bei WF-Schemaänderungen vorgestellt. Dabei werden auch fortschrittliche WF-Beschreibungskonstrukte (z. B. Schleifen) in die Betrachtungen einbezogen. Außerdem wird aufgezeigt, wie der Benutzer durch eine effiziente und automatische Migration von Workflow-Instanzen optimal unterstützt werden kann. An den Kernteilen dieses Beitrags, wie effiziente Überprüfbarkeit bei Migration von Workflow-Instanzen, umfassende Unterstützung wichtiger Modellaspekte und Benutzerfreundlichkeit durch automatische Anpassungen bei Workflow-Instanzmigrationen, führt kein Weg zu einem umfassenden Änderungsmanagement vorbei.

PDF

Autoren: Walter Guttmann

We proceed by program transformation to derive a version of the Heapsort algorithm from a non-deterministic specification. The object language is Haskell and, therefore, the style of the resulting Heapsort program is necessarily applicative. Our development is supported by the program transformation system Ultra. Although a valuable tool, several shortcomings of Ultra are identified.

PDF

Autoren: Axel Dold, Friedrich W. von Henke, Vincent Vialard, Wolfgang Goerigk

We report on a large verification effort in constructing an initial fully trusted bootstrap compiler executable for a realistic system programming language and real target processor. The construction and verification process comprises three tasks: the verification of the compiling specification (a relation between abstract source and target programs) with respect to the language semantics and a realistic correctness criterion. Second, the implementation of this specification in the high-level source language following a transformational approach, and third, the construction of a binary executable written in the compiler's target language. The focus of this report is on the first verification task. This proof has been completely mechanized using the PVS specification and verification system and is one of the largest case-studies in formal verification we are aware of.

PDF