Provably Correct Code Generation
Automatically generating the
production software from a specification solves many of the problems
in system development. If correct, automated translation guarantees
that the behavior of the production code is consistent with the
formal specification. There are several commercial systems
that are based on this idea and translate a formal or semi-formal
specification to executable code, for instance, Statemate from
I-Logix, the Rose tools from Rational Corporation, and SCADE from
Verilog.
There are, however, various reasons to
distrust code generated from a formal or semi-formal specification.
First, the translation process may not be formal: the specification
and/or target language may not have formal semantics, the
translation may not be formally defined, and the code generator may
not transparently implement the formal translation. Second,
the code may not be traceable back to the original specification.
Third, the generated code may not be suitable for the environment:
it may be too inefficient, or not match the traceability/readability
standards required for the project.
We are attempting to generate
production code that can be trusted and is efficient enough to be
used in most safety-critical domains. Our approach is based on the
denotational semantics of both RSML-e (Requirements
State Machine Language without Events) and a simplified imperative
target language (SIMPL). The semantics are used to prove that
the translator correctly implements the RSML-e
semantics in SIMPL. SIMPL is a subset of several imperative
languages (for example, C, C++, and Ada) so that we can trivially
map our generated code to several imperative languages. SIMPL also
has a much smaller semantics than commercial imperative languages,
so it is easier to use in the translation proofs.
We intend to use the code generator in
both research and industrial systems to investigate the following
questions:
-
How difficult is it to provide a
complete formalization of the code-generation process?
-
What is the worst-case execution
time of the generated code, and is it sufficient for a broad
variety of safety-critical applications?
-
Which provably-correct
optimizations provide the largest benefit to the worst-case
execution time? How do they affect
traceability/readability?
-
Is it possible to split an RSML-e
specification into communicating subtasks to improve performance
and processor utilization? Can formal correctness
arguments for the generated code be provided?
As far as we are aware, no code-generation approach from a formal
specification language provides a completely formal basis for
translation. Our approach will yield a full formalization of the
translation process. We believe that generating non-optimized,
easily readable and traceable code is sufficient for a variety of
safety-critical systems. For applications with more stringent
time deadlines, provably-correct optimizations can dramatically
improve performance and still provide a high degree of traceability
and readability from the specification. |
