Теория процессов
 Скачать 1.62 Mb.
|
11.2 Исчисление взаимодействующих си- стем (CCS) Исчисление Взаимодействующих Систем (Calculus of Communicating Systems, CCS) было впервые опубликовано Милнером в 1980 г. в книге [89]. Стандартным учебником по CCS является книга [92]. 321 В [89] отражены результаты исследований Милнера, прове- дённые им в период с 1973 по 1980 г. Основные работы Милнера по моделям параллельных про- цессов, выполненные в этот период: • работы [84], [85], в них Милнер исследует денотационную семантику параллельных процессов • [83], [88], здесь, в частности, введено понятие потокового графа (flow graph) с синхронизированными портами, • [86], [87], в этих работах появилось современное CCS. Используемая в CCS модель взаимодействия параллельных процессов, основанная на понятии передачи сообщений, взята Милнером из работы Хоара [71]. В статье [66] исследуются сильная и наблюдаемая эквива- лентности и вводится логика Хеннесси - Милнера. Понятия, введённые в CCS, развивались и в рамках других подходов, среди которых следует отметить в первую очередь • π–исчисление ([53], [97], [94]), и • структурную операционную семантику (SOS), это направ- ление было создано Г. Плоткиным, и опубликовано в работе [104]. Более подробная информация исторического характера о CCS может быть найдена в [105]. 11.3 Теория взаимодействующих после- довательных процессов (CSP) Теория взаимодействующих последовательных процессов (Com- municating sequential processes, CSP) была разработана англий- ским математиком Тони Хоаром (C.A.R. Hoare) (р. в 1934). Эта теория возникла в 1976 г. и была опубликована в [71]. Более пол- ное изложение CSP содержится в книге [73]. 322 В CSP изучается модель взаимодействия параллельных про- цессов, основанная на передаче сообщений. Рассматривается син- хронное взаимодействие между процессами. Одним из ключевых понятий CSP является понятие охраняе- мой команды, которое Хоар позаимствовал из работы Дейкстры [52]. В [72] рассматривается модель CSP, основанная на теории трасс. Недостатком этой модели является отсутствие методов изучения дедлокового поведения. Этот недостаток устранён в другой модели CSP (failure model), введённой в [46]. 11.4 Алгебра взаимодействующих про- цессов (ACP) Ян Бергстра (Jan Bergstra) и Ян Виллем Клоп (Jan Willem Klop) в 1982 г. в работе [37] ввели термин “процессная алгебра” (process algebra), понимая по этим теорию первого порядка с равенством, в которой предметные переменные принимают значения в мно- жестве процессов. Затем разработанные ими подходы привели к созданию нового направления в теории процессов - алгебры вза- имодействующих процессов (Algebra of Communicating Processes, ACP), которое изложено в работах [39], [40], [34]. Главным объектом изучения в ACP являются логические тео- рии, в которых испольуются функциональные символы, соответ- ствующие операциям над процессами (a., +, и т.д.) В [30] проводится сравнительный анализ различных точек зрения на понятие процессной алгебры. 11.5 Процессные алгебры Термин процессная алгебра (ПА), введённый Бергстрой и Клопом, постепенно стал использоваться в двух значениях: • в первом значении данный термин обозначает произволь- ную теорию первого порядка с равенством, областью ин- терпретации которой является некоторое множество про- цессов, и 323 • во втором значении данный термин обозначает большой класс направлений, каждое из которых связано с некоторой алгебраической теорией, описывающей свойства процессов, в этом значении данный термин используется, например, в названии книги “Справочная книга по процессной алгебре” (Handbook of Process Algebra) [42] Ниже мы перечисляем наиболее важные источники, относя- щиеся к ПА в обоих значениях этого термина. 1. Справочная книга по ПА [42]. 2. Краткий обзор основных результатов в ПА: [19]. 3. Исторические обзоры: [27], [28], [15]. 4. Различные подходы, связанные с понятием эквивалентно- сти процессов: [101], [59], [57], [58], [56]. 5. ПА с семантикой частичных порядков: [44]. 6. ПА с рекурсией: [91], [47]. 7. SOS-модель для ПА: [21], [38]. 8. Алгебраические методы верификации: [63]. 9. ПА с данными (действия и процессы параметризованы эле- ментами данных) • ПА с данными µ-CRL • [62] (есть программное средство для верификации на основе излагаемого подхода). • PSF [79] (есть программное средство). • Язык формальных описаний LOTOS [45]. 10. ПА с временем (действия и процессы параметризованы мо- ментами времени) • ПА с временем на основе CCS: [114], [99]. • ПА с временем на основе CSP: [107]. Учебник: [109]. 324 • ПА с временем на основе ACP: [29]. • Интеграция дискретного и плотного времени, относи- тельного и абсолютного времени: [32]. • Теория ATP: [100]. • Учёт времени в БМ: [33]. • Программное средство UPPAAL [74] • Программное средство KRONOS [116] (временные ав- томаты). • µ-CRL с временем: [111] (эквациональные рассужде- ния). 11. Вероятностные ПА (действия и процессы параметризованы вероятностями). Данные ПА предназначены для комбинированного иссле- дования систем, при котором одновременно производится верификация, и анализ производительности. • Пионерская работа: [64]. • Вероятностные ПА, основанные на CSP: [76] • Вероятностные ПА, основанные на CCS: [69] • Вероятностные ПА, основанные на ACP: [31]. • ПА TIPP (и связанное с ней програмное средство): [60]. • ПА EMPA: [43]. • В работах [50] и [23] рассмотрено одновременное ис- пользование обычной и вероятностной альтернативной композиции процессов. • В работе [51] рассмотрено понятие аппроксимации ве- роятностных процессов. 12. Программные средства, относящиеся к ПА • Concurrency Workbench [98] (ПА типа CCS). • CWB-NC [117]. 325 • CADP [54]. • CSP: FDR http://www.fsel.com/ 11.6 Мобильные процессы Мобильные процессы описывают поведение распределённых си- стем, во время функционирования которых может изменяться • конфигурация связей между их компонентами, и • структура этих компонентов. Основные источники: 1. π-исчисление (Milner и др.): • старый справочник: [53], • стандартный справочник: [97], • учебники: [94], [8], [10], [9] • страница в Википедии: [14] • реализация π-исчисления на распределённой вычисли- тельной системе: [115]. • приложения π–исчисления к моделированию и вери- фикации криптографических протоколов: [12] 2. The ambient calculus: [48]. 3. Action calculus (Milner): [93] 4. Биграфы: [95], [96]. 5. Обзор литературы по мобильным процессам: [11]. 6. Программное средство: Mobility Workbench [112]. 7. Сайт www.cs.auc.dk/mobility Другие источники: 326 • Лекция Р. Милнера “Computing in Space” [6], которую он прочитал на открытии здания им. Билла Гейтса, постро- енном для Компьютерной Лаборатории университета Кем- бриджа 1 мая 2002 г. В лекции вводятся понятия “ambient” и “bigraph”. • Лекция Р. Милнера “Turing, Computing and Communication” [7]. 11.7 Гибридные системы Это системы, в которых • значения одних переменных изменяются дискретно, и • значения других переменных изменяются непрерывно. Моделирование поведения таких систем производится с ис- пользованием дифференциальных и алгебраических уравнений. Основные подходы: • Гибридные процессные алгебры: [41], [49], [113]. • Гибридные автоматы [22] [77]. Для моделирования и верификации гибридных систем разра- ботано программное средство HyTech [68]. 11.8 Другие математические теории и программные средства, связанные с моделированием процессов • Страница в Википедии по теории процессов [13]. • Теория сетей Петри [103]. • Теория частичных порядков [80]. • Темпоральная логика и model checking [106], [118]. 327 • Теория трасс [108]. • Исчисление инвариантов [24]. • Метрический подход (в котором изучается понятие рассто- яния между процессами): [35], [36]. • SCCS [90]. • CIRCAL [82]. • MEIJE [25]. • Процессная алгебра Hennessy [65]. • Модели процессов с бесконечным числом состояний: [119], [120], [121], [122]. • Синхронно взаимодействующие автоматы: [123], [124], [125]. • Асинхронно взаимодействующие расширенные автоматы: [126]–[130]. • Фрмальные языки SDL [131], Estelle [132], LOTOS [133]. • Формализм Statecharts, введенный D. Harel’ом [134], [135] и входящий в язык проектирования UML. • Модель взаимодействующих расширенных временных ав- томатов CETA (Communicating Extended Timed Automata) [136]–[140]. • A Calculus of Broadcasting Systems [17], [18]. 11.9 Бизнес-процессы 1. BPEL (Business process execution language) [141]. 2. BPML (Business Process Modeling Language) [16], [142]. 3. Статья “Does Better Math Lead to Better Business Processes?” [143]. 328 4. Страничка “π-calculus and Business Process Management” [144]. 5. Статья “Workflow is just a π-process”, Howard Smith and Peter Fingar, October 2003 [145]. 6. “Третья волна” в моделировании бизнес-процессов: [146], [147]. 7. Статья “Composition of executable business process models by combining business rules and process flows” [148]. 8. Web services choreography description language [149]. 329 Литература [1] Web-страничка Р.Милнера http://www.cl.cam.ac.uk/rm135/ [2] Страничка Р.Милнера в Википедии http://en.wikipedia.org/wiki/Robin_Milner [3] Интервью Р. Милнера http://www.dcs.qmul.ac.uk/martinb/ interviews/milner/ [4] http://www.fairdene.com/picalculus/ robinmilner.html [5] http://www.cs.unibo.it/gorrieri/ icalp97/Lauree_milner.html [6] R. Milner: Computing in Space. May, 2002. http://www.fairdene.com/picalculus/ milner-computing-in-space.pdf [7] R. Milner: Turing, Computing and Communication. King’s College, October 1997. http://www.fairdene.com/picalculus/ milner-infomatics.pdf [8] Учебное пособие по π-исчислению: the pi-calculus, a tutorial. http://www.fairdene.com/picalculus/ pi-c-tutorial.pdf 330 [9] J. Parrow: An introduction to the π-calculus. [42], p. 479-543. [10] D. Sangiorgi and D. Walker: The π-calculus: A Theory of Mobile Processes. ISBN 0521781779. http://us.cambridge.org/titles/ catalogue.asp?isbn=0521781779 [11] S. Dal Zilio: Mobile Processes: a Commented Bibliography. http://www.fairdene.com/picalculus/ mobile-processes-bibliography.pdf [12] M. Abadi and A. D. Gordon: A calculus for cryptographic protocols: The Spi calculus. Journal of Information and Computation, 143:1-70, 1999. [13] Страница в Википедии "Process calculus" http://en.wikipedia.org/wiki/Process_calculus [14] Страница в Википедии по π-исчислению http://en.wikipedia.org/wiki/Pi-calculus [15] J.C.M. Baeten: A brief history of process algebra, Rapport CSR 04-02, Vakgroep Informatica, Technische Universiteit Eindhoven, 2004 http://www.win.tue.nl/fm/0402history.pdf [16] Business Process Modeling Language http://en.wikipedia.org/wiki/BPML [17] http://en.wikipedia.org/wiki/ Calculus_of_Broadcasting_Systems [18] K. V. S. Prasad: A Calculus of Broadcasting Systems, Science of Computer Programming, 25, 1995. [19] L. Aceto: Some of my favorite results in classic process algebra. Technical Report NS-03-2, BRICS, 2003. 331 [20] L. Aceto, Z.Т. ´ Esik, W.J. Fokkink, and A. Ing´ olfsd´ ottir (editors): Process Algebra: Open Problems and Future Directions. BRICS Notes Series NS-03-3, 2003. [21] L. Aceto, W.J. Fokkink, and C. Verhoef: Structural operational semantics. In [42], pp. 197–292, 2001. [22] R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine: The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3–34, 1995. [23] S. Andova: Probabilistic Process Algebra. PhD thesis, Technische Universiteit Eindhoven, 2002. [24] K.R. Apt, N. Francez, and W.P. de Roever: A proof system for communicating sequential processes. TOPLAS, 2:359–385, 1980. [25] D. Austry and G. Boudol: Alg´ ebre de processus et synchronisation. Theoretical Computer Science, 30:91–131, 1984. [26] J.C.M. Baeten: The total order assumption. In S. Purushothaman and A. Zwarico, editors, Proceedings First North American Process Algebra Workshop, Workshops in Computing, pages 231–240. Springer Verlag, 1993. [27] J.C.M. Baeten: Over 30 years of process algebra: Past, present and future. In L. Aceto, Z. Т. ´ Esik, W.J. Fokkink, and A. Ing´ olfsd´ ottir, editors, Process Algebra: Open Problems and Future Directions, volume NS-03-3 of BRICS Notes Series, pages 7–12, 2003. [28] http://www.win.tue.nl/fm/pubbaeten.html [29] J.C.M. Baeten and J.A. Bergstra: Real time process algebra. Formal Aspects of Computing, 3(2):142–188, 1991. [30] J.C.M. Baeten, J.A. Bergstra, C.A.R. Hoare, R. Milner, J. Parrow, and R. de Simone: The variety of 332 process algebra. Deliverable ESPRIT Basic Research Action 3006, CONCUR, 1991. [31] J.C.M. Baeten, J.A. Bergstra, and S.A. Smolka: Axiomatizing probabilistic processes: ACP with generative probabilities. Information and Computation, 121(2):234–255, 1995. [32] J.C.M. Baeten and C.A. Middelburg: Process Algebra with Timing. EATCS Monographs. Springer Verlag, 2002. [33] J.C.M. Baeten, C.A. Middelburg, and M.A. Reniers: A new equivalence for processes with timing. Technical Report CSR 02-10, Eindhoven University of Technology, Computer Science Department, 2002. [34] J.C.M. Baeten and W.P. Weijland: Process Algebra. Number 18 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1990. [35] J.W. de Bakker and J.I. Zucker: Denotational semantics of concurrency. In Proceedings 14th Symposium on Theory of Computing, pages 153–158. ACM, 1982. [36] J.W. de Bakker and J.I. Zucker: Processes and the denotational semantics of concurrency. Information and Control, 54:70–120, 1982. [37] J.A. Bergstra and J.W. Klop: Fixed point semantics in process algebra. Technical Report IW 208, Mathematical Centre, Amsterdam, 1982. [38] J.A. Bergstra and J.W. Klop: The algebra of recursively defined processes and the algebra of regular processes. In J. Paredaens, editor, Proceedings 11th ICALP, number 172 in LNCS, pages 82–95. Springer Verlag, 1984. [39] J.A. Bergstra and J.W. Klop: Process algebra for synchronous communication. Information and Control, 60(1/3):109–137, 1984. 333 [40] J.A. Bergstra and J.W. Klop: A convergence theorem in process algebra. In J.W. de Bakker and J.J.M.M. Rutten, editors, Ten Years of Concurrency Semantics, pages 164–195. World Scientific, 1992. [41] J.A. Bergstra and C.A. Middelburg: Process algebra semantics for hybrid systems. Technical Report CS-R 03/06, Technische Universiteit Eindhoven, Dept. of Comp. Sci., 2003. [42] J.A. Bergstra, A. Ponse, and S.A. Smolka, editors: Handbook of Process Algebra. North-Holland, Amsterdam, 2001. [43] M. Bernardo and R. Gorrieri: A tutorial on EMPA: A theory of concurrent processes with non-determinism, priorities, probabilities and time. Theoretical Computer Science, 202:1–54, 1998. [44] E. Best, R. Devillers, and M. Koutny: A unified model for nets and process algebras. In [42], pp. 945–1045, 2001. [45] E. Brinksma (editor): Information Processing Systems, Open Systems Interconnection, LOTOS – A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour, volume IS-8807 of International Standard. ISO, Geneva, 1989. [46] S.D. Brookes, C.A.R. Hoare, and A.W. Roscoe: A theory of communicating sequential processes. Journal of the ACM, 31(3):560–599, 1984. [47] O. Burkart, D. Caucal, F. Moller, and B. Steffen: Verification on infinite structures. In [42], pp. 545–623, 2001. [48] L. Cardelli and A.D. Gordon: Mobile ambients. Theoretical Computer Science, 240:177–213, 2000. [49] P.J.L. Cuijpers and M.A. Reniers: Hybrid process algebra. Technical Report CS-R 03/07, Technische Universiteit Eindhoven, Dept. of Comp. Sci., 2003. 334 [50] P.R. D’Argenio: Algebras and Automata for Timed and Stochastic Systems. PhD thesis, University of Twente, 1999. [51] J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden: Metrics for labeled Markov systems. In J.C.M. Baeten and S. Mauw, editors, Proceedings CONCUR’99, number 1664 in Lecture Notes in Computer Science, pages 258– 273. Springer Verlag, 1999. [52] E.W. Dijkstra: Guarded commands, nondeterminacy, and formal derivation of programs. Communications of the ACM, 18(8):453– 457, 1975. [53] U. Engberg and M. Nielsen: A calculus of communicating systems with label passing. Technical Report DAIMI PB-208, Aarhus University, 1986. [54] J.-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu: CADP (CAESAR/ALDEBARAN development package): A protocol validation and verification toolbox. In R. Alur and T.A. Henzinger, editors, Proceedings CAV ’96, number 1102 in Lecture Notes in Computer Science, pages 437–440. Springer Verlag, 1996. [55] R.W. Floyd: Assigning meanings to programs. In J.T. Schwartz, editor, Proceedings Symposium in Applied Mathematics, Mathematical Aspects of Computer Science, pages 19–32. AMS, 1967. [56] R.J. van Glabbeek: The linear time – branching time spectrum II; the semantics of sequential systems with silent moves. In E. Best, editor, Proceedings CONCUR ’93, number 715 in Lecture Notes in Computer Science, pages 66–81. Springer Verlag, 1993. [57] R.J. van Glabbeek: What is branching time semantics and why to use it? In M. Nielsen, editor, The Concurrency Column, pages 190–198. Bulletin of the EATCS 53, 1994. |