Одной из важных задач проектирования реактивных алгоритмов является обеспечение правильности исходной спецификации алгоритма, a точнее, требований к его функционированию. Это может быть достигнуто только путем формальнойверификации необходимых свойств алгоритма. Задача верификации состоит в том,чтобы показать, что модель верифицируемой системы обладает заданным свойством корректности ее поведения. Верификация предполагает наличие формальной модели алгоритма и языка для задания проверяемых свойств. B качестве модели алгоритма рассматривается его спецификация в логическом языке. При этом специфицирyeмый алгоритм представляется в виде двух частей: управляющей иоперационной, взаимодействующих между собой и c внешней средой. Логическаяспецификация алгоритма определяет описание его управляющей части и тех аспектов операционной части и внешней среды, которые относятся к взаимодей-ствню управляющей и операционной частей между собой и c внешней средой.Таким образом, логическая спецификация алгоритма состоит из трех частей: спе-цификаций управляющей части, операционной части и внешней среды. B качествематематической модели каждой части спецификации рассматривается конечный автомат. Составляющие части алгоритма удобно специфицировать как неинициальные системы, отдельно задавая начальное условие, определяющее начальные состояния соответствующих автоматов.
展开▼
