Process Extraction in an Abstract Logic of Events

April 13, 2006
Bob Constable | Cornell University, Professor & Dean of CIS

In 2003 Mark Bickford and I defined and formalized a logic of events for specifying distributed computing tasks and for reasoning about distributed systems. The Logic of Events is a very abstract account of distributed computing that applies to biological processes as well as to processes in an asynchronous message passing network computing model.

Although the logic is very abstract, we can show that it is “not too abstract” in the sense that from constructive proofs that tasks are achievable, we can extract abstract distributed systems. Mark and his colleague David Guaspari have translated this abstract code, called Message Automata, into Java and we would like to translate to C# as well.

The logic naturally formalizes the intuitive language of events and message sequence diagrams that designers of distributed systems use. It supports a specification language for distributed tasks that complements Spec#.

Speaker Details

Dean Robert Constable continues to head a large research group in automated reasoning and software system verification. He is known for his work connecting programs and mathematical proofs, which has led to new ways of automating the production of reliable software. Dean Constable has written three books on this topic as well as numerous research articles. As a graduate PhD student at Princeton University, he worked with Alonzo Church, one of the pioneers of computer science. You can find more information about his research at http://www.cs.cornell.edu/Info/Projects/NuPrl/