Relation between session model verification and prevention of unnecessary checks in generated code

[treiher]

Context and Problem Statement

For the session model verification (#633) as well as for the prevention of unnecessary checks in the generated SPARK code (#1131), the semantics of actions must be known. The information about the necessary pre- and post-conditions of single actions is currently only known in SPARK Model (i.e., the Python representation of the generated code).

Current approach:

Specification ⇾ Model ⤵
                     SPARK Model ⇾ SPARK Code
          Integration ⤴

Use Cases

• #633
• #1131

Considered Options

O1 Analysis on SPARK Model

+ Takes integration-specific values (buffer sizes) into account − Analysis results specific to SPARK and not directly applicable to other future code generators − Mapping of errors on Model may be difficult

O2 Analysis on Model

Requires to move information about semantics of actions (like pre- and post-conditions) into the model.

+ Independent of programming language specific properties enables adding support for different code generators − Some cases cannot be detected due to missing integration-specific knowledge (buffer sizes) in Model

O3 Analysis on Intermediate Representation

New approach:

Specification ⇾ Model ⤵
                     Intermediate Representation ⇾ SPARK Model ⇾ SPARK Code
          Integration ⤴

+ Independent of programming language specific properties enables adding support for different code generators + Takes integration-specific values (buffer sizes) into account + Enables applying generic code optimizations independent of specific code generator

Decision Outcome

O3