В роботі вирішується задача розробки високонадійних систем, зокрема тих, що критичні до безпеки. Розглядаються проблеми тестування та верифікації, які актуальні на кожній стадії процесу розробки. Окрім того при розробці мають бути дотримані такі стандарти розробки систем як досяжність 100% тестового покриття та застосування технології модельного тестування для розподільних та недетермінованих систем. Пропонується вирішення проблеми з використання символьних методів на основі теорії інсерційного моделювання та предикатних перетворювачів. В якості формальних специфікацій, що визначають модель системи використовується мова Live UCM, як композиція стандартної мови UCM (Use Case Maps) та мова базових протоколів. Запропоновані методи реалізовані в низці програмних систем та апробовані на прикладах перевірки властивостей безпеки в моделях у проектах в різних галузях сучасної індустрії.
