Atomic Weapons Establishment

Abstract Solutions has been working with AWE (the UK Atomic Weapons Establishment) on a research project to investigate the advantages and practicability of a combined system development approach using Executable UML and SPARK Ada.

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.

More details of the approach can be found in papers from Ian Wilkie of Abstract Solutions and Damian Curtis of AWE.

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.

Abstract Solutions is proud to work with the following companies