Рассматриваются формальная спецификация и автоматизированная верификация систем обработки транзакций, используемых в распределенных базах данных. В таких системах стандартный набор свойств ACID должен быть обеспечен комбинацией протоколов контроля параллелизма и восстановления. В существующей литературе такие протоколы обычно изучаются раздельно, и проблема их взаимодействия нередко игнорируется. Для изучения формальной верификации комбинированного набора протоколов мы специфицируем систему обработки транзакций, интегрирующих строгое двухфазное блокирование, протокол восстановления undo/redo и двухфазное атомарное завершение. Мы доказали с помощью интерактивного доказывателя теорем PVS, что в нашей системе выполняются свойства атомарности, долговечности и сериализуемости. Ключевые слова: базы данных, протоколы контроля параллелизма, протоколы восстановления, отказоустойчивость, формальная спецификация, автоматизированная верификация, интерактивный доказыватель теорем
