...
Code diversity is created during the process. We can introduce variants at: EventML specification of classes, and code synthesis.
For more details about the example below see Mark's presentation at the May 2012 CRASH meeting.
Methodology
To create correct-by-construction code we:
- Write the specification 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:
...
Example with Consensus
In this example we will look at Paxos consensus, focusing on specifying the Scout protocol.
...