М.С. Соболев "Использование логики X-CTL для формальной верификации Х-машин"
Аннотация.
Приведен обзор логики CTL и ее применения для формальной верификации. Предложена логика Х-CTL, позволяющая осуществлять формальную верификацию Х-машин. Приведен пример модели-счетчика.
Ключевые слова:
формальная верификация, проверка моделей, Х-машина, сложные системы.
