Ein Ansatz zur Analyse von Systemspezifikationen und -entwürfen mithilfe von Modellen und Eigenschaften, die sich logisch überprüfen lassen.
Hillel Wayne stellt Prinzipien formaler Methoden vor, um Designfehler vor der Implementierung eines Systems zu erkennen, mit Schwerpunkt auf der Stärke von Eigenschaften, der Erkundung des Zustandsraums und Umgebungsannahmen. Die Beispiele zeigen, wie eine vereinfachte Analyse von Nebenläufigkeit, Fehlern und Wiederholungsversuchen kostspielige Fehler frühzeitig aufdecken kann.