Probabilistic Verification, Temporal Logic, Probabilistic Automata, Security Properties, Attack Pattern, Vulnerability Detection, Risk Assessment, UML, SysML, Activity Diagrams.