search

openETCS / validation

WP4: Validation and verification strategy
8 stars 22 forks source link

Strategic Work: write verification for transformations #188

Open BerndHekele opened 10 years ago

BerndHekele commented 10 years ago

The item needs grooming.
The following table gives an overview on usecases and owners of the use-case.

from / to SysML System- Scade B Petri-Nets Scade C-Code System-C
SysML - [1] @astante [2], @MERCEmentre Laas via System-Scade @peleska @Alexn84 [3]
System-Scade [4] - [5]
B [6] - provided by ClearSy
Petri-Nets ? -
Scade via System Scade [7] @christianstahl [8] - inside evaluation pending by URO
C-Code ? -
System-C ? already C++ -

Footnotes: 4 Already existing but additional files appear here 1 Here the consistency checks are needed within the Eclipse ValidationFramework #192 5 Already existing and provided by ESTEREL 3 via Acceleo 6 @astante : Would be an additional task #192 8 Behavioral properties: Only message flows are considered and transform SCADE (lustre) to petri nets using abstraction techniques 7 Back propagation is planned to be released by ESTEREL 2 Reduced scope of behavioral model

astante commented 10 years ago

There are some errors in the table. The entry "provided by ClearSy" belongs to the C-Code column. The entry "already C++" belongs to the column C-Code. Also the entry "inside" belongs to the column "C-Code".

Could you also please add @MERCEmentre the the SysML to B Transformation part?

MERCEmentre commented 10 years ago

In addition to SysML to B transformation, can you add @MERCEmentre to SysML to C transformation?