Дедуктивная верификация протокола скользящего окна

Рассматривается известный протокол скользящего окна, который обеспечивает надёжную и эффективную передачу данных по ненадёжным каналам. Формальное доказательство корректности этого протокола требует преодоления существенных трудностей, связанных с высокой степенью параллелизма, которая создаёт значительные возможности для ошибок. Здесь рассматривается версия данного протокола, основанная на выборочном повторе кадров. На языке системы верификации PVS описаны спецификация этого протокола с помощью машины состояний и его свойство безопасности. С помощью системы PVS проведено в интерактивном режиме доказательство этого свойства протокола скользящего окна.