Formal Methods in Concurrent and Distributed Systems

点击翻译按钮获取中文摘要

With the increased complexity of distributed and concurrent programs, it becomes necessary to use formal methods to reason about such systems. This entails new research on using temporal logics and state transition systems to reason about concurrent programs. The problem of proving properties of systems of processes communicating through message channels that may lose or duplicate messages is investigated. New methods for automatically verifying properties of such systems specified in different temporal logics are proposed. Part of the research will be directed towards developing algorithms for verifying real-time properties of finite state concurrent programs specified in a branching time temporal logic. New formalisms for specifying real-time behavior of finite-state processes will be investigated. In addition, new methods for proving correctness of concurrent programs with respect to specifications given by, possibly finite state, nondeterministic automata will be explored. Research on fault-tolerance in distributed systems will focus on developing new algorithms for achieving fault-tolerance through roll back recovery in distributed systems. Specifically, efficient algorithms that tolerate arbitrarily spaced crash failures as well as application specific recovery procedures will be investigated.