Implementation of the AFMUC metamodel, a UML Misuse Case extension using Aspect-Oriented Modeling to modularize crosscutting security threats and mitigations. Includes the formal weaving algorithm, Coq-verified proofs, and Papyrus models based on the EU-Rent case study.
formal-methods coq-formalization threat-modeling formal-verification metamodeling aom mitigation-strategies correctness-proofs misusecase
-
Updated
Mar 29, 2026 - Rocq Prover