Построение формальной модели Т-системы и исследование ее корректности

В статье исследуются методы распараллеливания программ, применяемые в Т-системе -средстве автоматического динамического распараллеливания вычислительных приложений. Отличительная особенность Т-системы от аналогичных средств -ориентация на программы, написанные на широко распространенных языках C, C++. В работе построена формальная модель для базовых конструкций Т-системы с помощью операционного подхода. В рамках модели доказывается корректность используемых механизмов. Разработанная модель была положена в основу новой реализации Т-системы.