Zur Modellierung von Softwarearchitekturen kann eine ganze Reihe formaler Notationen verwendet werden. Sprachen wie B, Z oder FOCUS haben eine formal definierte, mathematisch präzise Semantik und können eine ganze Reihe erfolgreich abgeschlossener Projekte vorweisen, welche diese Notationen verwendet haben.
Einige ADLs wie etwa WRIGHT oder DARWIN haben dies ebenfalls. Die formale Notation erleichtert die widerspruchsfreie Spezifikation von Architekturen. Die Modelle werden von jedem Leser und jeder Software, welche die Notation versteht, immer gleich interpretiert.
Vorteile: Abhängig von der zugrundeliegenden mathematischen Theorie können die formalen Modelle auf bestimmte Eigenschaften hin untersucht werden. Der Sprache WRIGHT liegen beispielsweise die CSPs (Communication Sequential Processes nach Hoare) zugrunde, daher können WRIGHT Modelle auf Eigenschaften wie Verklemmungsfreiheit mit Model-Checkern untersucht werden. Bei kritischen Systemen muss häufig bewiesen werden, dass diese bestimmte Eigenschaften erfüllen oder nicht erfüllen. Über das Testen des Systems ist der Nachweis nicht möglich. Die Verwendung formaler Notationen ist hier zwingend erforderlich.
Nachteile: Das mathematische Modell, das einer formalen Notation zugrunde liegt, schränkt deren Einsatzbandbreite ein. Bestimmte Eigenschaften können gut modelliert und analysiert werden, etwa die Verklemmungsfreiheit mit WRIGHTs CSPs, andere Eigenschaften, etwa der Durchsatz können mit der mathematischen Theorie nicht oder nur schwer untersucht werden, hierfür braucht man spezielle mathematische Modelle, etwa Markov-Ketten.
Eine formale Notation ist in der Regel nicht intuitiv verständlich, insbesondere ihre Symbole und die Semantik müssen erlernt werden. Diese Aufwände sind in Entwicklungsprojekten zu berücksichtigen. Erfahrungen mit der Sprache B zeigen, dass mit Schulungsaufwänden im Bereich von 2-3 Wochen zu rechnen ist. Entsprechende Schulungen sind bei Notationen wie der UML jedoch auch erforderlich, damit diese sachgerecht eingesetzt werden.