Model-Based Verification of Security and Non-Functional Behavior using AADL
Jörgen Hansson, Bruce Lewis, Jérôme Hugues, Lutz Wrage, Peter H. Feiler, John Morley · IEEE Security & Privacy · 2009
As computer-based systems have become more complex and we continue to exploit the benefits of code generation for those systems' components or subsystems, we're finding significant integration problems due to unanticipated behavior. It isn't enough to have correct code for software components and subsystems, they must be properly integrated and correctly executed to create a fully functional system that meets its nonfunctional requirements, such as real-time performance, reliability, security, or safety. A single-source system model annotated with analysis-specific information can reflect architectural changes with little additional effort. The Architecture Analysis and Design Language (AADL) provides a platform for multidimensional model analysis and verification.