UML and SysML play a central role in modern software and systems engineering. They are considered as the de facto standard for modeling software and systems. Today’s systems are created from a myriad of interacting parts that are combined to produce visible behavior. The main difficulty arises from the different ways in modeling each component and the way they interact with each other. Moreover, nowadays secure software has become an essential part in industrial development. One challenge in academia as well as in industry is to produce a secure product. Another challenge is to prove its correctness especially when the software environment is imprecise and uncertain.

The aim of this thesis is to provide a practical and formal framework that enables security risk assessment and security requirements verification on a system modeled as a composition of UML/SysML behavioral diagrams. Our main contribution is a novel approach to automatically verify security of systems on their design models based on security requirements, probabilistic adversarial interactions between potential attackers and the system’s models. These structures are shaped to provide an elegant way to define the combination between different kinds of diagrams. We rely on stochastic security templates to specify security properties and a standard catalogue of attack patterns to build a library of attacks design patterns. The result of the interaction between selected attack scenarios and the composed diagrams with the instantiated security properties are used to quantify security risk by applying probabilistic model-checker. To handle the verification process scalability, our approach allows the verification of large system efficiently by optimizing and avoiding the global model construction. To demonstrate the effectiveness of our approach, we apply our methodology on academia as well as industrial benchmarks.