Информационные системы и технологии МАТЕМАТИЧЕСКОЕ И ПРОГРАММНОЕ ОБЕСПЕЧЕНИЕ ВЫЧИСЛИТЕЛЬНОЙ ТЕХНИКИ И АВТОМАТИЗИРОВАННЫХ СИСТЕМ УДК 004.021; 519.711 В.А. БАШКИН ВЕРИФИКАЦИЯ НА ОСНОВЕ МОДЕЛЕЙ С ОДНИМ НЕОГРАНИЧЕННЫМ СЧЕТЧИКОМ Предлагается новый метод доказательства свойств систем, моделируемых при помощи односчетчиковых сетей Петри (параллельных и распределенных процессов, алгоритмов и протоколов). <...> Подобные модели позволяют представлять системы как с конечными, так и с бесконечными множествами состояний. <...> Проверяемые свойства предлагается записывать при помощи формул теморальной логики EF (логики достижимости). <...> Новизна метода состоит в использовании некоторых конструктивных теоретико-числовых свойств бесконечной части одномерных линейных и полулинейных множеств. <...> Представлен алгоритм формальной верификации темпоральных формул логики EF, использующий декомпозицию формулы и вычисления над однопериодическими полулинейными базисами специального вида. <...> A new method is presented for verification of systems, modeled by one-counter Petri nets (parallel and distributed processes, algorithms and protocols). <...> It is proposed to formulate the checked property by EF-formula (where EF is a temporal logic of reachability). <...> В случае параллельных и распределенных систем возникают дополнительные критические свойства, связанные с возможностью возникновения нескольких независимых потоков вычислений: максимальная и минимальная степени параллелизма, неизбежность синхронизации после распараллеливания и т.д. <...> Одним из классических способов формализованного анализа систем является верификация моделей (model checking) [5]. <...> Метод состоит в том, что вначале строится математическая модель системы, адекватно отражающая важные аспекты её структуры (например, диаграмму переходов управляющего устройства), а также формулируется математическое утверждение, описывающее нужное свойство (например, отсутствие тупиков). <...> Для описания проверяемых свойств обычно используют формулы, заданные посредством различных темпоральных логик. <...> Например <...>