Аннотация.Описан новый генератор символьных трасс, разработанный для последней версии системы инсерционного моделирования. Основными характеристиками генератора являются использование графического представления описания многоуровневых моделей, разделение локальных описаний и отношения следования, возможность настройки на различные стратегии поиска, применение нового предикатного трансформера, допускающего кванторы общности с ослабленными ограничениями относительно предыдущих версий.
Ключевые слова: верификация, инсерционное моделирование, язык 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.