Treffer: An Open Logical Programming Environment. A Practical Framework for Sharing Formal Models

The project has designed, built and tested a prototype system called a Logical Programming Environment (LPE), which provides the means to formally specify, design, verify, and optimize distributed embedded systems. The LPE has been used in increasingly complex applications, ranging from automatic code improvements for the Ensemble group communication system to the formal design of adaptive network systems and the automatic generation of coordinated contracts for BBN's Unmanned Aerial Vehicle (UAV) application. In each case, using the LPE has led to significantly increased assurance, flexibility, or efficiency of the application. In the process, substantial extensions to the LPE's logical foundations and its automated reasoning capabilities were made, thus increasing its ability to contribute to the design and implementation of reliable, reusable, reconfigurable, correct, and efficient distributed embedded systems. ; Prepared in cooperation with DARPA, Defense Advanced Research Projects Agency, Arlington, VA.