...
Our method uses formal proofs of high-level system requirements then synthesizes code from the proofs. Within our method we use the following concepts:
Wiki Markup Logic of Events: a simple formal theory of mathematical structure corresponding to message sequence diagrams \[http://www.nuprl.org/documents/Bickford/LOE-LADA2012.html\]
- Event Classes: abstract description of processes
The main tool we use is EventML which is a programming and specification language. EventML, built by Vinvent Rahli, cooperates with the Nuprl interactive theorem prover at every stage of program development to help programmers ensure correctness, document the code, and support modifications and improvements. It generates an Inductive Logical Form that proves the specification and can also automatically synthesize code.
During the several steps of the process (state machine code synthesis) we can introduce variants at: Specification of Classes, and code synthesis.
See Mark's Correct-by-Construction slides from the CRASH May 2012 PI meeting.
...
Using EventML's interface with Nuprl, we generate the ILF. If there are any issues with the proof we revise the specification and reiterate the process with the ILF.
Step 3 - Synthesize Consensus Code
...