Scalable Formal Methods for Distributed Systems

Award Information
Agency:
Department of Defense
Branch
Air Force
Amount:
$99,946.00
Award Year:
2007
Program:
STTR
Phase:
Phase I
Contract:
FA9550-07-C-0118
Award Id:
83346
Agency Tracking Number:
F074-019-0162
Solicitation Year:
n/a
Solicitation Topic Code:
n/a
Solicitation Number:
n/a
Small Business Information
100 Great Meadow Rd., Suite 603, Wethersfield, CT, 06109
Hubzone Owned:
N
Minority Owned:
N
Woman Owned:
N
Duns:
808837496
Principal Investigator:
Sudipto Ghoshal
Manager, Professional Services
(860) 257-8014
sudipto@teamqsi.com
Business Contact:
Chakrapani Vallurupalli
President & Chief Operating Officer
(860) 257-8014
chuckv@teamqsi.com
Research Institute:
UNIV. OF ILLINOIS
Kathy Young
Office of Sponsored Programs
1901 South First Street, #A
Champaign, IL, 61820
(217) 333-2187
Nonprofit college or university
Abstract
When designing distributed systems, it is necessary to compare two or more designs of the models of the system. By developing formal methods theory to automate the process of checking for differences, multiple designs can be quickly compared to come up with the best design of the system. UIUC has done research on an algorithm called Circular coinduction to automatically discover bisimulation relations and to search for the equivalence or the differences between two states. UIUC has also done research on language specification using Rewriting Logic. There is a synergy between the formal methods techniques developed at UIUC and the need for the formal methods algorithms to automate the process of comparing multi-signal models developed through TEAMS software tool at QSI. The proposed effort seeks to explore this synergy. We propose to extend the formal specification for multi-signal dependency model and research ways in which circular coinduction can be adapted for efficiently solving the equivalence-related tasks of the project. The model checking part of the project will be addressed by specifying the model in Rewriting Logic and use the generic (yet very efficient) model-checker offered by the Maude system, which fully supports Rewriting Logic specifications.

* 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

Enviromental Protection Agency logo

National Aeronautics and Space Administration logo

National Science Foundation logo
US Flag An Official Website of the United States Government