The TA-9 SPARK Ada code generator can, at one level, be regarded as simply an Ada 95 code generator but it does much more than just produce executable target code to implement user xUML models. It also implements the Praxis SPARK approach to software production whereby safety, security and quality are assured through static code analysis and partial proof of correctness.
Developed in collaboration with the UK Atomic Weapons Establishment (AWE), TA-9 is targeted at safety and mission critical systems where code quality is of paramount importance.
Like all of Abstract Solutions' code generators, TA-9 generates 100% of the code necessary to implement the platform independent xUML model, including the transformation of actions specified in ASL into SPARK Ada.
The SPARK Ada 95 Language
SPARK Ada is a subset of the Ada 95 language. A valid SPARK program can always be successfully compiled and deployed using any Ada 95 compiler.
The SPARK subset avoids potentially unsafe constructs in the Ada language and reinforces type safeness in the code. In addition, the SPARK language includes formal annotations (captured as Ada comments) that make static declarations about the nature of the code that can then be checked by static analysis and proof tools.
For example, SPARK annotations allow users to specify what each module in a program does in terms of access to global data and transformations of inputs to outputs. This specification applies transitively so that higher-level modules are specified in terms of their overall effect, including the action of any lower level modules called therein.
The SPARK examiner can then statically verify that the actual Ada in the modules does what the specification states.
Combined with a development process that emphasises up-front specification of the design before implementation of module internals, this approach means that analysis can show that the program meets its specification.
SPARK annotations and tools can also be used to provide proof of absence of run time errors. Specifically, they can be used to prove to a very high level of confidence that a program will never generate an Ada exception (aside from Storage Errors).
Refining a program to the point where a high level of proof is achieved will often uncover many subtle errors in the code, many of which may not otherwise be caught, even by exhaustive testing.
Finally, use of pre and post conditions on modules can allow users to prove important properties of the system. If chosen carefully these properties may be used to reinforce safety and security arguments.
The Hybrid xUML/SPARK Approach
TA-9 supports a hybrid approach where users can apply a similar approach of up-front specification of the xUML models by adding SPARK-like annotations early in the development process. These annotations perform the same functions as the SPARK annotations but refer to xUML model elements rather than SPARK language constructs.
The TA-9 code generator then takes the (annotated) model and generates not only the functional SPARK Ada that implements the model but also the SPARK annotations that describe the code. These generated annotations are produced from a combination of the transformation of the user created annotations in the xUML model and knowledge of the generated SPARK Ada that implements the model and the xUML formalism.
The resulting annotated SPARK code is then submitted to the static examiner and proof tools. Problems uncovered by these tools can then be traced back to the original model.
This hybrid approach makes the full power of SPARK accessible through high level UML modelling. Users can annotate the model without having to understand the intricacies of how SPARK requires annotations to be placed in source code. This leaves the user free to concentrate on specifying the data actions of the model while TA-9 supplies the repetitive detail defined by the structure of the model.
This automated support also means that the manual annotation load on the system developer does not increase so fast as the system size grows.
TA-9 supports full data and information flow analysis of the models as well as proof of absence of run time errors.
If code generated from an annotated model can be successfully run through the static analysis and proof tools then this shows that not only does the model correctly implement the behaviour described by the user-written annotations but that the TA-9 code generator has successfully preserved the meaning of both the annotations and the model when transforming them to SPARK.
The Generated SPARK Code
TA-9 takes a xUML model and generates 100% of the code necessary to implement it as a single Ada program running as a single Ada Task.
All memory allocation is static and users make use of the tagging mechanisms within iUML Modeller to specify the necessary instance population sizes.
Using TA-9, xUML models can be run in either sequential or interleaved mode and can be easily integrated with legacy code if required.
Platform Support
TA-9 generates standard Ada 95 and so can, in principle, be run on any platform supporting that language. At the lowest levels of the xUML models, interfaces to hardware or users may require the inclusion of platform specific Ada packages.
However, with the exception of the xUML timer mechanism, there is no need for users to adapt any of the run time aspect of TA-9 to different platforms.
TA-9 is developed and tested using the GNAT compiler on the Microsoft Windows platform and is integrated with AdaCore's GNAT Programming Studio
Variants
TA-9 is supplied in two variants:
- The Portable Variant provides the TA-9 code generator and the source code of the run time support files. This enables users to port a TA-9 generated application to any platform that supports Ada 95.
- The Adaptable Variant provides the same capability as the Portable Variant but also includes the iCCG source models that were used to create the code generator. This enables users to change any aspect of the code generation or SPARK annotation transformation.