Building Event Structures over Higher-Order Processes as Realizers
Speaker: Bob Constable , Cornell
Date: May 7 2010
Time: 1:00PM to 2:30PM
Location: 32-G575
Host: Nancy Lynch, MIT
Contact: Rotem Oshman, rotem@csail.mit.edu
Relevant URL: Using a constructive Logic of Events based on Computational Type Theory (CTT) we have been able to formally specify safety and liveness properties for distributed protocols and synthesize executable code from constructive proofs in Nuprl that the specifications are realizable. We have used this proofs-as-processes method to build fault-tolerant protocols, adaptive protocols, and provably secure protocols. Recently we have created versions of Paxos this way.
This system development capability is based on a constructive semantics for assertions in our "standard" Logic of Events using the concept of event structures from Winskel which are defined over executions of process in the standard model of asynchronous message passing computation. This semantics is expressed in CTT in such a way that proof terms contain distributed realizers.
These realizers are state machines similar to IOA which can easily be compiled into appropriate programming languages such as Java, Erlang, F#, etc. Critical to the practical success of this methodology is the use of programmable event classes to specify computing tasks at a high level of abstraction that can be refined automatically to processes.
In 2010 we substantially extend this synthesis/verification/development method so that it applies to a very general notion of process of the kind used in process algebras (e.g. the higher-order pi-calculus, Petri nets, CCS, CSP, etc.) as well for the standard process model used in the Logic of Events mentioned above, e.g. the standard textbook model for systems courses.
Our generalization enables the synthesis of correct-by-construction processes over a wide variety of process models by extracting them as distributed realizers for specifications event logic. I will lecture about this new model.
See other events that are part of Theory of Distributed Systems 2010/2011
See other events happening in May 2010
