Мы представляем алгоритмы автоматической верификации распределенных систем реального времени по их формально-логической спецификации методом MASL. Предложенные алгоритмы основаны на так называемом принципе символьной верификации (symbolic model checking), как и соответствующие алгоритмы для логик ветвящегося времени CTL и альтернированного времени ATL. Алгоритмическая сложность решения задачи верификации для случая MASL с фиксированной внешней средой ограничена полиномом от длины спецификации и мощности множества состояний и действий системы. Для случая MASL с неопределенной внешней средой, задача верификации разрешима за полиномиальное время от размера модели, но имеют экспоненциальную сложность относительно структуры спецификации среды.
Original languageRussian
Pages (from-to)65-74
JournalВЕСТНИК САНКТ-ПЕТЕРБУРГСКОГО УНИВЕРСИТЕТА. СЕРИЯ 1: МАТЕМАТИКА, МЕХАНИКА, АСТРОНОМИЯ
Volume1
Issue number3
StatePublished - 2007
Externally publishedYes

ID: 5157391