Методы исследования свойств высокопроизводительных инфраструктур. Обзор

Представлен аналитический обзор современных методов верификации программного обеспечения параллельных и распределенных систем. Описаны методы верификации на основе исследования свойств конечных автоматов, сетей Петри и транзиционных систем....

Ausführliche Beschreibung

Gespeichert in:

Bibliographische Detailangaben
Datum:	2015
Hauptverfasser:	Бойко, Ю.В., Глибовец, Н.Н., Ершов, С.В., Крывый, С.Л., Погорилый, С.Д., Ролик, А.И., Теленик, С.Ф., Куляс, А.И., Крак, Ю.В., Ясочка, М.В.
Format:	Artikel
Sprache:	Russian
Veröffentlicht:	Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України 2015
Schriftenreihe:	Управляющие системы и машины
Schlagworte:	Фундаментальные и прикладные проблемы информатики и информационных технологий
Online Zugang:	https://nasplib.isofts.kiev.ua/handle/123456789/87174
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!
Назва журналу:	Digital Library of Periodicals of National Academy of Sciences of Ukraine
Zitieren:	Методы исследования свойств высокопроизводительных инфраструктур. Обзор / Ю.В. Бойко, Н.Н. Глибовец, С.В. Ершов, С.Л. Крывый, С.Д. Погорилый, А.И. Ролик, С.Ф. Теленик, А.И. Куляс, Ю.В. Крак, М.В. Ясочка // Управляющие системы и машины. — 2015. — № 1. — С. 3–13. — Бібліогр.: 16 назв. — рос.

Institution

Digital Library of Periodicals of National Academy of Sciences of Ukraine

id	nasplib_isofts_kiev_ua-123456789-87174
record_format	dspace
spelling	nasplib_isofts_kiev_ua-123456789-871742025-02-23T19:41:16Z Методы исследования свойств высокопроизводительных инфраструктур. Обзор Methods for Investigating Properties of High-performance Infrastructures. The review Бойко, Ю.В. Глибовец, Н.Н. Ершов, С.В. Крывый, С.Л. Погорилый, С.Д. Ролик, А.И. Теленик, С.Ф. Куляс, А.И. Крак, Ю.В. Ясочка, М.В. Фундаментальные и прикладные проблемы информатики и информационных технологий Представлен аналитический обзор современных методов верификации программного обеспечения параллельных и распределенных систем. Описаны методы верификации на основе исследования свойств конечных автоматов, сетей Петри и транзиционных систем. Представлено аналітичний огляд сучасних методів верифікації програмного забезпечення паралельних та розподілених систем. Описано методи верифікації на основі дослідження властивостей скінченних автоматів, мереж Петрі та транзиційних систем. An analytical survey of the modern verification methods of reactive and distributed systems is presented. The verification methods founded based on investigation properties of the finite state automata, Petri nets and the transition systems are described. 2015 Article Методы исследования свойств высокопроизводительных инфраструктур. Обзор / Ю.В. Бойко, Н.Н. Глибовец, С.В. Ершов, С.Л. Крывый, С.Д. Погорилый, А.И. Ролик, С.Ф. Теленик, А.И. Куляс, Ю.В. Крак, М.В. Ясочка // Управляющие системы и машины. — 2015. — № 1. — С. 3–13. — Бібліогр.: 16 назв. — рос. 0130-5395 https://nasplib.isofts.kiev.ua/handle/123456789/87174 51.681.3 ru Управляющие системы и машины application/pdf Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України
institution	Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection	DSpace DC
language	Russian
topic	Фундаментальные и прикладные проблемы информатики и информационных технологий Фундаментальные и прикладные проблемы информатики и информационных технологий
spellingShingle	Фундаментальные и прикладные проблемы информатики и информационных технологий Фундаментальные и прикладные проблемы информатики и информационных технологий Бойко, Ю.В. Глибовец, Н.Н. Ершов, С.В. Крывый, С.Л. Погорилый, С.Д. Ролик, А.И. Теленик, С.Ф. Куляс, А.И. Крак, Ю.В. Ясочка, М.В. Методы исследования свойств высокопроизводительных инфраструктур. Обзор Управляющие системы и машины
description	Представлен аналитический обзор современных методов верификации программного обеспечения параллельных и распределенных систем. Описаны методы верификации на основе исследования свойств конечных автоматов, сетей Петри и транзиционных систем.
format	Article
author	Бойко, Ю.В. Глибовец, Н.Н. Ершов, С.В. Крывый, С.Л. Погорилый, С.Д. Ролик, А.И. Теленик, С.Ф. Куляс, А.И. Крак, Ю.В. Ясочка, М.В.
author_facet	Бойко, Ю.В. Глибовец, Н.Н. Ершов, С.В. Крывый, С.Л. Погорилый, С.Д. Ролик, А.И. Теленик, С.Ф. Куляс, А.И. Крак, Ю.В. Ясочка, М.В.
author_sort	Бойко, Ю.В.
title	Методы исследования свойств высокопроизводительных инфраструктур. Обзор
title_short	Методы исследования свойств высокопроизводительных инфраструктур. Обзор
title_full	Методы исследования свойств высокопроизводительных инфраструктур. Обзор
title_fullStr	Методы исследования свойств высокопроизводительных инфраструктур. Обзор
title_full_unstemmed	Методы исследования свойств высокопроизводительных инфраструктур. Обзор
title_sort	методы исследования свойств высокопроизводительных инфраструктур. обзор
publisher	Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України
publishDate	2015
topic_facet	Фундаментальные и прикладные проблемы информатики и информационных технологий
url	https://nasplib.isofts.kiev.ua/handle/123456789/87174
citation_txt	Методы исследования свойств высокопроизводительных инфраструктур. Обзор / Ю.В. Бойко, Н.Н. Глибовец, С.В. Ершов, С.Л. Крывый, С.Д. Погорилый, А.И. Ролик, С.Ф. Теленик, А.И. Куляс, Ю.В. Крак, М.В. Ясочка // Управляющие системы и машины. — 2015. — № 1. — С. 3–13. — Бібліогр.: 16 назв. — рос.
series	Управляющие системы и машины
work_keys_str_mv	AT bojkoûv metodyissledovaniâsvojstvvysokoproizvoditelʹnyhinfrastrukturobzor AT glibovecnn metodyissledovaniâsvojstvvysokoproizvoditelʹnyhinfrastrukturobzor AT eršovsv metodyissledovaniâsvojstvvysokoproizvoditelʹnyhinfrastrukturobzor AT kryvyjsl metodyissledovaniâsvojstvvysokoproizvoditelʹnyhinfrastrukturobzor AT pogorilyjsd metodyissledovaniâsvojstvvysokoproizvoditelʹnyhinfrastrukturobzor AT rolikai metodyissledovaniâsvojstvvysokoproizvoditelʹnyhinfrastrukturobzor AT teleniksf metodyissledovaniâsvojstvvysokoproizvoditelʹnyhinfrastrukturobzor AT kulâsai metodyissledovaniâsvojstvvysokoproizvoditelʹnyhinfrastrukturobzor AT krakûv metodyissledovaniâsvojstvvysokoproizvoditelʹnyhinfrastrukturobzor AT âsočkamv metodyissledovaniâsvojstvvysokoproizvoditelʹnyhinfrastrukturobzor AT bojkoûv methodsforinvestigatingpropertiesofhighperformanceinfrastructuresthereview AT glibovecnn methodsforinvestigatingpropertiesofhighperformanceinfrastructuresthereview AT eršovsv methodsforinvestigatingpropertiesofhighperformanceinfrastructuresthereview AT kryvyjsl methodsforinvestigatingpropertiesofhighperformanceinfrastructuresthereview AT pogorilyjsd methodsforinvestigatingpropertiesofhighperformanceinfrastructuresthereview AT rolikai methodsforinvestigatingpropertiesofhighperformanceinfrastructuresthereview AT teleniksf methodsforinvestigatingpropertiesofhighperformanceinfrastructuresthereview AT kulâsai methodsforinvestigatingpropertiesofhighperformanceinfrastructuresthereview AT krakûv methodsforinvestigatingpropertiesofhighperformanceinfrastructuresthereview AT âsočkamv methodsforinvestigatingpropertiesofhighperformanceinfrastructuresthereview
first_indexed	2025-11-24T18:06:40Z
last_indexed	2025-11-24T18:06:40Z
_version_	1849696033822474240
fulltext	УСиМ, 2015, № 1 3 Фундаментальные и прикладные проблемы информатики и информационных технологий УДК 51.681.3 Ю.В. Бойко, Н.Н. Глибовец, С.В. Ершов, С.Л. Крывый, С.Д. Погорелый, А.И. Ролик, С.Ф. Теленик, А.И. Куляс, Ю.В. Крак, М.В. Ясочка Методы исследования свойств высокопроизводительных инфраструктур. Обзор Представлен аналитический обзор современных методов верификации программного обеспечения параллельных и распределенных систем. Описаны методы верификации на основе исследования свойств конечных автоматов, сетей Петри и транзиционных систем. An analytical survey of the modern verification methods of reactive and distributed systems is presented. The verification methods founded based on investigation properties of the finite state automata, Petri nets and the transition systems are described. Представлено аналітичний огляд сучасних метод1в верифікації програмного забезпечення паралельних та розподілених систем. Описано методи верифікації на основі дослідження властивостей скінченних автоматів, мереж Петрі та транзиційних систем. 1 Ключевые слова: верификация, конечные автоматы, транзиционные системы, сети Петри, верификация на моделях. Введение. Представлен обзор результатов, по- лученных как авторами, так и другими иссле- дователями в области создания надежного про- граммного и технического обеспечения для вы- сокопроизводительных инфраструктур. В ча- стности описаны методы анализа семантичес- ких свойств моделей систем реактивного и рас- пределенного типов. Выбор этих направлений объясняется тем, что в настоящее время в об- ласти проектирования, разработки и внедрения развиваются и активно применяются именно такого типа системы [1–8]. Анализ семантических свойств систем со- стоит в разработке анализаторов, которые, по- лучая на входе в качестве входных данных ин- формацию о системе, выдают на выходе отве- ты на вопросы о ее свойствах. Сложность ре- шения такой проблемы связана как с алгорит- мической неразрешимостью общей проблемы анализа, так и со сложностью самого процесса анализа. Поэтому такие ответы неизбежно бу- дут частичными, но и они всегда очень суще- ственны. Одним из подходов к частичному решению проблемы такого анализа есть иссле- дование свойств математических моделей ре- альных систем формальными методами. Ос- новными математическими моделями служат транзиционные системы, автоматные, сетевые и логико-алгебраические модели. В связи с алгоритмической неразрешимо- стью общей проблемы анализа, он возможен на разного рода аппроксимациях структур, вхо- дящих в семантические спецификации иссле- дуемых объектов. На практике эта методоло- гия может быть применена в процессе разра- ботки иерархии семантик и иерархии абст- рактных алгебр, а также логических языков на разных уровнях абстракции. Цель такой мето- дологии – создание средств такой семантиче- ской системы анализаторов, которая (по воз- можности) автоматически выполняла бы ана- лиз спецификаций. Транзиционные системы и их произве- дения Одной из наиболее общих математических моделей разного рода систем являются тран- зиционные системы. Посредством этой модели исследуются многие свойства реальных парал- лельных и распределенных систем. Определение 1. Транзиционной системой (ТС) называется пятерка A = (S,T,,,s0), где S – множество состояний, Т – множество пере- ходов между состояниями,  : T  S – функция начала перехода,  : T  S – функция конца перехода, s0  S – начальное состояние ТС. 4 УСиМ, 2015, № 1 Графически ТС изображается в виде оргра- фа, вершины которого соответствуют состоя- ниям, а дуги – переходам ТС. Пример 1. Рассмотрим две ТС. Рис. 1 В первой из приведенных ТС A (S  = 0 1 2 3 1 2 3 4 0{ , , , }, { , , , }, , , )s s s s T t t t t s    , где функ- ции  и  задаются графом этой ТС. В частно- сти, 1( )t = 0s , 1( )t = 1s , 5( )t = 3s , 5( )t = 0s . Множество переходов T можно рассматри- вать как алфавит, а конечную или бесконеч- ную последовательность переходов этого ал- фавита называть транзиционным словом или просто словом переходов. Множество всех слов в алфавите Т будем обозначать F(T). Если Tt  , то тройка ( ( ), , ( ) )t t t  назы- вается шагом вычислений в ТС A = (S, T, , , s0). Состояние s  S называется достижимым с помощью перехода t  T, если существует Ss  такое, что (s, t, s') – шаг вычислений в ТС A. Слово )(...21 TFttt k  называется вы- числением в A 0( , , , , )S T s   , если существу- ет последовательность состояний ksss ,...,, 21 такая, что ),,( 1 iii sts  есть шаг вычислений для каждого {1, 2, , }i k  . Добавим к множе- ству переходов Т пустой переход  , который будет обозначать отсутствие перехода из со- стояния s  S. Если 1 2, , , ( )kt t t F T – вы- числение в ТС, то говорят, что оно начинается в состоянии s0 и ведет в состояние sk. Вычис- ление называется историей, если оно стартует в начальном состоянии s0. Слово 1 2... ( )t t F T бесконечной длины называется бесконечным вычислением в ТС, если существует беско- нечная последовательность состояний 1 2 ...i is s такая, что ),,( 1 jj iji sts  – шаг вычислений в ТС для каждого ij  1, и бесконечной историей, если 1 0is s . Если h – история, ведущая в состояние s, а с – вычисление, начинающееся в состоянии s, то конкатенация hc тоже есть история. В этом случае говорят, что hc – расширение истории h с помощью вычисления с. Синхронное произведение ТС. Пусть A1, A2, …, An – ТС, где Ai 0( , , , , )i i i i iS T s   , A i  A j  , если ji  , i, j = 1, 2, ..., п. Определение 2. Ограничением синхрониза- ции называется подмножество Т множества 1 2( { }) ( { }) ... ( { }) \{ , ,..., }nT T T            , где  – тождественный переход. Элементы множества Т называются гло- бальными переходами. Если t = 1 2{ , , , }nt t t  T и it   , тo говорят, что ТС A i принимает уча- стие в переходе t. Кортеж А = (A1, A2, …, A n, Т) называется произведением ТС A1, A2, …, A n над множе- ством Т, а ТС A1, A2, …, A n – компонентами А. На рис. 1 показано произведение ТС1 и ТС2, определяемое множеством глобальных пере- ходов 1 2 3 2 4 2 5 1 3{( , ),( , ),( , ),( , ),( , ),( , ),( , )}t t t u t u t u u     T (см. пример 1). Глобальным состоянием А = (A1, A2,…, An, Т) называется n-ка 1 2( , ,..., )ns s s , где ii Ss  , а со- стояние 1 2 0 0 0( , ,..., )ns s s – начальным состоянием A. Шагом вычисления А называется тройка (s, t, s'), где s = 1 2( , ,..., )ns s s и s' = 1 2( , ,..., )ns s s   – глобальные состояния, a t 1 2( , ,..., )nt t t – гло- УСиМ, 2015, № 1 5 бальный переход, удовлетворяющий следую- щим условиям: {1, 2, ..., }i n   если it   , то ( )i is t  и ( )i is t   ;  если it   , то ii ss  . Глобальный переход t называется допусти- мым в глобальном состоянии s, если суще- ствует глобальное состояние s' такое, что (s, t, s') – шаг вычисления. Последовательность глобальных переходов t1, t2, ..., tk,... называется глобальным вычисле- нием, если существует последовательность глобальных состояний s0, s1, ..., sk такая, что (si–1, ti, si) – шаг вычислений для каждого },...,2,1{ ki . В этом случае говорят, что гло- бальное вычисление начинается в глобальном состоянии s0 и ведет в глобальное состояние sk. Глобальное вычисление, которое начинается в состоянии s0, называется глобальной историей вычисления. Пример 2. Рассмотрим произведение ТС на рис. 1. Начальное глобальное состояние – ),( 00 rs . Глобальным вычислением будет по- следовательность 1 1 3 2( , ), ( , ), ( , ),t u t u  посколь- ку три шага вычислений 0 0 1(( , )( , ),s r t  1 0( , )),s r 1 0 1 1 1(( , )( , ), ( , )),s r u s r 1 1 3 2(( , )( , ),s r t u 3 2( , ))s r составляет вычисление, ведущее из состояния ),( 00 rs в состояние ),( 23 rs . Рис. 2 Последовательность 1 3 1( , ), ( , )t t u не будет глобальным вычислением, поскольку переход ),( 13 ut не есть глобальным переходом из Т. Многие свойства произведения ТС можно исследовать путем его моделирования сетями Петри [8]. Сети Петри и представление ТС Сети Петри (СП). Сетью называется трой- ка (Р, Т, F), где Р и Т непересекающиеся мно- жества, элементы которых называются мес- тами и переходами соответственно, a F  ( ) ( )P T T P    – отношение инцидентно- сти. Элементы из F называются стрелками, а места – вершинами, подразумевая графическое представление сети. Если Fyx ),( , то х на- зывается входной вершиной у, а у – выходной вершиной х. Множества входных и выходных вершин для х обозначаются x и x соответ- ственно. Сеть (Р, Т, F) называется размеченной, если задана функция разметок NPM : , где N – множество натуральных чисел. Если М(р) = m, то это значит, что функция М ставит в верши- ну р ровно m фишек. Разметка сети в случае, когда P n и множество Р упорядочено, представляется вектором 1 2( , , ..., )nM m m m , где )( ii pMm  , Ppi  , i = 1, 2, ... , п. Сетью Петри называется четверка (P, T, F, W, М0), где (P, T, F) – сеть, М0 – начальная разметка ее мест, a }0{\: NFW  – функция кратности дуг СП. Необходимость введения функции кратно- сти дуг объясняется тем, что место и переход или переход и место могут быть связаны не одной, а несколькими дугами. Если в СП все дуги имеют кратность 1, то такая СП называ- ется ординарной. Заметим, что имеется алго- ритм, с помощью которого произвольная СП может быть преобразована в ординарную СП [9]. Такую СП будем обозначать четверкой (Р, Т, F, М0) и далее, если не оговорено про- тивное, под СП будем понимать ординарную сеть. Переход Tt СП может сработать при разметке М, если она размечает каждое вход- ное место этого перехода, т.е. Mt  . В этом 6 УСиМ, 2015, № 1 случае разметка М называется допустимой для перехода t. Если М допустима для t, то этот переход может сработать и привести к новой разметке М'   ttM })\{( . Разметка М' получается из разметки М путем удаления одной фишки из каждого входного места и добавления одной фишки в каждое выходное место перехода t. Переход от М к М' обозначается так: MM t  . Говорят, что разметка М' дости- жима из разметки М, если существует последо- вательность переходов 1 2, , , nt t t из Т таких, что n tttt MMMM n ...321 21 . Разметка М' называется просто достижи- мой, если она достижима из начальной раз- метки 0M СП. СП как математическая модель вычислений хорошо изучены и поэтому полезно моделиро- вание ТС с помощью СП. Представление произведения ТС с помо- щью СП. СП (P, T, F, M0) представляет произ- ведение А = (A1, A2, …, A n, Т) ТС Ai = (Si, Ti, i, 0, )i i s , где Ai  A j  при ji  , i, j = 1, 2, ... , п, если P = ,...2 ni SSS  T = T, F = ={( , ) is t  t и ( )} {( , )i i is t s t    t и s = ( )}i it  для некоторого i{1, 2, ... , n}, где it обозначает i-ю компоненту t  Т, 1 0 0( ,M s 2 0 0,..., )ns s . Пример 3. СП, представляющая произведе- ние ТС (см. рис. 1), имеет вид (рис. 2). В этой СП имеем 2 1( , ) { }t s   , 2( , )t   2{ },s 4 2 2 1( , ) { , }t u s r  и },{),( 2324 rsut  . Далее будем использовать обозначения { ( ) }i i it t    t и { ( ) }i i it t    t . Заметим, что семантика произведения ТС и семантика СП, представляющие его, согласу- ются в том смысле, что последовательность глобальных переходов t1, t2, ..., tk будет гло- бальной историей произведения ТС А тогда и только тогда, когда она – допустимая последо- вательность срабатываний переходов в СП. Представление произведения ТС в виде СП позволяет исследовать свойства этого произ- ведения методами анализа хорошо развитых свойств СП. Классы СП и их свойства. Рассмотрим классификацию СП и методы исследования их важнейших свойств. Для этого введем некото- рые определения общего характера. Определение 3. Место р СП называется ограниченным, если существует такое число kN, что для произвольной достижимой раз- метки М в СП выполняется неравенство М(р)  k. СП называется ограниченной, если каждое ее место ограничено. Место р СП называется безопасным, если для произвольной достижимой разметки М этой СП М(р)  1. СП называется безопасной, если все ее места безопасны. Пара (p, t) ((t, p)) – место р и переход t – в СП называется местом–полуциклом (перехо- дом–полуциклом), если место р (переход t) – как входное, так и выходное место (переход) для перехода t (места р). Пусть для некоторой СП (Р, Т, F, W, М0) имеется подмножество PQ  и Q . Множество Q называют дедлоком (сифоном) тогда и только тогда, когда  QQ , и ло- вушкой тогда и только тогда, когда QQ  . Очевидно, что множество всех разметок в СП конечно тогда и только тогда, когда СП ограничена. Матрица инцидентности и уравнение со- стояния. Для СП (S, W, M0) с п переходами и т местами матрицей инцидентности А назы- вается матрица с целочисленными коэффици- ентами размерности пт, элементы которой определяются уравнением ( , ) ( , ),i j j i i ja I t p I p t  где i – отношение инцидентности данной СП. Справедливость этого уравнения вытекает из правила сохранения фишек, поскольку коэф- фициент ija матрицы инцидентности пред- ставляет число фишек, которые перемещают- УСиМ, 2015, № 1 7 ся, изменяются и добавляются в место pi при срабатывании перехода tj в СП. Поскольку j-я строка в матрице инцидентно- сти А означает смену разметки в результате сра- батывания перехода tj можно записать урав- нение, называемое уравнением состояния СП: ,0 dMMxA k  (1) где k = 1, 2, ..., а А – матрица инцидентности СП, х – вектор срабатывания переходов, Мk – фи- нальная разметка, а М0 – начальная разметка СП. Система уравнений (1) называется также необходимым условием достижимости раз- метки Мk из начальной разметки М0. Известно, что когда разметка Мk достижима из начальной разметки М0, то система (1) всегда имеет ре- шение. Обратное утверждение, к сожалению, не всегда корректно. Но из необходимого ус- ловия достижимости разметки вытекает доста- точное условие недостижимости заданной разметки в СП. Это следует из правила кон- трапозиции. Заметим, что решения системы (1) ищут в множестве натуральных чисел N. Для решения такого типа систем разработано не- сколько алгоритмов [3, 6, 7, 16]. Все эти алго- ритмы принадлежат классу временной слож- ности NP [11, 14] и проблема построения более эффективных алгоритмов для таких систем ос- тается актуальной. Анализ структурных свойств СП. Рас- смотрим классы СП, в частности, так называе- мые чистые СП и методы анализа их струк- турных свойств. Последние – это свойства, не зависящие от начальной разметки СП в том смысле, что они выполняются для ее произ- вольной начальной разметки. Определение 4. СП (S, W, М0) называется чистой, если из ( , )p t F вытекает Fpt ),( или   tt (т.е. СП не содержит мест– полуциклов). К структурным свойствам чистых СП отно- сятся следующие свойства: структурная жи- вучесть, управляемость, структурная ограни- ченность, консервативность и частичная кон- сервативность, повторяемость и частичная повторяемость, непротиворечивость и час- тичная непротиворечивость. Методы анализа этих свойств зависят от класса СП, для которых они исследуются. Классификация СП выполняется путем введе- ния определенных ограничений на места и пе- реходы СП. Определение 5. Пусть (Р, Т, F, W, М0) – СП, удовлетворяющая условиям, PpTt  , })1,0{),(),,(( ptItpI . СП (P, T, F, W, M0) на- зывается: машиной состояний (МС) 1;t T t t     синхрографом (СГ) 1  ppPp ; СП свободного выбора (СВ) ,p p   (P p ( 1))p p p p p            ; расширенной СП свободного выбора (РСВ) , ( ( ));p p P p p p p p p             простой СП (ПСП) , (p p P p p      ( 1 1 ))p p p p           ; асимметричной СП (АСП) ,p p   ( ( )).P p p p p p p p p                Для этих классов СП справедливы следую- щие факты. Теорема 1. 1) СП свободного выбора струк- турно жива тогда и только тогда, когда ка- ждый ее дедлок имеет ловушку. 2) Если СП (S, W, M0) с т местами полно- стью управляема, то rank (AT) = т, где А – мат- рица инцидентности СП. 3) СП (S, W, М0) структурно ограничена то- гда и только тогда, когда, система 0 xA , х > 0 несовместна над N или, что то же самое, система 0 yAT , у > 0, имеет хотя бы одно решение в N. 4) СП (S, W, М0) (частично) консервативна тогда и только тогда, когда система 0 xA , х > 0 (х  0), несовместна над N или, что то же 8 УСиМ, 2015, № 1 самое, система 0 yAT имеет хотя бы одно решение у > 0 (у  0) над N. 5) СП (S, W, М0) (частично) повторяема то- гда и только тогда, когда система 0 xA имеет хотя бы одно решение х > 0 (х  0) над N. 6) СП (S, W, М0) (частично) непротиворе- чива тогда и только тогда, когда система 0 xA имеет хотя бы одно решение х > 0 (х  0) над N. S- и Т-инварианты и ограниченность. Введенное уравнение состояния СП, которое имело вид системы линейных диофантовых уравнений над множеством натуральных чи- сел N: ,0 xAMM d  (2) где M0, Md – начальная и конечная разметки СП соответственно, а А – матрица инцидент- ности этой СП, позволяет ввести понятия ин- вариантов СП. Определение 6. Решение х системы 0 xA (т.е. когда в выражении (2) М0 = Md) называется Т-инвариантом СП, а решение системы AT  y = 0 называется S-инвариантом СП (или Р-инвариантом). Инварианты СП – полезное средство при исследовании ее структурных свойств. Это вы- текает из таких утверждений. Пусть дана неко- торая СП с т местами и п переходами. Теорема 2. 1) Вектор у размерности т есть S-инвариант СП тогда и только тогда, когда yMyM TT 0 для произвольной фиксирован- ной начальной разметки М0 и произвольной достижимой разметки М. 2) Вектор х размерности п есть Т-инвариант СП тогда и только тогда, когда существует разметка М0 и последовательность срабатыва- ния переходов , ведущая от М0 к М0, такие, что  = х. Из теоремы 1 п. 3 о структурной ограничен- ности чистых СП вытекает, что существует век- тор у такой, что 0 yA . Но тогда существует х 0 такой, что xAMM  0 и 0 T TM y M y  + T Tx A y . Поскольку 0yAT , то yMyM TT 0 и, следовательно, ),(/)()( 0 pyyMpM T (3) где у(р) означает р-ю компоненту вектора у. Полученное неравенство дает верхнюю оцен- ку для числа фишек, которые укладываются в место р. Эта граница может быть улучшена, если в неравенстве (3) используются все S-ин- варианты из минимального порождающего мно- жества S-инвариантов. Поскольку инварианты СП служат векторами, то минимальность век- торов рассматривается над множеством нату- ральных чисел N, т.е. вектор у называется мини- мальным, если не существует другого вектора 1y такого, что )()(1 pypy  для всех мест р. Определение 7. Порождающее множество S-инвариантов (Т-инвариантов) называется ми- нимальным порождающим множеством S-ин- вариантов (Т-инвариантов), если не существу- ет ни одного непустого его подмножества, которое тоже – порождающее. Из теории систем линейных уравнений из- вестно, что TSS-алгоритм [12] находит мини- мальное порождающее множество решений та- кой системы и для ее нахождения можно при- менить этот алгоритм. Таким образом, неравенство (3) редуциру- ется к виду 0( ) min / ( ) ,T i iM p M y y p    (4) где минимум ищем на всем множестве S-инва- риантов из минимального порождающего мно- жества. В работе [13] сказано, що данную оценку улучшить невозможно ни для каких других инвариантов. Инвариантам СП отводится существенная роль в исследовании свойства ограниченности. Определение 8. Говорят, что СП покрыва- ется позитивными S-(T)-инвариантами тогда и только тогда, когда для произвольного места ip (перехода it ) существует S-(T)-инвариант у такой, что iy > 0 для всех i = 1, 2, ..., \| Р \|. УСиМ, 2015, № 1 9 Связь между ограниченностью и инвариан- тами СП выражается такими утверждениями [2, 13]. Теорема 3. 1) Если все места СП покрыва- ются позитивными S-инвариантами, то она ог- раничена. 2) Если существует S-инвариант 0y , у которого компонента 0iy , то место ip ог- раничено, т.е. существует такое натуральное число k, что для произвольной разметки М, достижимой из начальной разметки, справед- ливо неравенство kpM i )( . 3) Если СП ограничена и живая, то она по- крывается позитивными Т-инвариантами. 4) Если СП ограничена и переход it в СП живой, то существует Т-инвариант 0x , у которого компонента 0ix . Поиск дедлоков и ловушек в СП. Рас- смотрим метод анализа живучести СП с по- мощью дедлоков и ловушек, который бази- руется на использовании диофантовых огра- ничений. Напомним, что когда произвольный пере- ход имеет выходное место, принадлежащее дедлоку Q, то в него следует включать и его выходное место. А для ловушки наоборот. Из этого определения вытекает, что когда дедлок Q есть пустое множество, то он всегда оста- ется таковым в процессе функционирования СП. Для ловушки ситуация противополож- ная: если хотя бы одно ее место получило фишку, то ловушка постоянно остается не- пустым множеством в процессе функциони- рования СП. Дедлоки и ловушки можно найти в СП пу- тем решения системы логичных уравнений, описывающих эти свойства, или эквивалент- ной ей системы линейных уравнений над мно- жеством {0,1} [13]. Ловушка называется помеченной началь- ной разметкой, если хотя бы одно место этой ловушки получает по крайней мере одну фишку. Необходимость построения множеств дед- локов и ловушек для данной СП состоит в том, что посредством анализа полученных множеств можно исследовать свойство живучести СП. Это вытекает из такого утверждения. Теорема 4. СП свободного выбора как и расширенная СП свободного выбора живая тогда и только тогда, когда каждый дедлок этой СП содержит ловушку, помеченную на- чальной разметкой М0. При использовании СП для верификации свойств систем существенным будет определе- ние пути, ведущего к ошибке или к подозри- тельному месту, или переходу в СП. Этот путь скрыт в Т-инвариантах, поскольку они содержат информацию только о том, какие переходы сра- ботали, но не несут никакой информации о по- следовательности их срабатывания. Если уста- новлено, что СП ограничена, то граф достижи- мых разметок такой СП есть конечным автома- том. Применяя к этому автомату алгоритм ана- лиза, построим регулярное выражение, а по нему определим кратчайшие пути, ведущие в подоз- рительные места СП. Первая группа свойств СП проверяется средствами линейной алгебры, в частности, средствами решения систем линейных дио- фантовых уравнений и неравенств в области натуральных чисел. Эта группа средств базируется на оригиналь- ном методе построения минимального порож- дающего множества решений систем линейных уравнений в области натуральных чисел. Этот метод решения назван ТSS-методом [3]. С по- мощью этого алгоритма генерируются инвари- анты СП без какой-либо дополнительной обра- ботки. Использование этого алгоритма позволя- ет решить проблему достижимости в подклассе СП свободного выбора; недостижимости раз- метки в общем случае; ограниченности СП для единственного ее места; вычисления ловушек и дедлоков СП; структурных свойств для дан- ной СП. Вторая группа средств базируется на хоро- шо разработанных алгоритмах построения, представления и обхода графов [10]. Третья группа тоже имеет хорошую алго- ритмическую поддержку в виде алгоритмов 10 УСиМ, 2015, № 1 анализа и преобразования регулярных языков и регулярных выражений [5]. Перейдем к рассмотрению методов вери- фикации свойств систем логико-алгебраичес- кими средствами и средствами конечных ав- томатов. Анализ свойств реактивных систем Реактивной называется система, которая должна потенциально работать бесконечно. Методы верификации таких систем основаны на проверке на модели и некоторых ее разно- видностях. Неформально суть этого метода состоит в следующем. Ожидаемые свойства реальной системы описываются в виде формул некоторого формального логического языка, а реальная система моделируется соответст- вующей ТС или произведением ТС. Верифи- кация состоит в проверке выполнимости за- данных формул на модели [1, 8]. Одним из по- пулярных логических языков есть язык линей- ной темпоральной логики (LTL – linear tempo- ral logic). Язык линейной темпоральной логики. Множество LTL-формул над заданным множе- ством атомарных формул АР определяется ин- дуктивно: – каждая атомарная формула есть LTL-фор- мулой, – если  LTL-формула, то  и X LTL- формулы, – если ,  LTL-формулы, то  и  U есть LTL-формулы. LTL-формулы интерпретируются над беско- нечными словами, символами которых явля- ются множества атомарных формул, т.е. бес- конечными словами в алфавите В(АР), где В(АР) – булеан множества атомарных формул АР. Интуитивно это означает, что некоторое множество атомарных формул, соответствую- щих исследуемому базисному утверждению, выполняется в i-й момент времени. Пусть  – LTL-формула и бесконечное слово 0 1 2...x x x  , где ix В(АР) для каждого 0i . Обозначение ╞  означает, что слово  вы- полняет  или удовлетворяет . Отношение вы- полнимости ╞ определяется индуктивно: пусть р АР и 1... i i ix x   – суффикс слова , тогда ╞ р, если 0xp , ╞  , если  не выполняет , ╞  , если ╞  или ╞ , ╞ X , если 1 ╞ , ╞ , U если 0 nn   ╞  и (0 ) ii i n    ╞ . Формула X читается как  в следующий момент, a U – как  пока не . Другими словами, X выполняется в данный момент времени, если в следующий момент будет вы- полняться , а U выполняется в данный мо- мент времени, если формула  выполняется в данный момент или она будет выполнена в бу- дущий момент времени, а в каждый момент времени до этого момента, выполняется фор- мула . Остальные логические связки вводятся обычным путем: true = p p для любого рАР, false =  true, = ,  R = = ( )  U , F = true U и G = false R . Пример 4. Пусть АР = {р} и даны LTL-фор- мулы ( )p p G X и )( pp XF  над алфа- витом АР ={р} атомарных формул. Первая формула читается как всегда, если р выполня- ется в данный момент времени, то в сле- дующий момент она не выполняется, а вто- рая формула – существует два последова- тельных момента времени, когда формула р выполняется. Пусть ( 0)p  и 00 (0)pp  обозначают два бесконечных слова вида: 000 ppp ... и 00pp000... соответственно. На этих словах получаем: ( 0)p  ╞ ( )p p G X , 00 (0)pp  не вы- полняет ( )p p G X , ( 0)p  не выполняет )( pp XF  , 00 (0)pp ╞ )( pp XF  . Интерпретация LTL-формул на произве- дении ТС. Пусть имеется произведение ТС УСиМ, 2015, № 1 11 А = (A1, A2, …, A n, Т), где Ai 0( , , , , )i i i i iS T a   , i = 0,1,..., п. Базисными утверждениями будут такие текущим локальным состоянием i-й ком- поненты является ai. Следовательно, множе- ством атомарных формул выбирается множе- ство  n i iSAP 1  . Пусть задана бесконечная глобальная исто- рия h = t1, t2, t3, ... произведения А, тогда суще- ствует единственная последовательность гло- бальных состояний 0 1 2a a a  такая, что 0a – начальное состояние, a (ai, ti+1, ai+1) – шаг вы- числений в А для каждого 0i . Иными сло- вами, 0 1 2a a a  – последовательность со- стояний, которые проходят во время выпол- нения h. Бесконечная последовательность ( ) h множеств атомарных формул определяется так: для каждого 0i i-й элемент ( ) h представляет собой множество локальных со- стояний глобального состояния ai (т.е. мно- жество локальных состояний компонент произведения ТС в i-й момент времени). Из определения шага вычисления следует, что если iS и 1iS соответственно i-й и (i + 1)-й элемент ( ) h , то    iiii ttSS )\(1 . Пример 5. Рассмотрим произведение ТС, показанных на рис. 3 [8]. LTL-формулы стро- ятся над алфавитом АР = },,,{ 1010 uutt и пусть Т={ ( , ), ( , )a b   a b , ( , )}c c . Рис. 3 Последовательность h = abc(ab)ω – беско- нечная история. Последовательность глобаль- ных состояний, появляющихся во время вы- полнения, будет такой: 0 0 0 1 0 0 1 0 1 1( , )( , )( , )(( , )( , ))t u t u t u t u t u  , т.е. ( ) h = 0 0 0 1 0 0 1 0 1 1( , )( , )( , )(( , )( , ))t u t u t u t u t u  . Теперь можно определить интерпретацию LTL-формулы  на (h). Будем говорить, что произведение А выполняет формулу  (обо- значение А╞ ), если каждая бесконечная ис- тория произведения А выполняет . Другими словами, произведение А выполняет формулу , если все ее бесконечные истории выполня- ют формулу . Проблема проверки выполнимости на моде- ли состоит в определении для заданных произ- ведения А и LTL-формулы , выполнима или нет формула  на А. Как и в случае историй, видим, что для данной бесконечной -истории 1 2, ,  t t существует единственная последовательность 0 1, ,r r -состояний такая, что  1, ,i i ir t r есть -шагом произведения А для каждого 1i . Обозначим эту последовательность    и назовем ее -последовательностью . В этом случае говорят, что  выполняет  и обозна- чают это ╞ , если ( )  ╞ . Проверка LTL-свойств. Эта проблема име- ет несколько эквивалентных формулировок. Проверка того, что все бесконечные истории произведения А выполняют LTL-формулу  эквивалентна тому, что существует некоторая бесконечная история, которая не выполняет , а это, в свою очередь, эквивалентно тому, что существует некоторая история, которая выпол- няет  . Таким образом, при рассмотрении бесконечных историй, выполняющих некото- рое свойство, как язык слов бесконечной дли- ны в алфавите AP , проблема выполнимости сводится к проблеме проверки пустоты неко- торых такого типа языков. В данном случае тестер свойств произведе- ния А рассматривает А как механизм, распо- знающий язык L слов бесконечной длины со- ответствующих -историям, и бесконечным историям произведения А. Следовательно, по- 12 УСиМ, 2015, № 1 лучаем такую процедуру проверки выполни- мости формулы : а) построить тестер, распознающий язык 1L всех -историй, выполняющих  ; б) используя этот тестер и его произведение с тестером языка L всех -историй, построить тестер, допускающий язык 1LL ; в) проверить равенство  1LL ; если оно выполняется, то формула  выполняется на всех бесконечных -историях, иначе на некоторой выполняется  (и эта история дает контрпример). Такого типа тестеры известны – это автома- ты Бюхи и обобщенные автоматы Бюхи, назы- ваемые также автоматами Мюллера [5, 16]. Тестер для LTL-формул называют Бюхи-тес- тером или просто тестером для произведения А. Тестер – это тройка вида BT = (B, F, ), где B = 0( , , , , )S T a  – транзитивная система, SF  – множество заключительных состоя- ний и :T  T – функция отметок, сопос- тавляющая каждому переходу B некоторый глобальный переход из Т произведения А. Тес- тер BT воспринимает бесконечные последова- тельности t1t2t3... T , если существует беско- нечная история ...321 uuuh  в B и заключитель- ное состояние Fa такое, что ( )i iu t для каждого 1i и на истории h состояние а по- является бесконечно часто. Это значит, что по- следовательность ( )h содержит бесконечно много вхождений состояния а. Язык, который воспринимается BT, состоит из слов T . Пусть  – LTL-формула. Тестер BT проверя- ет выполнимость формулы  или служит тес- тером свойства , если он воспринимает все бесконечные -истории А, которые выполня- ют . Существует огромная литература по про- блеме проверки на модели и большое число различных конструкций для такого типа про- верки. Здесь будет рассмотрена одна из самых простых конструкций. Построение Бюхи-тестера часто выпол- няется в два этапа: сначала строится обобщен- ный Бюхи-тестер для заданной LTL-формулы , а затем этот тестер преобразуется в Бюхи- тестер для этой формулы. Обобщенным Бюхи-тестером для А называ- ется кортеж BT = (B, {F0, F1; ..., Fk–1}, ), где B,  такие же, как и в определении Бюхи-тестера, a F0, F1; ..., Fk–1 – множество подмножеств за- ключительных состояний. B воспринимает бес- конечную последовательность t1t2t3... T , если существует бесконечная история 1 2 3, , ,a a ah  и заключительные состояния 1 0 2 1, ,a F a F   1, k ka F  такие, что ( )i iu t для каждого 1i и каждое состоя- ние 1, , ka a входит в h бесконечное число раз. Язык называется распознаваемым или до- пускаемым тестером BT, если каждое слово этого языка допускается этим тестером. Сравнение с логическим подходом к анали- зу свойств систем показывает, что: – некоторые свойства могут быть выражены ТС и СП более естественно и проще, чем в ло- гических формализмах; – некоторые свойства (ограниченность, воз- можность возврата к начальному состоянию, оп- ределение дедлоков и ловушек) вовсе не могут быть выражены или очень трудно выражаются средствами логических формализмов; – проверка соответствующих свойств сред- ствами ТС и СП более проста. Заключение. Подводя итоги сказанному, от- метим две основные проблемы, с которыми сталкиваются разработчики систем анализа про- грамм. Основная проблема, препятствующая ши- рокому внедрению описанных методов, – про- блема комбинаторного взрыва, которая со- стоит в том, что при моделировании реаль- ной системы относительно небольших разме- ров, ее математическая модель может иметь УСиМ, 2015, № 1 13 астрономическое число состояний, и такой объект (СП или ТС) не может поместиться в память компьютера, что приводит к невоз- можности его дальнейшего анализа и обра- ботки. На поиск решения этой проблемы на- правлены главные усилия специалистов в об- ласти разработки формальных методов ана- лиза програмного обеспечения. Вторая проблема состоит в том, что име- ющиеся алгоритмы анализа свойств облада- ют высокой временной и емкостной сложно- стью, что затрудняет их широкое использо- вание в коммерческих системах анализа и верификации свойств формальных моделей реальных систем. В общем случае ситуация выглядит так, что с каждым годом сложность программно- го обеспечения возрастает и необходимы ав- томатизированные средства их анализа. С другой стороны, имеющиеся средства анали- за свойств таких программных систем не мо- гут обеспечить надежную и качественную их верификацию. В этом и состоит, по мнению авторов, главное противоречие и трудности, связанные с разработкой надежного и высо- кокачественного программного обеспечения. 1. Карпов Ю.Г. MODEL CHECKING: Верификация параллельных и распределенных программных систем. – С-Пб.: БХВ, 2010. – 551 с. 2. Котов В.Е. Сети Петри. – М.: Наука, 1984. – 157 с. 3. Крывый С.Л. О некоторых методах решения и кри- териях совместности систем линейных диофанто- вых уравнений в области натуральных чисел // Ки- бернетика и системный анализ. – 1999. – № 4. – С. 12–36. 4. Схрейвер А. Теория линейного и целочисленного программирования, В 2-х т. – М.: Мир, 1991. – 742 с. 5. Трахтенброт Б.А., Барздинь Я.М. Конечные авто- маты (Поведение и синтез). – М.: Наука, 1970. – 400 с. 6. Contejan Е., Ajili F. Avoiding slack variables in the solving of linear diophantine equations and inequa- tions // Theoretical Соmр. Science. – 1997. – 173. – P. 183–208. 7. Clausen M., Fortenbacher A. Efficient solution of lin- ear diophantine equations // Symbolic Computation. – 1989. – 8, N 1, 2. – P. 201–216. 8. Esparza J., Heljanko K. Unfoldings. A Partial-Order Approach to Model Checking. EATCS Mongraphs in Theoretical Computer Science. – Springer-Verlag, 2008. – 172 p. 9. Hack M.H.Т. Decidability Questions for Petri Nets // Ph. D. Thesis, M.I.T. – 1976. – 32 p. 10. Jonathan L. Gross, Jay Yellen Handbook of Graph Theory. – CRC Press, 2004. – P. 57– 68. 11. Johnson D.S. A Catalogue of Complexity Classes // J. van Leeuwen / Ed. «Handbook of Theoretical Com- puter Science». – V.A., 1990: Elsevier. – P. 67–161. 12. Kryvyi S. A Criteria of compatibility systems of linear diophantine constraints. – Lect. Notes in Comp. Sci. – Springer-Verlag, 2002. – 2328. – P. 264–271. 13. Murata T. Petri Nets: Properties, Analysis and Appli- cations // Proc. of the IEEE. – 1989. – 77, N 4. – P. 541–580. 14. Papadimitriou С.H. Computational complexity. – Ad- dison-Wesley. – 1994. – 532 p. 15. Pettier L. Minimal solution of linear diophantine sys- tems: bounds and algorithms // Proc. of the Fourth Int. Conf. on Rewriting Techniq. and Appl., Como, Italy, 1991. – P. 162–173. 16. Thomas W. Automata on infinite objects. – Handbook on theoretical computer science. – 1990. – P. 135–191. Поступила 03.12.2014 Тел. для справок: +38 044 259-0511 (Киев) E-mail: sl.krivoi@gmail.com; sdp@univ.net.ua © Ю.В. Бойко, Н.Н. Глибовец, С.В. Ершов, С.Л. Крывый, С.Д. Погорелый, А.И. Ролик, С.Ф. Теленик, А.И. Куляс, Ю.В. Крак, М.В. Ясочка, 2015  Внимание ! Оформление подписки для желающих опубликовать статьи в нашем журнале обязательно. В розничную продажу журнал не поступает. Подписной индекс 71008

Методы исследования свойств высокопроизводительных инфраструктур. Обзор

Institution

Ähnliche Einträge