?
Комбинированное средство верификации распределённых вычислительных систем реального времени
Проверка правильности функционирования распределенных программ --- это одна из наиболее трудных и актуальных задач современного программирования. В статье описано комбинированное программно-инструментальное средство верификации распределенных вычислительных систем реального времени (РВС РВ). Для описания РВС РВ используется универсальный язык моделирования UML. Семантика диаграмм состояний UML определяется на основе модели вычислений иерархических временных автоматов. Средство верификации диаграмм UML состоит из графического редактора диаграмм состояний, средства верификации сетей конечных автоматов реального времени UPPAAL и транслятора, преобразующего диаграммы UML в сети временных автоматов. Основное внимание уделено описанию алгоритма трансляции иерархических временных автоматов в сети автоматов реального времени. Для иллюстрации предложенного подхода к верификации РВС РВ исследована задача проверки правильности функционирования системы управления дорожным движением на перекрестке.