Elan: The Event Logic Assistant

Abstraction has been the most reliable means for gaining intellectual control of complex problems and for extending the scope and scale of our analytical abilities. In the past several years, ATC-NY and Cornell University have developed the formalism of {\em event logic\/}to support specification and reasoning about distributed systems at a very high level of abstraction and the refinement of specifications to a level of abstraction from which it is possible to generate code. ``Bare'' event logic requires extensive interactive theorem-proving by an expert user. We will develop {E}lan: The Event Logic Assistant, to provide a systematic way to apply event logic with a high degree of automation. Users formalize requirements in the ``high-level core'' of event logic, express distributed algorithms as ``information flow constraints,'' and derive implementations by solving the constraints. They will apply the {E}lan automated tool suite to prove that the constraints imply the requirements and to solve the constraints. Preliminary experiments suggest that these proof engines can be based on SAT solvers and model checkers. In Phase I we will prototype two tools: an automated prover for the high-level core event logic, and a translator from temporal logic into event logic to enable modelchecking of constraints.