Verification Work: Behavioral testing done on SysML or SCADE level?

[BerndHekele]

Sub-Task of #189.

• How to trace the results of the verification from SysML to scade?
• Scade does model checking on c-code and shows error on model level @christianstahl @MarcBehrens

[christianstahl]

Below some verification functionality provided by SCADE Suite that I am aware of (possibly incomplete):

Verification

• properties are safety properties or state properties that can be graphically specified in the SCADE language
• support of contracts (assumptions and guarantees over variables) to restrict the domain of the inputs and thus reduce the state space
• counterexamples can be loaded into the simulator for replay
• the prover is from provertechnologies (prover.com): it is a SAT checker that implements abstractions and interpolation

Testing

• specification of scenarios
• test coverage (replaces code coverage)
• certified reports can be generated
• test whether requirements are covered by tests (i.e., for each requirement, there is at least one test)
• rapid prototyper in the tool SCADE Display that can link simulation in- and outputs to graphical elements (a cockpit can be modeled that way) and that can be used for debugging and test case specification

[MarcBehrens]

• can be applied on Calculate Train Position: Verification #227
• the need to have full c2 coverage (state and transition) is identified, could you give an update here @cecilebraun