In this paper, we will consider two aspects of UML in order to assess how well suited it is for modeling SPARK systems. The first aspect is the ability to represent SPARK in UML from a theoretical perspective. The second aspect is more from a handson perspective and evaluates what makes a UML CASE-tool more suitable for modeling SPARK systems than another. Categories and Subject Descriptors D.2.2 [Software Engineering]: Design Tools and Techniques – computer-aided software engineering (CASE), D.2.1 [Software Engineering]: Requirements/Specifications – languages. D.3.2 [Programming Languages]: Language Classifications – data-flow languages, object-oriented languages. General Terms Design, Languages Keywords SPARK, UML, Ada, profile, metamodel, INFORMED