![](/jitcs/templates/ITMagazine/images/center_title_left.gif) |
М.С. Соболев "Использование логики X-CTL для формальной верификации Х-машин" |
![](/jitcs/templates/ITMagazine/images/center_title_right.gif) |
Аннотация. Приведен обзор логики CTL и ее применения для формальной верификации. Предложена логика Х-CTL, позволяющая осуществлять формальную верификацию Х-машин. Приведен пример модели-счетчика. Ключевые слова: формальная верификация, проверка моделей, Х-машина, сложные системы. Стр. 47-52.
|