Executable UML and SPARK Ada: The Best of Both Worlds
Ian Wilkie · Softwaretechnik-Trends · 2005
Executable UML is a well defined UML subset supported by an Action Language that enables the construction of executable models from which reliable target code can be automatically generated. SPARK Ada is a safe Ada subset with formal annotations that renders programs amenable to static analysis and formal verification. This paper describes a hybrid approach where formally annotated Executable UML (xUML) models are automatically transformed into annotated SPARK programs. The resulting programs can then be examined using existing and trusted SPARK tools in order to infer the correctness of the source UML model Motivation