High-integrity code generation for state-based formalisms

We are attempting to create a translator for a formal state-based specification language (RSML^-e) that is suitable for use in safety-critical systems. For such a translator, there are two main concerns: the generated code must be shown to be semantically equivalent to the specification, and it must be fast enough to be used in the intended target environment. We address the first concern by providing a formal proof of the translation, and by keeping the implementation of the tool as simple as possible. The second concern is addressed through a variety of methods: decomposing a specification into parallel subtasks; providing provably-correct optimizations; and making worst case performance guarantees on the generated code