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. The project investigates a hybrid approach where formally annotated Executable UML 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.
A code generator that implements the translation has been developed using Abstract Solutions’ iCCG product and is described in a presentation by Sam Moody of AWE made at the Safety Critical Systems Club.