Scalable Formal Methods for Distributed Systems

Award Information
Agency: Department of Defense
Branch: Air Force
Contract: FA9550-07-C-0118
Agency Tracking Number: F074-019-0162
Amount: $99,946.00
Phase: Phase I
Program: STTR
Awards Year: 2007
Solicitation Year: 2007
Solicitation Topic Code: AF07-T019
Solicitation Number: N/A
Small Business Information
QUALTECH SYSTEMS, INC.
100 Great Meadow Rd., Suite 603, Wethersfield, CT, 06109
DUNS: 808837496
HUBZone Owned: N
Woman Owned: N
Socially and Economically Disadvantaged: N
Principal Investigator
 Sudipto Ghoshal
 Manager, Professional Services
 (860) 257-8014
 sudipto@teamqsi.com
Business Contact
 Chakrapani Vallurupalli
Title: President & Chief Operating Officer
Phone: (860) 257-8014
Email: chuckv@teamqsi.com
Research Institution
 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
Environmental Protection Agency logo
National Aeronautics and Space Administration logo
National Science Foundation logo
US Flag An Official Website of the United States Government