SCorES, A Logical Programming Environment for Distributed Systems

Award Information
Agency: Department of Defense
Branch: Air Force
Contract: FA9550-04-C-0106
Agency Tracking Number: F045-023-0029
Amount: $99,993.00
Phase: Phase I
Program: STTR
Awards Year: 2004
Solicitation Year: 2004
Solicitation Topic Code: AF04-T023
Solicitation Number: N/A
Small Business Information
ATC - NY
33 Thornwood Drive, Suite 500, Ithaca, NY, 14850
DUNS: 101321479
HUBZone Owned: N
Woman Owned: N
Socially and Economically Disadvantaged: N
Principal Investigator
 David Guaspari
 Staff Scientist
 (607) 257-1975
 davidg@atc-nycorp.com
Business Contact
 Richard Smith
Title: Controller
Phone: (607) 257-1975
Email: rick@atc-nycorp.com
Research Institution
 Cornell University
 Daniel B Whitaker
 Office of Sponsored Programs, 120 Day Hall
Ithaca, NY, 14853
 (607) 255-5337
 Nonprofit college or university
Abstract
Distributed systems, important to civilian and military infrastucture, have steadily become more complex and steadily more difficult to understand, implement, and maintain. Addressing these dangers, a collaboration between ATC-NY and Cornell University will build a mathematically based tool, SCorES, providing powerful automated support for specifying, developing, verifying, and synthesizing real-time distributed systems at a high level of abstraction. Mathematical techniques for modeling and analyzing distributed systems are difficult to use because they are insufficiently abstract. SCorES supports abstract methods that are "declarative" (rather than operational) and "constructive". Declarative methods permit systems to be specified, analyzed, developed, and verified at a conceptual level congenial to human designers. Constructive methods permit automatic code synthesis. The key is to define a "logic" for this new domain, so all development steps become logical inferences. Work by Cornell and ATC-NY has already defined a logic appropriate for the class of distributed systems that can be specified and modeled without reference to quantitative real time. This logic has specified and derived demonstrably correct nontrivial distributed algorithms (e.g., consensus protocols). We will extend our methods to hybrid systems, including variables that evolve in continuous time and implement SCorES by encoding these methods within the NuPRL logical environment.

* information listed above is at the time of submission.

Agency Micro-sites

SBA logo
Department of Agriculture logo
Department of Commerce logo
Department of Defense logo
Department of Education logo
Department of Energy logo
Department of Health and Human Services logo
Department of Homeland Security logo
Department of Transportation logo
Environmental Protection Agency logo
National Aeronautics and Space Administration logo
National Science Foundation logo
US Flag An Official Website of the United States Government