...
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 presentation at LADA 2012 by Robert Constable, Mark Bickford, and Vincent Rahli
- Automated Proof of Authentication Protocols in a Logic of Events by Mark Bickford
- Event Classes: abstract description of processes
- Investigating Correct-by-Construction Attack-Tolerant Systems by Robert Constable, Mark Bickford, Robbert Van Renesse
- Generating Event Logics with Higher-Order Processes as Realizers by Mark Bickford, Robert L. Constable, David Guaspari
- Component Specification Using Event Classes by Mark Bickford
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.
*Resources for EventML
**EventML documentation and downloads available at http://www.nuprl.org/software/
**EventML Tutorial
**Example of 2/3 consensus in EventML
**
Code diversity is created during the process. We During the process we can introduce variants at: Specification specification of Classesclasses, and code synthesis.
See For more details about the example below see Mark's Correct-by-Construction slides from the CRASH presentation at the May 2012 PI CRASH meeting.
More about EventML is at http://www.nuprl.org/software/ and for additional examples see the EventML Tutorial
To create correct-by-construction code we:
...
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
...