ИСТИНА

Язык UML предназначен для моделирования широкого класса систем, поэтому в его стандарте намеренно не фиксирована семантика. Однако для формальной проверки свойств модели необходимо строго задать синтаксис и семантику всех используемых элементов диаграмм состояний. В данной работе задаются дополнительные ограничения на структуру диаграмм состояний и синтаксис выражений и, таким образом, устраняется неоднозначность интерпретации элементов диаграмм. Транслятор диаграмм UML в автоматы UPPAAL получает на вход диаграмму состояний в распространённом формате XMI. После преобразования диаграммы во внутреннее представление непосредственная трансляция осуществляется в два этапа. Сначала диаграмма переводится в промежуточное представление – иерархический временной автомат (HTA) [1], затем этот автомат преобразуется в сеть временных автоматов в соответствии с алгоритмом, основанным на методе из работы [1]. Алгоритм трансляции HTA в сеть временных автоматов UPPAAL последовательно обрабатывает все композитные состояния от корня к листьям, транслируя каждое из них в отдельный процесс в сети временных автоматов. Этот процесс содержит состояние, соответствующее неактивности исходного композитного состояния в HTA, состояния, соответствующие всем вложенным состояниям, и служебные состояния, использующиеся для синхронизации работы всех автоматов посредством передачи сообщений и изменения значений служебных переменных. Алгоритм существенно изменен по сравнению с описанием в [1], в частности, добавлены фрагменты алгоритма, пропущенные в [1] и добавлена возможность широковещательной посылки. Для проверки работы алгоритма была использована модель системы реального времени, описанная подробно в [2]. Авторы этой статьи построили вручную модель на UPPAAL для данной системы и проверили для нее некоторые свойства. Мы построили иерархическую модель системы перекрестка на UML вместо менее компактной и более трудной для восприятия плоской модели из [2] и получили модель на UPPAAL с помощью транслятора автоматически. В результаты верификации полученной автоматической трансляцией системы временных автоматов все свойства из [2] были успешно проверены.