VerDikt - Verifikation semistrukturierter Dokumente mit Kontextabhängigkeiten

• Antragsteller: Professor Dr. Burkhard Freitag
• Fachliche Zuordnung: Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme
• Förderung: Förderung von 2007 bis 2013
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 35223802

• Erstellungsjahr: 2012

Zusammenfassung der Projektergebnisse

Das Projekt Verdikt – “Verifikation semistrukturierter Dokumente im Kontext” – hat das Ziel, Methoden zur automatischen Prüfung der Konsistenz von Dokumenten zu entwickeln. Ein Dokument wird dann als konsistent angesehen, wenn es bestimmte Vorgaben an seine Struktur und an seinen Inhalt erfüllt, so dass keine wesentlichen Informationen fehlen und der Inhalt verständlich und zusammenhängend vermittelt wird. Die automatisierte Überprüfung inhaltlich-struktureller Vorgaben reduziert den Aufwand in der Qualitätssicherung und hilft, Fehler in Prozessbeschreibungen, technischen Dokumentationen, Bedienungsanleitungen und anderen strukturierten Dokumenten zu vermeiden. Die grundlegende Funktionalität des Verfahrens wurde bereits im ersten Projektabschnitt sichergestellt, so dass sich dieser Bericht mit den erweiterten Zielen des zweiten Abschnitts befasst. Die Übertragbarkeit auf andere Domänen und Einsatzgebiete ist ein wichtiger Indikator für den generellen Nutzen des Ansatzes. Deshalb war es ein Ziel des zweiten Projektabschnitts, diese Übertragbarkeit nicht nur zu evaluieren, sondern auch so stark wie möglich zu vereinfachen. Es war möglich, durch Verwendung von domänenspezifischem Hintergrundwissen die inhaltlich-strukturelle Analyse der Dokumente so weit zu generalisieren, dass bei einem Domänenwechsel neben dem Austausch dieses Hintergrundwissens und der Formulierung neuer Konsistenzvorgaben nur wenige Anpassungen nötig sind. Aufgrund der stark unterschiedlichen Konsistenzanforderungen in unterschiedlichen Domänen ist eine Verwendung der bereits formulierten Vorgaben in den meisten Fällen nicht möglich. Die Erstellung solcher Vorgaben ist bereits inhaltlich außerordentlich komplex. Daher ist es besonders wichtig, eine weitere Erhöhung dieser Komplexität durch die Formalisierung zu vermeiden. Zu diesem Zweck wurde die bereits entwickelte Muster-basierte Spezifikation um eine Beispiel-basierte Spezifikation ergänzt, die vom Anwender keine Vorkenntnisse in formaler Verifikation verlangt. Statt dessen erlaubt sie es, anhand vereinfachter, dem Anwender aus seiner Domäne vertrauter Dokumente die Vorgaben nicht nur anzugeben, sondern auch zu testen und Auswirkungen von Veränderungen der Vorgabe direkt zu beobachten. Oft ist es nötig, auf bestimmte Aspekte eines Dokuments zu fokussieren und andere Aspekte auszublenden, um Vorgaben sinnvoll formulieren und prüfen zu können. Für einige Vorgaben benötigt man einen überblicksartigen Blick auf das zu prüfende Dokument, ohne sich in Feinheiten zu verlieren. Für andere Vorgaben wiederum ist ein sehr detaillierter Blick nötig. Um diesen unterschiedlichen Anforderungen gerecht zu werden, wurde ein Ansatz entwickelt mit dem unterschiedliche Sichten auf das Dokument definiert werden können. Jede dieser Sichten blendet unnötige Aspekte aus und ermöglicht so nicht nur eine effizientere Überprüfung der Vorgaben, sondern erlaubt es sogar, Vorgaben zu prüfen, die ohne diese Fokussierung nicht zu formulieren gewesen wären. Kontexte haben an verschiedenen Stellen Einfluss auf die Verifikation. Die Konsistenzvorgaben an ein Dokument können sich abhängig vom Dokumentbereich unterscheiden, so dass beispielsweise in sicherheitsrelevanten Bereichen stärkere Vorgaben gelten als in anderen Bereichen. Dies lässt sich leicht mit der bereits erprobten Methode der Definition von Sichten verwirklichen, indem unterschiedliche Sichten mit Fokus auf die jeweiligen Dokumentbereiche erstellt werden, in denen andere Vorgaben erfüllt sein sollen. Der Kontext kann außerdem Einfluss auf die Interpretation von Inhalten haben. Beispielsweise kann die tatsächliche, vom Kontext abhängige Bedeutung eines Wortes wie “Bank” darüber entscheiden, ob sich das Vorkommen des Begriffs auf das Ergebnis der Verifikation auswirkt. Die Erwähnung von Sitzmöbeln hat im Allgemeinen auf Prüfergebnisse in der Finanzdomäne keine Auswirkungen, anders als vielleicht die Erwähnung von Geldinstituten. Die im Verdikt Projekt erzielten Ergebnisse erlauben es, effektiv und effizient komplexe Konsistenzvorgaben an Dokumente zu formulieren und zu überprüfen. Die Ausdruckskraft der Vorgaben ist dabei deutlich größer als bei bisherigen Ansätzen und das Vorgehen kann leicht auf andere Anwendungsbereiche übertragen werden. Das entwickelte Softwareframework erlaubt eine direkte Nutzung der Ergebnisse für vorgegebene Domänen und Dokumentformate und kann auf weitere Domänen und Formate erweitert werden.

Projektbezogene Publikationen (Auswahl)

• Dokumentverifikation mit Temporaler Beschreibungslogik, Universität Passau, Fakultät für Informatik und Mathematik, Diss. 2008. Gesellschaft f. Informatik e.V., Bonn, Ausgezeichnete Informatikdissertationen 2008, GI-Edition der LNI
  Franz Weitl
  
• Logic-based verification of technical documentation. In DocEng 09: Proceedings of the 9th ACM Symposium on Document Engineering, pages 251–252, Munich, Germany, 2009. ACM
  Christian Schönberg, Franz Weitl, Mirjana Jakšić , and Burkhard Freitag
  
• Incremental construction of counterexamples in model checking web documents. In Proc. of the 6th International Workshop on Automated Specification and Verification of Web Systems (WWV 2010), pages 61–75, Vienna, Austria, 2010
  Franz Weitl and Shin Nakajima
  
• Rich ontology extraction and wikipedia expansion using language resources. In Proceedings of the 11th International Conference on Web-Age Information Management (WAIM’10), LNCS, volume 6184, Jiuzhaigou, China, 2010. Springer
  Christian Schönberg, Helmuth Pree, and Burkhard Freitag
  
• Structured counterexamples for the temporal description logic ALCCTL. In Proc. of the 8th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2010), Pisa, Italy, 2010
  Franz Weitl, Shin Nakajima, and Burkhard Freitag
  
• Temporal patterns for document verification. In Proc. of the 6th International Workshop on Automated Specification and Verification of Web Systems (WWV 2010), pages 17–31, Vienna, Austria, 2010
  Mirjana Jakšić and Burkhard Freitag
  
• Verifying the consistency of web-based technical documentations. Journal of Symbolic Computation, Special Issue on Automated Specification and Verification of Web Systems, 46(2):183–206, 2011
  Christian Schönberg, Franz Weitl, and Burkhard Freitag