You are here
Scalable Formal Methods for Distributed Systems
Title: Manager, Professional Services
Phone: (860) 257-8014
Email: sudipto@teamqsi.com
Title: President & Chief Operating Officer
Phone: (860) 257-8014
Email: chuckv@teamqsi.com
Contact: Kathy Young
Address:
Phone: (217) 333-2187
Type: Nonprofit College or University
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. *