Ein großes Problem bei der gemeinsamen Erstellung von Dokumenten durch mehrere Personen betrifft die Konsistenz der Daten, denn jeder sollte beliebige Änderungen vornehmen können. Dies gilt in besonderem Maß, wenn Benutzer mit mobilen Endgeräten beteiligt sind, welche nicht permanent mit den Datenservern verbunden sind und somit die meiste Zeit Offline arbeiten. D.h. die Daten werden lokal bearbeitet und Änderungen eher abschnittsweise, auf einmal in das gemeinsame Dokument eingebracht. Um die dabei nicht zwangsweise entstehenden Inkonsistenzen zu kontrollieren und zu beheben, wurden bereits eine Reihe von Protokollen zur Konsistenzerhaltung (z.B. Grove, 2-Phasen-Sperren) vorgeschlagen.

Diese, mit zunehmender Komplexität, verwendeten Protokolle bestimmen in großem Maß den reibungslosen Ablauf bei der gemeinsamen Erstellung/Bearbeitung von Dokumenten. Deren Zuverlässigkeit scheint eine unabdingbare Forderung zu sein. Der Nachweis der "fehlerfreien Funktion"(Verifikation) ist jedoch ein sehr schwieriges Unterfangen.

Die am häufigsten verwendeten Verifikationstechniken sind Test (z.B. Blackbox- und Glasboxtest) und Simulation. Diese Verfahren sind jedoch sehr aufwändig und garantieren keine 100%ige Fehlerfreiheit.

Anfang der 80er Jahre wurde eine Methode entwickelt, welche es erlaubt, die logische Struktur komplexer Systeme/Protokolle vollautomatisch zu analysieren und den Nachweis der gestellten Anforderungen zu erbringen. Diese Technik wird Model Checking genannt und ist Grundbaustein moderner Verifikationswerkzeuge (z.B. Spin, Verisoft, UPPAAL, ...). Diese Werkzeuge erlauben die Modellierung und Verifikation von parallelen Systemen, Kommunikationsprotokollen und u.v.m.

Dabei werden die unterschiedlichsten Methoden verwendet. Beispielsweise besitzt Spin eine eigene Spezifikationssprache, mit welcher z.B. Kommunikationsprotokolle nachgebildet werden können, wogegen Verisoft auf dem Sourcecode arbeitet und die gestellten Forderungen direkt im zu überprüfenden System/Protokoll definiert werden können.

Um die an ein zu verifizierendes System gestellten Forderungen präzise formulieren und überprüfen (z.B. Finden von Deadlocks (Verklemmungen) und "unerreichbaren" Unterroutinen) zu können, verwenden die einzelnen Werkzeuge gesonderte oder integrierte Spezifikationsformalismen (z.B. LTL, CTL).