Scalable Formal Methods for Distributed Systems

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.