MORES2

Das Projekt MORES2 zielt auf die Entwicklung geeigneter Verfeinerungstechniken für Workflow-Spezifikationen. Dabei müssen zum einen die verschiedenen Aspekte der Workflowmodellierung (z.B. Tasks, Daten, Benutzer) geeignet verfeinerbar sein und zum anderen die Sicherheitseigenschaften auf entsprechende Eigenschaften auf anderen Verfeinerungsebenen übersetzbar sein. Sicherheitsgarantien auf oberen Ebenen dienen damit als initiale Bausteine für eine Verifikation der Sicherheit auf unterliegenden Ebenen. Es kann dabei nicht erwartet werden, dass der zu entwickelnde Verfeinerungsbegriff die Sicherheitsgarantien invariant lässt, da zum einen dies die möglichen Verfeinerungen derartig reduziert, dass sie in der Praxis kaum noch relevant wären, und zum anderen beim Übergang zwischen den Verfeinerungsebenen es zu einer Modifikation der Beobachtungsmöglichkeiten kommen kann, die zu einem Wechsel der Modellierung der geforderten Sicherheitsgarantien führt. MORES2 wird daher Techniken entwickeln, um die Sicherheitsgarantien der oberen Ebenen in den Nachweis der entsprechenden Sicherheitseigenschaften auf unteren Ebenen zu integrieren. Eine entsprechende Werkzeugunterstützung auf Basis existierender interaktiver Beweiser wird hierfür aufgebaut.