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

• Verification of session model #633
• Prevent unnecessary checks in session states #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 (#1204)

[treiher]

The design and implementation of the intermediate representation will be tracked in #1204.