CRASH Methodology
...
for Correct-by-construction Attack-tolerant Systems
To create correct-by-construction code we:
- Write the secification in EventML
- Automatically generate and prove an Inductive Logical Form of the specification
- Synthesize code
- Diversify and deploy code
We introduce diversity at multiple steps in the process:
- EventML specification
- Code synthesis
...