Дубинин В.Н., Зинкин С.А. Языки логического программирования в проектировании вычислительных систем и сетей

Подождите немного. Документ загружается.

из начального состояния, никогда не наблюдается одновременное

нахождение двух узлов в критических областях.

Определим предикат crit следующим образом:

crit(I,S):- inlist(critical(I,H),S).

Истинное значение выражения crit(I,S) интерпретируется как

нахождение i-го узла в критической области. ЛДВ-формула для проверки

свойства взаимного исключения имеет вид:

╞ init→ALL∼(crit(site_a) & crit(site_b)).

Запрос mutual_exclusion для проверки указанного свойства на языке

Пролог может иметь следующий вид:

mutual_exclusion:- init(S),implies(init,all(not(

and(crit(site_a), crit(site_b)))),S).

Введя целевое утверждение mutual_exclusion через некоторое время,

Пролог-интерпретатор выдаст ответ yes, что означает, что верифицируемая

система обладает свойством взаимного исключения.

Докажем отсутствие блокировок в РВС, работающей в соответствии с

алгоритмом взаимного исключения. В системе отсутствуют блокировки,

если для всех вариантов функционирования системы, стартующей из

начального состояния, при запросе узла на вхождение в критическую

область, он (узел) рано или поздно, но неизбежно в нее войдет. Введем

предикат req следующим образом:

req(I,S):- inlist(request(I,J,H),S).

Истинное значение выражения req(I,S) интерпретируется как готовность и

желание i-го узла войти в свою критическую область. Для проверки

отсутствия блокировок используется следующая ЛДВ-формула (для узла

site_a):

╞ init→ALL(req(site_a)→INEV(crit(site_a)).

Для узла site_b формула строится аналогично. Формулировку

соответствующего запроса на языке Пролог можно определить следующим

образом:

starvation_free:- init(S),implies(init(S),all(implies(

req(site_a),inev(crit(site_a)))),S).

На запрос starvation_free Пролог-система отвечает yes, что можно

проинтерпретировать как отсутствие блокировок.

Для доказательства отсутствия тупиков определим предикат transition,

используемый в теле клоза liveness, следующим образом:

transition(T0):- site(S),tr(T),T)=..[T,S].

site(site_a).

site(site_b).

tr(send).

tr(receive).

tr(release).

tr(i_reply).

tr(w_reply).

Результаты оценки целевого утверждения liveness позволяют сделать

вывод, что тупики в системе отсутствуют.

3.3.6. Альтернативно-битовый протокол

Считается, что протокол составлен корректно, если при реализации

поведение системы отвечает следующим требованиям:

1. Отсутствие тупиков, т.е. таких состояний, когда цель еще не

достигнута, а ни один объект не может изменить своего состояния.

2. Полнота - все предусмотренные спецификацией условия, действия и

ситуации учтены, и соответствующие состояния достижимы.

3. Отсутствие бесполезных зацикливаний.

4. Недопустимость переполнений - реализация ограничений на

количество переходов в отдельные состояния, обусловленные

спецификацией.

5. Соответствие терминальных состояний поставленным в спецификациях

целям.

Эти пять условий определяют общую корректность, поскольку все

протоколы обязательно должны удовлетворять этим условиям. Кроме

общей корректности для каждого конкретного типа протоколов существует

частная корректность, обусловленная спецификой протокола. В качестве

условий, определяющих частную корректность АБ-протокола, можно

выделить, например, следующие: "Линия не должна передавать более чем

один кадр одновременно", "Передатчик может находиться либо в состоянии

готовности, либо в состоянии ожидания подтверждения, но не в обоих

сразу".

Докажем общую корректность АБ-протокола. Для этого докажем, что

сетевая модель, представленная на рис.2.11, жива.

Определим предикат transition, используемый в теле клоза liveness,

следующим образом:

transition(T0):- bit(S),tr(T),T0=..[T,S].

bit(zero).

bit(one).

tr(tsend).

tr(recack).

tr(propagate).

tr(repeata).

tr(reception).

tr(loss).

tr(repeatm).

На утверждение liveness Пролог-интерпретатор отвечает yes,

следовательно, АБ-протокол в общем корректен.

Покажем выполнение условия частной корректности, согласно которому

линия не должна передавать более чем один кадр одновременно. Из сетевой

модели на рис.2.11 видно, что среда передачи определяется позициями send и

receive. Маркировка любой из этих позиций означает нахождение в среде

передачи кадра(ов). Число кадров в среде передачи определяется как

M(send) + M(receive),

где функция М в данном случае ставит в соответствие позициям сетевой

модели численное значение маркировки. Упомянутое требование в терминах

сетевой модели формулируется следующим образом: всегда должно

выполняться неравенство:

0 ≤ M(send)+M(receive) ≤ 1.

C использованием временной логики данное условие может быть

выражено в виде следующей формулы:

╞ init→ALL(M(send)=0 & M(receive)=0

∨ M(send)=0 & M(receive)=1

∨ M(send)=1 & M(receive)=0).

Выразим данную формулу на языке Пролог. Введем предикат

num(E,N,L) для определения N - числа вхождений элемента E в список L,

следующим образом:

num(E,0,[]).

num(E,N,[E|R]):-num(E,N1,R), N is N1+1.

num(E,N,[F|R]):-num(E,N,R).

С использованием данного предиката вышеприведенная ЛДВ-формула

представляется на языке Пролог следующим образом:

implies(init,all(or(or(and(num(send(_,_,_),0),

num(receive(_,_,_),0)),and(num(send(_,_,_),0),

num(receive(_,_,_),1))),and(num(send(_,_,_),1),

num(receive(_,_,_),0)))),S).

Данное утверждение достигается, следовательно, отмеченное условие

выполняется.

Покажем выполнение условия частной корректности АБ-протокола,

согласно которому передатчик может находиться либо в состоянии

готовности, либо в состоянии ожидания подтверждения (но не в обоих

сразу). Как было отмечено в разд.2.5, условие M(send)=1 интерпретируется

как нахождение передатчика в состоянии готовности, а M(wait)=1 - в

состоянии ожидания подтверждения. В терминах сетевых моделей данное

условие корректности может быть сформулировано следующим образом:

всегда должно выполняться равенство:

M(psend)+M(wait)=1.

Иными словами, позиции psend и wait образуют инвариант.

Формула временной логики, представляющая данное утверждение,

╞ init→ALL(M(psend)=0 & M(wait)=1

∨ M(psend)=1 & M(wait)=0)).

Интерпретация данной формулы на языке Пролог следующая:

implies(init(all(or(and(num(psend(_),0),num(wait(_),1)),

and(num(psend(_),1),num(wait(_),0)))),S).

Данное целевое утверждение достигается, следовательно, отмеченное

условие выполняется.

Проверим истинность следующего утверждения: "В любом случае

переданный кадр рано или поздно, но неизбежно подтвердится". Для этого

определим предикаты sended и confirmed.

sended(S):-inlist(wait(B),S).

confirmed(S):-inlist(psend(B),S).

Истинность первого предиката указывает на то, что кадр передан, а

второго - на то, что предыдущий переданный кадр подтвержден.

Формула временной логики, представляющая данное утверждение,

записывается следующим образом:

╞ init→ALL(sended→INEV(confirmed)).

На языке Пролог данная формула интерпретируется следующим образом:

implies(init,all(implies(sended,inev(confirmed)))),S).

При оценке данного утверждения будет получен ложный результат.

Таким образом, приведенное выше утверждение ложно. Объяснение может

быть следующим: при высоком уровне помех в канале связи существует

ситуация, когда информационный кадр или подтверждение постоянно

искажаются. В результате этого возникают бесконечные повторные передачи

и в итоге переданный кадр так и не будет подтвержден.

Могут быть составлены и другие утверждения, касающиеся

функционирования АБ-протокола, например, такие как "возможно некоторое

время четности передатчика и приемника не будут совпадать", "в

состоянии ожидания передатчик ожидает подтверждения той же четности"

и т.д.

Литература

1. Кларк К., Маккейб Ф. Введение в логическое программирование на

микро-Прологе. - М.: Радио и связь, 1987. - 312 с.

2. Логический подход к искусственному интеллекту: от классической

логики к логическому программированию /Тейз А. и др. - М.: Мир, 1990.

- 432 с.

3. Грэй П. Логика, алгебра и базы данных. - М.: Машинострое-ние, 1989. -

368 с.

4. Лорьер Жан-Луи. Системы искусственного интеллекта. - М.: Мир,

1991. - 568 с.

5. Хоггер К. Введение в логическое программирование. - М.: Мир, 1988.

- 348 с.

6. Братко И. Программирование на языке Пролог для искусственного

интеллекта. - М.: Мир, 1990. - 559 с.

7. Доорс Дж. и др. Пролог - язык программирования будущего. -М.:

Финансы и статистика, 1990. - 144 с.

8. Ин Ц., Соломон Д. Использование Турбо-Пролога. - М.: Мир, 1990.

9. Искусственный интеллект: В 3-х кн. Кн. 3. Программные и аппаратные

средства. Справочник/Под ред. В.Н. Захарова, В.Ф. Хорошевского. - М.:

Радио и связь, 1990. - 368 с.

10. Стерлинг Л., Шапиро Э. Искусство программирования на языке

Пролог. - М.: Мир, 1990. - 335 с.

11. Малпас Дж. Реляционный язык Пролог и его применение.- М.: Наука,

1990.- 464 с.

12. Кузнецов В.Е. Представление в ЭВМ неформальных процедур.

Продукционные системы. - М.: Наука, 1989. -

13. Нейлор К. Как построить свою экспертную систему. - М. :

Энергоатомиздат, 1991. - 286 с.

14. Попов Э.В. Экспертные системы. - М.: Наука, 1987. - 288 с.

15. Уотермен Д. Руководство по экспертным системам. - М. : Мир, 1989. -

388 с.

16. Экспертные системы. Принципы работы и примеры /А. Брукинг и др.,

под ред. Р. Форсайта. - М.: Радио и связь, 1987. - 224 с.

17. Элти Дж., Кумбс М. Экспертные системы: концепции и примеры. - М.:

Финансы и статистика, 1987. - 192 с.

18. Клоксин У., Меллиш К. Программирование на языке Пролог : Пер. с

англ. - М.: Мир, 1987. - 336 с.

19. Макаллистер Дж. Искусственный интеллект и Пролог на микро-ЭВМ:

Пер. с англ. - М.: Машиностроение, 1990.- 240 с.

20. Язык Пролог в пятом поколении ЭВМ. Сб. статей. - М.: Мир,1988.

- 501 с.

21. Пролог - язык программирования будущего: Пер. с англ./ Доорс Дж. и

др. - М.: Финансы и статистика, 1980. - 142 с.

22. Claudia M. Prolog programming. Applications for database systems, expert

systems, and natural language systems. - Addison-Wesley publishing

company. - 1986. - 325 P.

23. Питерсон Дж. Теория сетей Петри и моделирование сис-тем. - М.:Мир,

1984. - 263 с.

24. Соловьев Г.Н.,Никитин В.Д. Операционные системы ЭВМ:

Учеб.пособие. - М.:Высшая школа, 1989. - 255 с.

25. Шоу А. Логическое проектирование операционных сис-тем: Пер.с англ.

- М.: Мир, 1981. - 360 с.

26. Вычислительные сети и сетевые протоколы / Д.Дэвис, Д.Барбер,

У.Прайс и др. - М.: Мир, 1983. - 560 с.

27. Зайцев С.С. Описание и реализация протоколов сетей ЭВМ. - М.:

Наука, 1989. - 272 с.

28. Бандман О.Л. Сети Петри и корректность протоколов передачи данных

//Вычислительные системы: Межвуз.сб.науч.тр. - Новосибирск, 1985. -

С.29-51

29. Дубинин В.Н.,Зинкин С.А. Спецификация и верификация процессов

обмена информацией в вычислительных системах и сетях:

Учеб.пособие. - Пенза: Изд-во Пенз.политехн.ин-та, 1992. - 95 с.

30. Cтобо Д.Ж. Язык программирования Пролог. - М.: Радио и связь,

1993. - 368 с.

31. Системы дедуктивного вывода и решение логических задач.

Методические указания. Составители: С.Л.Зверев, В.Н.Дубинин. -

Пенза: ПГТУ, 1993. - 60 с.

32. Genrich H.J., Lautenbach . System modelling with high-level Petri nets //

Theor.Comput.Sci. - 1981. - v.13, N 1. -P. 109 - 136

33. Azema P.,Juanole G.,Sandus E.,Moutbernard M. Specification and

verification of distributed systems using Prolog interpreted Petri nets // Proc.

Int. Conf. Software Eng. - 1984. -P.510 - 518

34. Papapanagiotakis G.,Azema P.,Pradin-Chezalviel B. Propositional branching

time temporal logic in Prolog // 5

Annu.Int.Phoenix. Conf. Comput. and

Commun. - 1986. - P.371 - 377

35. Berthelot G.,Terrat R. Petri nets theory for the correct-ness of protocols //

IEEE Transactions on communications. - Vol. Com-30, N 12. - 1982. -

P.2497 - 2505

36. Марселлус Д. Программирование экспертных систем на Турбо

Прологе. - М.: Финансы и статистика, 1994. - 256 с.

37. Дубинин В.Н.,Гусаров С.В. Сетевые спецификации и моделирование

параллельных взаимодействующих интеллектуальных систем с

использованием языков искусственного интеллекта // Материалы

междунар. научн.-техн. конф. "Новые информационные технологии и

системы". - Пенза, 1994. - С.72

38. Перспективы развития вычислительной техники: В 11 кн.:

Справ.пособие / Под ред.Ю.М.Смирнова. Кн. 1: Информационные

семантические системы / Н.М.Соломатин . - М.: Высш.шк., 1989. - 127 с.

39. Перспективы развития вычислительной техники: В 11 кн.:

Справ.пособие / Под ред.Ю.М.Смирнова. Кн. 2: Интеллектуализация

ЭВМ / Е.С.Кузин, А.И.Ройтман, И.Б.Фоминых, Г.К.Хахалин. - М.:

Высш.шк., 1989. - 159 с.

40. Voss K. Stepwise specification of a distributed database system // Proc. 2nd

Int.Conf.Distrib.Comput.Syst. - Paris, 1981. - P. 218-226

41. Вашкевич Н.П.,Дубинин В.Н.,Зверев С.Л.,Зинкин С.А. Проектирование

интеллектуальных систем управления массовой памятью на основе

функционального подхода // Моделиране и симулиране на човешката

памет - МНЕМО'89: Тез. докл. III науч.-техн. конф. с международным

участием "ДЗУ'89". - Варна (НРБ), 1989. - С.24-26

42. Дубинин В. Н., Зинкин С.А. Экспертная система для верификации и

проектирования алгоритмов функционирования систем управления

внешней памятью ЭВМ // Практика применения баз данных для решения

информационно-поисковых задач и задач управления. - Пенза: ПДНТП,

1989. - С.28-29

43. Вашкевич Н.П.,Дубинин В.Н. Моделирование и верификация систем

управления внешней памятью ЭВМ с использованием системы

продукций // Базы данных и экспертные системы в АСНИ: Тез. докл.

конф. - Севастополь, 1990

44. Дубинин В.Н.,Зверев С.Л.,Зинкин С.А. Разработка интеллектуальной

САПР систем управления внешней памятью высокопроизводительных

ЭВМ // Программное обеспечение ЭВМ: Тез.докл. III междунар. науч.-

техн. конф. Секция 6. - Тверь,1990. - С.64-66

45. Вашкевич Н.П.,Дубинин В.Н.,Зинкин С.А. Использование методов

искусственного интеллекта при проектировании интеллектуальных

систем управления внешней и массовой памятью ЭВМ // Техническая

кибернетика. Изв. АН СССР. - 1991. - N 5. - С.63-74

46. Дубинин В.Н.,Зверев С.Л.,Зинкин С.А. Аппаратная поддержка

функций управления базами знаний в системах искусственного

интеллекта // Вычислительная техника в автоматизированных системах

контроля и управления: Межвуз.сб.науч.тр. - Пенза, ППИ. - 1991. - С.66-

47. Дубинин В.Н. Построение экспертных систем для верификации и

моделирования коммуникационных протоколов // Материалы

Межреспубл. конф. "Повышение эффективности средств обработки

информации на базе математического и машинного моделирования". -

Тамбов, 1993. - С.263-264

48. Дубинин В.Н. Язык логических запросов к базе данных о переходах

состояний для верификации дискретных систем // Материалы междунар.

науч.-техн. конф. "Новые информационные технологии и системы"

(НИТС'94). - Пенза,1994. - С.59

49. Дубинин В.Н. Интерпретация логических запросов, основанных на

временной логике // Материалы 2-й международной науч.- техн. конф.

"Новые информационные технологии и системы" (НИТС'96), ч. 1. -

Пенза : ПГТУ. - 1994. - С.73-74

50. Дубинин В.Н. Вычисление логических запросов, основанных на

временной логике. - Пензенский гос. техн. ун-т. - Пенза, 1996. - 54 с. -

Деп. в ВИНИТИ 14.02.96, N 488-В96

51. Дубинин В.Н. ПЕТРИС - комплекс программ для графического

моделирования расширенных сетей Петри / Пензенский гос. техн. ун-т. -

Пенза, 1996. - 34 с. - Деп. в ВИНИТИ 23.07.96; N 2502-В96

52. Программирование на языке Лисп: Методические указания /

Составитель: В.Н.Дубинин. - Пенза: Изд-во Пенз.гос.техн.ун-та, 1996. -

38 с.

53. Zinkin S.A. Using an intelligent storage for building knowledge

representation systems // IV Int. Conf.Disc Storage Devices. - Costenets

(Bulgaria),1990. - P.50-51

54. Zinkin S.A. Toward intellectual mass memory design for building high-

performance computer systems and networks // Proc. Second Int. Conf. Sci. &

Techn. "Current Problems of Fundamental Sciences", Part 14. - M.,1994

55. Zinkin S.A. The software and hardware architecture of a tightly-co- upled

interface for a knowledge representation system // Proc. Int. Conf. Sci. &

Techn. "New information technologies and systems" (NITS'94). - Penza,

1994. - P.50

56. Zinkin S.A. Design the intellectual mass memory for building high-

performance computer systems and networks // Proc. Int. Conf. Sci. & Techn.

"New information technologies and systems" (NITS'94). - Penza, 1994. - P.85

57. Vashkevitch N.P., Derbenyov S.A., Zinkin S.A. Prolog as a formalism for

nondeterministic automata simulation // Proc. Int. Conf. Sci. & Techn. "New

information technologies and systems" (NITS'94). - Penza, 1994. - P.39-40

58. Vashkevitch N.P., Derbenyov S.A., Zinkin S.A. Experiences in Prolog-

based hardware representation formalism // Proc. Int. Conf. Sci. & Techn.

"New information technologies and systems" (NITS'94). - Penza, 1994. -

P.41-42

59. Dubinin V.N. SIMS-M - a software package for design and implementation

of distributed systems on the basis of local area network // Proc. Int. Conf.

Sci. & Techn. "New information technologies and systems" (NITS'94). -

Penza, 1994. - С.77-78

60. Tuzilov I.V., Dubinin V.N., Finogeev A.G. Ontological knowledge

representation // Proc. Int. Conf. Sci. & Techn. "New information technologies

and systems" (NITS'94). - Penza, 1994. - P.52

61. Vashkevich N.P., Dubinin V.N. Net formalism based tools for design,

verification and implementation of distributed systems // Proc. EAST - WEST

Int. Conf. "Information Technology in Design" (EWITD'94), Part 2. - M.,

1994, P.170-174.

62. Dubinin V.N. Design of distributed CAD systems on the basis of local area

network // EAST-WEST Int.Conf. "Information Technology in Design"

(EWITD'96). - M.: 1996. - P.152-155

63. Zinkin S.A. Systolic nets modelling with simulation programs of different

types // Proc. EAST - WEST Int. Conf. "Information Technology in Design"

(EWITD'96). - M.: 1996. - P.87-90

64. Zinkin S.A. The software and hardware architecture of a tightly-coupled

interface for a knowledge representation system // Proc. EAST - WEST Int.

Conf. "Information Technology in Design" (EWITD'96). - M., 1996. - P.87-

65. Дубинин В.Н. Децентрализованное управление распределенными

данными в локальной вычислительной сети: спецификация,

моделирование, реализация и применение в распределенных

вычислениях / Пензенский гос. техн. ун-т. - Пенза, 1997. - 78 с. - Деп. в

ВИНИТИ 10.06.97, N 1946-B97.