Schwerpunkt dieser Dissertation ist die Implementierung und Durchsetzung von nicht-funktionalen Sicherheitseigenschaften während der Programmausführung. Konkret wird ein Entwicklungsprozess beschrieben, der sicherstellt, dass die Software die gewünschten Eigenschaften aufweist. Dieser reicht von der formalen Spezifikation über die Verifikation bis zur Durchsetzung der spezifizierten Eigenschaften zur Laufzeit. Dies ermöglicht es unerwünschtes Verhalten zu vermeiden. Diese Dissertation beginnt mit einer Studie und Klassifikation der Ansätze zur Spezifikation und Laufzeitverifikation von nicht-funktionalen Sicherheitseigenschaften. Dabei wurden folgende Beobachtungen gemacht: Erstens werden nicht-funktionale Eigenschaften während der frühen Phasen des Softwareentwicklungsprozesses weitestgehend ignoriert; sie werden meist erst berücksichtigt, wenn der funktionale Teil bereits implementiert ist was sich negativ auf die Codequalität auswirkt. Die Ansätze, die UML zur Modellierung dieser Eigenschaften benutzen, können die Widerspruchsfreiheit bezüglich der spezifizierten Eigenschaften nicht beweisen. Des Weiteren fehlt es der UML an Möglichkeiten verschiedene Arten nicht-funktionaler Eigenschaften, wie z.B. zeitbezogene Eigenschaften, auszudrücken. Zweitens, Ansätze, die das Verhalten der Anwendung zur Laufzeit beobachten und verifizieren und dadurch Verletzungen detektieren, sind im Falle kritischer Anwendungen nicht ausreichend. Solche Ansätze sollten die geforderten Eigenschaften durchsetzen und ein Systemfehlverhalten durch Unterdrücken der Ausführung unerwünschter Ereignisse vermeiden. Drittens, der Code zur Durchsetzung der nicht-funktionalen Anforderungen ist in aktuellen Ansätzen nicht gut modularisiert. Die Implementierung durchschneidet vielmehr den funktionalen Kern der Anwendung. Dieser Mangel an Modularität führt zu schwerwiegenden Problemen bezüglich der Codequalität und der Änderbarkeit der Sicherheitsanforderungen. Diese Dissertation verfolgt einen generischen, holistischen Ansatz namens Seven-pro, der formale Methoden und aspekt-orientierte Programmierung kombiniert, um nicht-funktionale Sicherheitsanforderungen sowohl zu spezifizieren als auch durchzusetzen. Seven-pro deckt den gesamten Entwicklungsprozess nicht-funktionaler Anforderungen ab und vermeidet Diskrepanzen zwischen Spezifikation und Implementierung durch das automatische Generieren von Aspekten basierend auf der Spezifikation. Die generierten Aspekte werden auf modulare Art und Weise mit dem funktionalen Kern der Anwendung integriert, um die formal spezifizierten Eigenschaften zur Laufzeit durchzusetzen. Zusätzlich zeigt diese Dissertation, wie Seven-pro verschiedene Arten von funktionalen Anforderungen im Kontext verteilter Anwendungen abdeckt. Der Ansatz wird dabei auf strukturelle, qualitative und quantitative nicht-funktionale Eigenschaften des Verhaltens angewendet. Die Arbeit präsentiert drei Anwendungen für die unterstützten Arten von Eigenschaften. Im Kontext struktureller Eigenschaften wird Seven-pro zur Spezifikation und Durchsetzung architektonischer Eigenschaften von verteilten, objekt-orientierten Anwendungen angewandt welche eine dynamische Softwarearchitektur aufweisen. Seven-pro verwendet eine Kombination aus Z-Notation und Petrinetzen zur Spezifikation (a) des Architekturstils und von Architekturinvarianten, (b) der Rekonfigurationsoptionen mit Vor- und Nachbedingung, sowie (c) der Protokolle zur Koordination der Reihenfolge der Rekonfigurationsoperationen. Ein Verifikationsschritt wird durchgeführt, um die Konsistenz der Spezifikation und den Erhalt des Architekturstils nach deren Rekonfiguration sicherzustellen. Daran anschließend werden die Z- und Petrinetzspezifikationen automatisch in AspectJ-Aspekte übersetzt, um vor jeder Rekonfigurationsoperation sicherzustellen, das alle zugehörigen Architektureigenschaften erfüllt sind. Im Kontext qualitativer Verhaltenseigenschaften wird Seven-pro eingesetzt zur Spezifikation und Durchsetzung statischer und dynamischer Aufgabentrennungs- und Delegationsrichtlinien auf Basis von rollenbasierten Zugangsbeschränkungen. Während der Spezifikationsphase wird TemporalZ, eine Kombination aus Z-Notation und linearer Temporallogik benutzt, um die unterstützten Richtlinien formal zu beschreiben. Während der Verifikationsphase werden die spezifizierten Richtlinien auf Widerspruchsfreiheit geprüft. In der Implementierungsphase wird die Aspektsprache Alpha mit einer neuen Bibliothek, die die spezifizierten Eigenschaften unterstützt, erweitert. Des weiteren werden TemporalZ-Spezifikationen automatisch in Alpha-Aspekte übersetzt, die Zugriffsrechte gemäß der spezifizierten Richtlinien beschränken. Im Kontext quantitativer Verhaltenseigenschaften wird Seven-pro zur Spezifikation und Durchsetzung zeitbezogener Eigenschaften einer Komposition von Web Services eingesetzt. Um sowohl relative als auch absolute zeitbezogene Eigenschaften zu unterstützen, wird eine neue formale Sprache mit dem Namen XTUS-Automata vorgeschlagen, die zeitbezogene Automaten um die Konstrukte der XTUS-Sprache erweitert. Nachdem sowohl die Deadlock-Freiheit als auch andere, XTUS-bezogene Eigenschaften bewiesen worden sind, werden die XTUS-Automata-Spezifikationen automatisch in AO4BPEL-Aspekte übersetzt.