Formale Methoden zur Analyse der Informationssicherheit von Softwaresystemen werden durch die Theorie der Information Flow Security bereitgestellt, mit deren Hilfe sich unautorisierte Informationsflüsse bereits im Entwurf auffinden lassen. Aufgrund spezifischer Eigenschaften von cyber-physischen Systemen sind diese theoretischen Grundlagen in der Praxis jedoch nicht direkt anwendbar. Daher werden in dieser Arbeit formale Methoden der Information Flow Security in einen modellgetriebenen Entwicklungsansatz für cyber-physische Systeme integriert. Zunächst wird eine Spezifikationstechnik für das disziplinübergreifende Systems Engineering um Sicherheitsrichtlinien erweitert, durch die sich Sicherheitsanforderungen bereits in einer frühen Entwicklungsphase dokumentieren und validieren lassen. Weiterhin wird ein Regelwerk für die Verfeinerung der Richtlinien im Kontext komponentenbasierter Softwarearchitekturen vorgestellt, deren Komponenten durch Nachrichtenaustausch kommunizieren. Diese Regeln befähigen Softwarearchitekten dazu, aus den verfeinerten Richtlinien einzelner Systemkomponenten Schlüsse über die Sicherheit des Gesamtsystems zu ziehen. Auf dieser Grundlage wird eine Verifikationstechnik vorgestellt, mit der sich die Einhaltung der Richtlinien durch das Echtzeitkommunikationsverhalten der Komponenten automatisch prüfen lässt. Hierdurch lassen sich selbst subtile Flüsse auffinden, bei denen Informationen aus den Zeitpunkten der ausgetauschten Nachrichten abgeleitet werden könnten. Da mehrere dieser Beiträge auf der Transformation von Modellen basieren, wird abschließend ein Ansatz zur Reduzierung des Entwicklungsaufwandes solcher Transformationen vorgestellt. Dadurch werden Entwickler befähigt, Teile einer deklarativen Transformation automatisch zu inferieren sowie die Ausführung durch imperative Anweisungen zu verfeinern.

The theory of information flow security provides formal methods for security analyses of software systems, enabling engineers to detect unauthorized information flows in the design phase. However, due to specific characteristics of cyber-physical systems, these theoretical foundations are not directly applicable to the engineering in practice. In this thesis, we extend the scope of applicability by integrating formal methods for information flow security into a model-driven engineering approach for cyber-physical systems. Initially, we enhance a discipline-spanning specification technique for systems engineering by introducing a notion of security policies, which enable systems engineers to document and validate security requirements at an early stage of development. Next, we propose a body of rules for the refinement of security policies in the context of component-based software architectures, whose constituent components communicate asynchronously by message passing. Our rules enable software architects to draw conclusions about the security of a composite system from the security policies of its constituent components. On this basis, we provide software engineers with an automated technique to verify that the real-time communication behavior of individual components adheres to their refined security policies. By conducting a time-sensitive analysis, our verification technique even allows for the detection of subtle flows in which information is deducible from the timing of messages. Finally, since several of our contributions are based on transformations of models, we present an approach for reducing the verbosity of such transformations and the associated development effort. In particular, we enable developers to infer parts of a declarative transformation automatically and to refine its execution by means of imperative instructions.