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.