Содержание к диссертации
Введение
Бесконечные синхронные потоки 14
1.1 Моделирование бесконечных потоков 14
1.2 Имя потока, вариант поведения и множество поведений потока 17
1.3 Бесконечные синхронные потоки 18
1.4 Моделирование конечных последовательностей 22
Метод синхронных потоков 28
2.1 Объект 29
2.2 Композиция объектов 37
2.3 Алгоритм синтеза математической модели системы из моделей составляющих ее объектов 48
2.4 Формальная коалгебраическая семантика 50
Темпоральная логика на потоках 55
3.1 Линейная темпоральная логика на потоках 56
3.2 Проверка моделей и доказательство теорем 62
Алгоритмы автоматического построения и анализа вариантов поведения объекта или системы объектов 65
4.1 Уточненная модель объекта с зависимыми и независимыми потоками 65
4.2 Требования конечного иедетерминизма в поведении объекта 67
4.2.1 Требования уникальности поведения объекта 67
4.2.2 Требования конечного недетерминизма в поведении объекта 68
4.3 Алгоритм построения фрагментов вариантов поведений объекта 76
4.4 Линейная темпоральная логика на фрагментах 77
4.5 Алгоритм анализа фрагментов вариантов поведения объекта путем проверки выполнимости ими временных свойств 79
Моделирование вариантов поведения системы производственных объектов 82
5.1 Модель простого производственного объекта 82
5.2 Модель простого складского объекта ч 87
5.3 Модель складского объекта с учетом динамики основных фондов 88
5.4 Модель внешнего поставщика фондов 90
5.5 Модель внешнего заказчика продукции 92
5.6 Модель системы производственного объекта с учетом внешних поставщиков и заказчика 93
5.7 Построение и анализ вариантов развития замкнутой системы 104
Основные результаты диссертационной работы 113
Приложение
Варианты поведения замкнутой ситсемы производственного объекта с поставщиками, заказчиком и управляющим объектом 125
- Имя потока, вариант поведения и множество поведений потока
- Алгоритм синтеза математической модели системы из моделей составляющих ее объектов
- Проверка моделей и доказательство теорем
- Требования уникальности поведения объекта
Введение к работе
Актуальность темы
В настоящее время усилился интерес к динамическим моделям систем, состоящих из большого числа взаимодействующих компонентов. Для решения задач моделирования таких систем требуется разработка методов моделирования, специально ориентированных на автоматизацию процессов синтеза и анализа моделей с использованием вычислительных мощностей современных персональных компьютеров. Создание и развитие автоматизированных методов моделирования является актуальной темой научных исследований.
Одним из перспективных направлений развития автоматизированных методов, является разработка методов моделирования с использованием дискретных потоков. Основы методов моделирования с использованием дискретных потоков заложены в 2001-2002 годах Ф.Арбабом, М.Бройем, Я.Руттсном, К.Столеном.
В методе Броя и Оголена входы и выходы каждого компонента системы, называемого объектом, моделировались при помощи потоков. Внутренние состояния объектов не рассматривались. Синхронность потоков не использовалась. Семантика объектов задавалась при помощи функций, преобразующих потоки на входах в потоки на выходах.
В методе Руттена и Арбаба предложены два варианта семантики: ко-алгебраическая и на основе конечных автоматов. Как и в работах Броя и Оголена, потоки использованы для моделирования входов и выходов объекта. В коалгебраической семантике внутренние состояния объектов не рассматривались. В семантике на основе конечных автоматов внутренние состояния определены внутренними состояниями соответствующего конечного автомата. Унификация способа моделирования входов, выходов и внутренних состояний не проведена. Синхронность потоков не использована.
Для развития методов моделирования с использованием дискретных потоков важными задачами являются: разработка эффективных унифицированных способов представления входных, выходных и внутренних переменных объектов и их систем, модификация этих методов с целью создания алгоритма анализа всех вариантов поведения моделей.
Цель диссертационной работы
Разработка метода синхронных потоков для дискретного моделирования динамических систем, создание алгоритмов, автоматизирующих синтез моделей систем, построение и анализ вариантов их поведений.
Научная новизна
В диссертации
Введено понятие синхронных потоков, доказаны теоремы об их основных свойствах, которые легли в основу метода синхронных потоков.
Разработан метод синхронных потоков, предназначенный для дискретного, автоматизированного моделирования вариантов поведения объектов и их систем.
Разработано унифицированное представление входов, выходов и внутренних переменных объектов через наборы синхронных потоков.
Разработаны модификации линейной темпоральной (временной) логики для работы с бесконечными потоками и их фрагментами. Темпоральная логика использована для строгой математической записи временных свойств возможных поведений объектов и их систем.
В методе синхронных потоков разработаны
Алгоритм синтеза математической модели системы по заданной структуре и по моделям составляющих систему объектов.
Алгоритм построения фрагментов вариантов поведений объекта или системы объектов и алгоритм анализа выполнимости ими временных (темпоральных) свойств.
5. Методом синхронных потоков разработаны дискретные модели: простого производственного объекта, простого складского объек та, складского объекта с учетом динамики его основных фондов, внешнего поставщика фондов, внешнего заказчика готовой продук ции.
Используя разработанный алгоритм синтеза математических моделей систем, получена модель замкнутой системы производственного объекта с поставщиками, заказчиком и управляющим объектом.
Разработанная модель решает задачу автоматического построения и анализа вариантов развития системы, позволяет менеджеру проанализировать все варианты развития и выбрать один из них.
Методы исследования
Методы исследования базируются на методах алгоритмизации, дискретного моделирования процессов, теории универсальных коалгебр, темпоральных логик, логике первого порядка.
Теоретическая и практическая значимость
Разработанный метод синхронных потоков, алгоритмы, основные идеи и утверждения, предложенные в диссертации, развивают эффективное направление в математическом моделировании через дискретные потоки и открывают дополнительные возможности исследования широкого класса динамических моделей с использованием вычислительных мощностей современных компьютеров.
Метод синхронных потоков применен для синтеза математических моделей систем производственных объектов, построения фрагментов всех вариантов поведений таких систем и анализа выполнимости ими временных свойств.
Апробация работы
Результаты диссертации докладывались и обсуждались на следующих конференциях: Workshop on Specification and Verification of Component-Based Systems (Лиссабон, 2005), CONCUR (Лондон 2004), International Workshop on Coalgebraic Methods in Computer Science (Барселона 2004), ETAPS (Барселона 2004), Всероссийская научно-практическая конференция "Инновации в пауке, технике, образовании и социальной сфере"(Казань 2003), Международная научная конференция "Компьютерное моделирование и информационные технологии в науке, инженерии и образовапии"(Пенза 2003), на школах-семинарах International Marktoberdorf Summer School (Мюнхен, 2004 и 2005), на семинарах Института теоретической информатики Технического университета Дрездена (Дрезден, 2003-2005), кафедры Управления, маркетинга и предпринимательства Казанского государственного технического университета им. А.Н. Туполева (Казань, 2003-2005).
Используемые формализмы
В этой секции определены понятия, использованные при задании математической семантики метода синхронных потоков. Семантика метода синхронных потоков основана на понятиях финальных коалгсбр бесконечных потоков элементов (из заранее определенного множества) и их подкоалгебр.
Далее приведен необходимый минимум определений. Теория универсальных коалгсбр подробно рассмотрена в работах [80], [90] а также [62, 79, 75, 76, 77, 86, 56, 60, 61].
Теория универсальных коалгебр является сравнительно молодым направлением в теоретической информатике, поэтому многие определения теории коалгебр базируются на теории категорий или на принципе дуальности и па дуальных определениях из теории универсальных (абстрактных, высших) алгебр. Теория универсальных алгебр подробно рассмотрена в работах [31, 7, 46, 23, 8, 21, 9, 24, 28, 20, 53]. Теория категорий изложена в работах [96, 48, 5, 47, 64, 95, 73, 63, 83].
Теория категорий
Теория категорий — это раздел математики, изучающий свойства отношений между математическими объектами, независящие от внутренней структуры самих объектов.
Определение 0.0.1. Категория С состоит из класса объектов objc и класса агг стрелок или морфизмов таких что: для каждого морфизма / Є arrc определена его область определения и область значений. Пусть областью определения морфизма / является объект А Є objc, а областью значений — объект В Є objc, тогда морфизм / определен как: для каждой пары морфизмов /: А —> В и д : В ^> С определена их композиция:
9f : А->С для каждого объекта А задан тоо/сдественный морфизм idA: idA : А —* А выполняются нижеследующие законы ассоциативности и mooic- дествеипости морфизмов.
Аксиома 0.0.2 (Закон тождественности). Тождественные морфизмы действуют тривиально. Пусть / : А —* В, тогда: / о idA = idBf = /
Аксиома 0.0.3 (Закон ассоциативности). Операция композиции ассоциативна. Пусть f : А—у В, g : В —* С и h : С —> D тогда: ho(gof) = {hog) of
Стандартным способом описания утверждений теории категорий являются коммутативные диаграммы.
Определение 0.0.4. Коммутативная диаграмма — это ориентированный граф, в вершинах которого находятся объекты, а стрелками являются морфизмы, причём результат композиции стрелок не зависит от выбранного пути.
Приведенные выше аксиомы теории категорий записаны с помощью коммутативных диаграмм, изображенных на рис. 1. Слева изображена коммутативная диаграмма закона тождественности, справа — коммутативная диаграмма закона ассоциативности. A-l—B
Рис. 1: Коммутативные диаграммы двух аксиом теории категорий: коммутативная диаграмма закона тождественности (слева) и коммутативная диаграмма закона ассоциативности (справа)
Определение 0.0.5. Морфизм / : А —> В называется изоморфизмом, если существует такой морфизм д : В —» А, что д f = idA и f од = idB
Определение 0.0.6. Два объекта А и В, между которыми существует изоморфизм, называются изоморфными А=і В.
В частности, для любого объекта А тождественный морфизм id а является изоморфизмом, поэтому любой объект изоморфен сам себе.
Определение 0.0.7, Для категории С определена дуальная ей категория Сор, в которой: объекты совпадают с объектами исходной категории:
А Є obj сор если и только если А Є obj с морфизмы получены «обращением стрелок»: /^ : В —> А Є arr ср если и только если f : А —» В є arr с
Для любого утверждения теории категорий можно сформулировать дуальное утверждение с помощью обращения стрелок. Дуальное явление обозначается тем же термином, но с приставкой "ко-".
Определение 0.0.8. Произведение объектов А и В это объект Ах В с двумя морфизмами pi : А х В —* А и р2 : А х В —> В такой, что для A*^-AxB-^B A-^A + B*^-B
Рис. 2: Коммутативная диаграмма произведения объектов (слева) и коммутативная диаграмма суммы объектов (справа) любого объекта С с морфизмами /і : С —> А и /2 : С — Б существует единственный (уникальный) морфизм {/1,/2) : С —> Л х Л такой, что: Pi{fuh) = /1 u Р2 (/1,/2) = /2
Определение 0.0.9. Сумма, копроизведение объектов А и В это объект Л + ? с двумя морфизмами і і : А —» А + ІЗ и г2 : В — А + Б такой, что для любого объекта С с морфизмами gi : А —> О и #2 : В —> (7 существует единственный (уникальный) морфизм [pi,2] : А + В —> С такой, что: [ffi) d о її = pi u [51, g2] ог2 = 52
Определение произведения объектов 0.0.8 наглядно представлено в виде коммутативной диаграммы слева на рис. 2, а определение 0.0.9 суммы объектов — в виде коммутативной диаграммы справа на рис. 2.
Теорема 0.0.10. Если произведение и копроизведеиие существуют, то они определяются однозначно с точностью до изоморфизлш.
Определение 0.0.11. Универсальный или инициальный объект категории — это такой объект, из которого существует единственный морфизм в любой другой объект этой категории.
Теорема 0.0.12. Если универсальный объект в категории существует, то он определяется с точностью до изоморфизма.
Дуальным образом определяется финальный или коуниверсальный объект.
Определение 0.0.13. Финальный, терминальный или коуииверсалъ-ный объект категории — это такой объект, в который из любого другого объекта категории существует единственный морфизм.
Теорема 0.0.14. Если финальный объект в категории существует, то он определяется с точностью до изоморфизма.
Введем понятие функтора, которое потребуется для описания коалгебр.
Определение 0.0.15. Функтор — это отображение одной категории в другую, сохраняющее структуру. Функтор F : С —* Ю> ставит в соответствие каждому объекту категории С объект категории В и каждому морфизму / : А — В категории С морфизм F(f) : F(A) —* F(B) категории В так, что: сохранены тождественные морфизмы: F{idA) = idF{A) сохранены композиции морфизмов: F(gof) = F(g)oF(f)
Определение 0.0.16. Категория Set функций и множеств — это категория, объектами в которой являются множества, морфизмами -— тотальные функции.
В категории Set универсальный объект — это пустое множество 0, терминальным объект — любое множество, состоящее из одного элемента. Терминальный объект обозначен через 1 = {*}.
Алгебры
Определение 0.0.17. Пусть F : Set —> Set функтор в категории Set функций и множеств. F-алгебра — это пара (М;а), состоящая из множества М и функции a : F(M) —» М. Множество М названо несущим миооїсеством алгебры. f{m1)-^If(m2) Mx —*M2
Рис. 3: Коммутативная диаграмма F-гомоморфизма между двумя F-алгєбрами
Определение 0.0.18. F-гомоморфизм между двумя F-алгебрами — это функция / : М\ —> Мг, отображающая одну F-алгебру {М^а\) в другую і^-алгебру (M2,ct2), такая что: footi = а2 о F{f)
На рис. 3 представлена коммутативная диаграмма F-гомоморфизма между двумя ^-алгебрами.
Определение 0.0.19. Для функтора F : Set —> Set семейство F-алгебр вместе с F-гомоморфизмами между ними образуют категорию Alg(F) алгебр функтора F.
Определение 0.0.20. F-алгебра (/; т) является инициальной если из нее существует точно один гомоморфизм в любую F-алгебру.
Инициальные алгебры одного и того же функтора уникальны вплоть до изоморфизма.
Определение 0.0.21. Пусть задана F-алгебра (М;а). Непустое подмножество R С (М;а) называется F-подалгеброй (или F-субалгеброй), если пара (R; а) сама является F-алгеброй.
Коалгебры
Определение 0.0.22. Пусть F : Set —> Set функтор в категории Set функций и множеств. F-коалгебра — это пара (М\а), состоящая из множества М и функции а : М —* F(M). Множество М называется несущим мпооїсеством коалгебры. мх—J—*- м2
Рис. 4: Коммутативная диаграмма F-гомоморфизма между двумя F-коалгсбрами
Определение 0.0.23. F-гомоморфизм между двумя F-коалгебрами — это функция / : М\ —» Мг, отображающая одну F-коалгебру (Mi,ai) в другую F-коалгебру (М2,аг), такая что: а2 о / = F(f) о а\
На рис. 4 представлена коммутативная диаграмма F-гомоморфизма между двумя F-коалгебрами.
Определение 0.0.24. Для функтора F : Set — Set семейство F-коалгебр вместе с F-гомоморфизмами между ними образуют категорию Coalg(F) коалгебр функтора F.
В этой категории нас интересует прежде всего финальная коалгебра (в случае, если она существует).
Определение 0.0.25. F-коалгебра (F; 7г) является финальной если из любой F-коалгебры существует точно один гомоморфизм в (Р;тг).
Финальные коалгебры одного и того же функтора уникальны вплоть до изоморфизма. Для многих функторов финальная коалгебра существует и известна, кроме того для многих функторов она строится каноническим путем [87].
Определение 0.0.26. Пусть задана F-коалгебра (М; а). Непустое подмножество R С (М;а) называется F-подкоалгеброй (или F-субкоалге-брой), если пара (Я; а) сама является F-коалгеброй.
Имя потока, вариант поведения и множество поведений потока
На произвольный поток натуральных чисел, обозначенный именем ж, не наложено никаких дополнительных ограничений кроме указания его типа. Поэтому поток х может быть реализован любой бесконечной последовательностью натуральных чисел. Это может быть бесконечная последовательность чисел, представленная потоком ах, или бесконечная последовательность чисел, представленная потоком pXi или представленная любым другим бесконечным потоком натуральных чисел.
Для произвольных фиксированных множеств Ai,..., Аг множество r-кортежей бесконечных потоков А( х... х Л с определенными на нем операциями head и tail, производимыми синхронно па всех потоках, изоморфно множеству бесконечных потоков (А\ х ... х Д.)" г-кортежей соответствующих элементов потоков Af,..., А .
Доказанные выше свойства r-кортсжей синхронных потоков положены в основу композициональной коалгебраической семантики объектов в методе синхронных потоков, т.е. такой семантики, в которой объединение объектов в систему трактуется как новый объект. Композицио-нальность семантики значительно упростила работу с ней и позволила создать алгоритм автоматического синтеза математической модели системы по заданной структуре и по моделям составляющих систему объектов.
Выражение Уг Є N. zi(i) = Z2(i) представляет собой пример инвариантного свойства, которое выполняется на всех элементах задействованных в нем потоков. Такие и более сложные инвариантные свойства используются для определения множества всех поведений объектов. Далее во время формальной записи инвариантных свойств квантор общности Уг Є N опускается, тем не менее его присутствие постоянно подразумеваться.
Определение 1.3.7. В сокращенной форме записи инвариантного свойства с подразумеваемым квантором общности, элемент z(i) потока z с индексом і назван текущим элементом потока, а значение этого элемента — текущим значением потока. Определение 1.3.8. Б сокращенной форме записи инвариантного свойства с подразумеваемым квантором общности, элемент z(i + 1) потока z с индексом г +1 назван следующим элементом потока, а его значение — следующим значением потока. Ввиду частого использования текущий элемент потока z обозначен как 2ы вместо записи z(i), а следующий элемент потока z обозначен как Хгр) вместо записи z(i + 1). В этом параграфе рассмотрен способ формального моделирования конечных последовательностей через бесконечные потоки. Определение 1.4.1. Множество А всех конечных и бесконечных последовательностей элементов из заранее фиксированного множества А задано следующим образом: где є — это пустая последовательность; {О, ...,п} — подмножество натуральных чисел от нуля до п; { $fin I Sfm : {0) —,п} — А } — множество функций Sfin, определенных на множестве {0, ...,п} и создающих отображения этого множества во множество элементов А; { Sinf Sin/ : IN — А } —- множество функций 5,-„/, определенных на множестве IV натуральных чисел и создающих отображения этого множества во множество элементов А. Определение 1.4.2. Множество А является несущим множеством финальной FA-коалгебры конечных и бесконечных последовательностей: где функция stepA имеет вид: Л — FA(A); функтор FA : Set — Set определен на множестве М как FA(M) = А х М+ 1; функция stepA определена следующим образом: если s пустая последова тельность, т.е. s = є; stepA {s) — (s(0),r) если s последовательность из одного элемента , (s(0), Xx.s(x + 1)) если s последовательность более чем из одного элемента. Операция stepA{s) возвращает специальный символ . А, в случае если последовательность s пустая, т.е. s = є. В случае если последовательность s не пустая, операция stepA{s) возвращает пару, состоящую из первого элемента последовательности и хвоста последовательности после удаления из нее первого элемента. Теорема 1.4.3. ДЛЯ финальной FA-коалгебры конечных и бесконечных последовательностей элементов из заранее фиксированного множества А не выполняются Теоремы 1.3.2, 1.3.4 и Следствия 1.3.3, 1.3.5.
Алгоритм синтеза математической модели системы из моделей составляющих ее объектов
Задано: 1) модели составляющих систему объектов, созданные методом синхронных потоков, 2) структура системы, заданная через операции параллельной композиции и соединения. Требование: все используемые интерконнекты должны быть четко определены на тех объектах, к которым они относятся. Результат: математическая модель системы объектов. Алгоритм: 1 4 I \ [ J— Рис. 2.6: Блок-схема алгоритма синтеза математической модели системы из моделей составляющих ее объектов 1) если формула системы не имеет суб-формул с операторами j или , то осуществить выход из алгоритма, 2) выбрать суб-формулу нижнего уровня с одним оператором, 3) если оператор , то переход к п. 4, иначе переход к п. 8, 4) выбрать модели, соответствующие именам двух объектов Obji и ObJ2, участвующих в параллельной композиции Obji\\ObJ2, 5) построить новый объект newObj подсистемы по правилу параллельной композиции, 6) заменить в формуле системы все вхождения суб-формулы Obji\\ObJ2 на имя нового объекта newObj, 7) переход к п. 1, 8) выбрать модель объекта Obj и список интерконнекта р, участвующих в операции соединения Obj р, 9) построить новый объект newObj подсистемы по правилами операции соединения интерфейсных потоков, 10) заменить в формуле системы все вхождения суб-формулы Obj р на имя нового объекта newObj, 11) переход к п. 1.
Любая семантика всегда задается с помощью набора описаний на так называемом "метаязыке", В зависимости от класса используемого метаязыка существует несколько видов семантик: неформальные — семантика задана при помощи понятий естественного языка; полу-формальные — часть семантики задана при помощи естественного языка, а часть — при помощи какого-либо формализма; формальные — полностью вся семантика задана при помощи математического аппарата какого-либо формализма.
Самой строгой является формальная семантика, а дальше по убывающей полу-формалыгая и неформальная. При этом качество и степень доверия к методу напрямую зависят от степени строгости задания его семантики. Поэтому в методе синхронных потоков в качестве метаязыка описания семантики выбран математический аппарат теории универсальных коалгебр.
Согласно ранее доказанным теоремам 1.3.2, 1.3.4 и следствиям 1.3.3, 1.3.5 о основных свойствах синхронных потоков, картеж синхронных потоков изоморфен потоку картежей элементов соответствующих потоков. Основываясь на этих свойствах, определим понятие "обобщенного потока объекта". Определение 2.4.1. Поток, изоморфный кортежу всех синхронных потоков объекта, назван обобщенным потоколі этого объекта. Определение 2.4.2. Семантика [А], или множество всех поведений (обобщенного потока) объекта А: А = X ; S ; У ; I ; Ф) задана пересечением: где {[/]} С2" — это множество обобщенных потоков, на которых выполняется ограничение на начальные значения /; {[Ф& С7Ш- это множество обобщенных потоков, на которых инвариантное свойство Уг Є ІУ.Ф выполняется на каждом элементе потока. Выражаясь в терминах теории универсальных коалгебр, множество {[Ф]} — это несущее множество подкоалгебры инварианта \/г Є W-Ф: финальной коалгебры обобщенных потоков объекта: ( Z , {headz», tailz- ) ) Каждый элемент из множества {А} — это конкретный вариант поведения (обобщенного потока) объекта или, эквивалентно, картеж из конкретных вариантов поведений всех составляющих объект потоков.
Разработан метод синхронных потоков, который специально ориентирован на использование вычислительных мощностей современных персональных компьютеров для автоматического синтеза математических моделей систем объектов, построения и анализа вариантов их поведений.
Разработано унифицированное представление входов, выходов и внутренних переменных объектов через наборы синхронных потоков.
В методе синхронных потоков разработан механизм поэтапного построения системы объектов. Результатом операций композиции нескольких объектов является система этих объектов, которая, в свою очередь, рассмотрена в методе синхронных потоков как больший объект, и с которым, в дальнейшем, метод синтаксически и семантически оперирует так же, как с любым другим объектом, т.е. он может использоваться как составная часть для построения других объектов.
Определены две операции композиции: первая названа параллельная композиция и служит для размещения объектов параллельно, вторая названа соединение и служит для соединения интерфейсных потоков объекта.
Введено графическое представление объектов, определено понятие обобщенного потока объекта, задана комиозициональная коалгебраиче-ская семантика объектов.
Разработан алгоритм автоматического синтеза математической модели системы из моделей составляющих ее объектов.
Проверка моделей и доказательство теорем
Метод синхронных потоков предоставляет возможность использования двух наиболее широко применяемых подходов к доказательству выполнимости временных свойств на вариантах поведения объекта или системы объектов: автоматическая проверка моделей, интерактивное доказательство теорем. Первый подход полностью автоматизирован, но имеет ограничения на количество элементов в исследуемых фрагментах потоков, и на количество различных вариантов поведения объекта.
Второй подход является мощным средством, позволяющим доказывать большой класс временных свойств на множестве поведений объекта.
Недостатком этого подхода, как следует из его названия, является интерактивность.
Для доказательства свойств требуется непосредственное участие высоко-квалифицированного специалиста в области темпоральных логик и формального доказательства теорем, что весьма дорого по себестоимости ввиду малого количества таких специалистов, высокого уровня их квалификации и больших средних временных затрат.
Поэтому в следующей главе для метода синхронных потоков разработан подход автоматической проверки моделей на выполнимость ими временных свойств на фрагментах вариантов поведений объектов и их систем.
Разработана модификация линейной темпоральной логики, специально ориентированная для работы с бесконечными потоками.
В диссертации она использована для строгой математической записи временных свойств возможных поведений объектов и их систем.
Линейная темпоральная логика необходима для строгой математической спецификации временных свойств возможных поведений объектов и их систем.
В методе синхронных потоков под спецификацией понимается математически строгая запись временных свойств поведений, которые ожидаются от создаваемых математических моделей объектов или систем объектов. После создания моделей разработанных объектов или систем проверяется их корректность относительно спецификации, т.е. выполнимость специфицированных для них временных свойств.
Требования уникальности поведения объекта
Поведение объекта названо детерминированным, если для обобщенного потока этого объекта выполняются следующие требования: задано единственное начальное значение, исходя из заданного значения текущего элемента, можно построить одно и только одно значение следующего элемента потока.
Поведение объекта названо недетерминирован-нъш если для обобщенного потока этого объекта выполняется хотя бы одно из следующих требований: задано несколько начальных значений, исходя из заданного значения текущего элемента, можно построить несколько различных значений следующего элемента потока.
Поседение объекта названо конечно недетерминированным если для обобщенного потока этого объекта выполняются следующие требования: задано конечное число начальных значений, исходя из заданного значения текущего элемента, можно построить конечное число различных значений следующего элемента потока.
В методе синхронных потоков присутствует три возможности для возникновения конечного недетерминизма: 1) в определении начальных значений аргументных потоков, 2) в определении следующих значений аргументных потоков, 3) в определении текущих значений зависимых потоков.
В инвариантном свойстве Ф для каждого с Є Arg из к аргументных потоков существует ровно cm записей, определяющих следующее значение потока. Пусть на каждом элементе аргументный поток с\ имеет cim вариантов следующего значения, аргументный поток сч — с т вариантов следующего значения. Эти варианты построения следующего значения аргументного потока не задействованы при определении начальных значений. Поэтому согласно законам комбинаторики, два аргументных потока с\ и с 2 на n-фрагментах, длинной вп + 1 элементов, образуют пс%т пС2Ш вариантов фрагментов поведений пары этих потоков.
Пусть на каждом наборе текущих элементов аргументных потоков объекта А зависимый поток z\ имеет z\m вариантов построения текущего значения, зависимый поток z% — z vn вариантов текущего значения. Эти варианты построения текущего значения потока задей-ствуются на всех элементах фрагмента.
Так как конечный недетерминизм начальных значений, недетерминизм в построении следующих значений и недетермииизм в построении текущих значений взаимно независимы, то количество различных п-фрагментов вариантов поведения объекта вычисляется как произведение.
Разработана модификация линейной темпоральной логики для работы с конечными фрагментами бесконечных потоков. Введена уточненная модель объекта, необходимая для формулировки требований конечного недетерминизма в поведении объектов и систем объектов. Определены требование уникальности поведения и требования конечного недетерминизма в поведении объектов и систем объектов.
Для уточненной модели объекта и для заданной конечной длинны фрагментов в п элементов, разработана формула подсчета количества различных фрагментов вариантов поведений этого объекта.
Для метода синхронных потоков разработаны алгоритмы автоматического построения и анализа фрагментов вариантов поведений объектов и систем объектов.
