Аннотация:
Приведен обзор логики CTL и ее применения для формальной верификации. Предложена логика Х-CTL, позволяющая осуществлять формальную верификацию Х-машин. Приведен пример модели-счетчика.
Ключевые слова:формальная верификация, проверка моделей, Х-машина, сложные системы.
Полный текст:
PDF файл (258 kB)