Верификация распределённых систем с применением Isabelle/HOL

Мы ежедневно пользуемся распределёнными системами (в форме интернет-сервисов). Эти системы очень полезны, но и реализовывать их непросто, так как сети непредсказуемы. Всякий раз, когда вы передаёте сообщение по сети, предполагается, что оно прибудет очень быстро, но возможны и достаточно долгие задержки. Может случиться так, что сообщение не прибудет вообще, либо прибудет несколько раз. Когда вы отправляете запрос другому процессу и не получаете отклика, вы понятия не имеете, что произошло: потерялся ли запрос, либо тот другой процесс аварийно завершился, либо сам отклик потерялся? Или же на самом деле ничего не потерялось, сообщение просто задержалось и ещё может прибыть. Невозможно доподлинно узнать, что произошло, поскольку ненадёжный обмен сообщениями – единственный способ межпроцессной коммуникации.