Рассмотрена методика моделирования, спецификации и верификации протоколов информационных вычислительных сетей. Показан способ использования автоматной модели в качестве формальной спецификации коммуникационного протокола. Приведены свойства и соответствующие им формулы, которым должен отвечать любой протокол. Представлен способ использования автоматной модели в качестве исходной модели для метода проверки моделей (model checking). Показан фрагмент реализации модели протокола передачи. Практическим результатом работы является верификация протокола передачи с проверкой общего доступа к среде беспроводных локальных сетей (IEEE 802.11). Ключевые слова: верификация, протокол, проверка моделей, спецификация, автомат.
