You are here

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
Solicitation Topic Code: AF07-T019
Solicitation Number: N/A
Timeline
Solicitation Year: 2007
Award Year: 2007
Award Start Date (Proposal Award Date): 2007-09-11
Award End Date (Contract End Date): 2008-06-11
Small Business Information
100 Great Meadow Rd., Suite 603
Wethersfield, CT 06109
United States
DUNS: 808837496
HUBZone Owned: No
Woman Owned: No
Socially and Economically Disadvantaged: No
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
United States

 (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. *

US Flag An Official Website of the United States Government