Анотація. Описано новий генератор символьних трас, розроблений для останньої версії системи інсерційного моделювання. Основними характеристиками цього генератора є використання графічного представлення опису багаторівневих моделей, поділ локальних описів і відносини слідування, можливість настроювання на різні стратегії пошуку.
Ключові слова: верифікація, інсерційне моделювання, мова UCM.
Летичевский Александр Адольфович,
академик НАН Украины, профессор, заведующий отделом Института кибернетики им. В.М. Глушкова НАН Украины, Киев,
e-mail: let@cyfra.net; let@iss.org.ua; aaletichevsky78@gmail.com.
Летичевский Александр Александрович,
кандидат физ.-мат. наук, старший научный сотрудник Института кибернетики им. В.М. Глушкова НАН Украины, Киев,
e-mail: lit@iss.org.ua.
Песчаненко Владимир Сергеевич,
кандидат физ.-мат. наук, доцент Херсонского государственного университета
e-mail: lvladim@ksu.ks.ua.
Губа Антон Андреевич,
младший научный сотрудник Института кибернетики им. В.М. Глушкова НАН Украины, Киев,
e-mail: anton.huba@iss.org.ua.