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.