maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2015-6-783-794mais-295Research ArticleОригинальные статьиArticlesО преподавании формальных моделей и алгоритмов анализа параллельных системTeaching Formal Models of Concurrency Specification and AnalysisШиловН. В.ShilovN. V.

канд. физ.-мат. наук, старший научный сотрудник,

630090 г. Новосибирск, пр. Лаврентьева, 6

PhD, Lavrent’ev av., 6, Novosibirsk, 630090

shilov@iis.nsk.suИнститут систем информатики им. А. П. Ершова СО РАНРоссияA.P. Ershov Institute of Informatics Systems SD RASRussian Federation201520122015226783794Copyright © Шилов Н.В., 20152015Шилов Н.В.Shilov N.V.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/295

В настоящее время наблюдается огромный практический интерес к параллельному программированию. Этот интерес обусловлен доступностью супер-ЭВМ, компьютерных кластеров и мощных графических процессоров для массового использования в вычислительной математике и компьютерном моделировании. Кроме того, такие технологии параллельного программирования, как MPI, OpenMP и CUDA, позволяют использовать безопасным образом опыт программирования на классических языках Си и FORTRAN для ускорения вычислений, избегая конфликтов (“гонок”) из-за ресурсов. Однако такой прогресс параллельного программирования не означает, что конкуренция из-за ресурсов не может возникать в параллельных общего вида, в так называемых распределенных системах в частности. Поэтому остается актуальным изучение и преподавание формальных моделей параллелизма и средств верификации поведенческих свойств параллельных (распределенных) систем. В статье представлен опыт преподавания специального курса по формальным моделям параллелизма для магистрантов и аспирантов, специализирующихся в области высокопроизводительных вычислений. Сначала в статье дан обзор курса в целом, предварительных знаний, необходимых для этого курса, целей и задач курса, представлен план лекций и список рекомендованной литературы. Затем представлен пример одной поучительной головоломки (на достижимость в пространстве состояний) и ее формализации средствами семантических, синтаксических и логических моделей, как-то: сетями Петри, средствами исчисления параллельных взаимодействующих процессов (CCS) и темпоральной логики CTL. Эта головоломка — хороший пример для того, чтобы показать специфику и пользу каждого из рассмотренных формализмов.

Статья представляет собой расширенную версию доклада на VI Международном семинаре “Program Semantics, Specification and Verification: Theory and Applications”, Казань, 2015.

Статья публикуется в авторской редакции.

There is a widespread and rapidly growing interest to the parallel programming nowadays. This interest is based on availability of supercomputers, computer clusters and powerful graphic processors for computational mathematics and simulation. MPI, OpenMP, CUDA and other technologies provide opportunity to write C and FORTRAN code for parallel speed-up of execution without races for resources. Nevertheless concurrency issues (like races) are still very important for parallel systems in general and distributed systems in particular. Due to this reason, there is a need of research, study and teaching of formal models of concurrency and methods of distributed system verification.

The paper presents an individual experience with teaching Formal Models of Concurrency as a graduate elective course for students specializing in high-performance computing. First it sketches course background, objectives, lecture plan and topics. Then the paper presents how to formalize (i.e. specify) a reachability puzzle in semantic, syntactic and logic formal models, namely: in Petri nets, in a dialect of Calculus of Communicating Systems (CCS) and in Computation Tree Logic (CTL). This puzzle is a good educational example to present specifics of different formal notations.

The article is published in the author’s wording.

системы с параллелизмомформальные методыформальные моделисети Петриисчисления взаимодействующих процессовпомеченные системы переходовпроблема достижимоститемпоральная логикаверификация моделейconcurrency and parallelismformal methodsformal modelsPetri netscalculi for communicating systemslabeled transition systemsreachability problemtemporal logicmodel checkingПрограмма IV.39.1 «Теоретические и прикладные проблемы создания эффективных надежных программных систем и информационных технологий»ReferencesHandbook of Process Algebra, eds. J. A. Bergstra, A. Ponse, S. A. Smolka, Elsevier, Amsterdam, 2001.Handbook of Process Algebra, eds. J. A. Bergstra, A. Ponse, S. A. Smolka, Elsevier, Amsterdam, 2001.L. Cardelli, A. D. Gordon, “Mobile ambient”, Lecture Notes in Computer Science, 1378, Springer-Verlag, Berlin, Heidelberg, 1998, 140–155.L. Cardelli, A. D. Gordon, “Mobile ambient”, Lecture Notes in Computer Science, 1378, Springer-Verlag, Berlin, Heidelberg, 1998, 140–155.L. Cardelli, “Mobility and Security.”, Foundations of Secure Computation, Proceedings of the NATO Advanced Study Institute on Foundations of Secure Computation, IOS Press, Amsterdam, 2000, 3–37.L. Cardelli, “Mobility and Security.”, Foundations of Secure Computation, Proceedings of the NATO Advanced Study Institute on Foundations of Secure Computation, IOS Press, Amsterdam, 2000, 3–37.E. M. Jr. Clarke, O. Grumberg, D. A. Peled, Model Checking, MIT Press, Cambridge, Massachusetts, 1999.E. M. Jr. Clarke, O. Grumberg, D. A. Peled, Model Checking, MIT Press, Cambridge, Massachusetts, 1999.R.W. Floyd, “The paradigms of Programming”, Communications of ACM, 22 (1979), 455–460.R.W. Floyd, “The paradigms of Programming”, Communications of ACM, 22 (1979), 455–460.D. Grossman, “Ready-For-Use: 3 Weeks of Parallelism and Concurrency in a Required Second-Year Data-Structures Course”, SPLASH 2010 Workshop on Curricula for Concurrency and Parallelism (Reno, Nevada, USA, Oct. 17, 2010), https://homes.cs.washington.edu/~djg/papers/grossmanSPAC_position2010.pdf.D. Grossman, “Ready-For-Use: 3 Weeks of Parallelism and Concurrency in a Required Second-Year Data-Structures Course”, SPLASH 2010 Workshop on Curricula for Concurrency and Parallelism (Reno, Nevada, USA, Oct. 17, 2010), https://homes.cs.washington.edu/~djg/papers/grossmanSPAC_position2010.pdf.C. A. R. Hoare, Communicating Sequential Processes, Prentice Hall, Upper Saddle River, New Jersey, 1985, (This book was updated by Jim Davies at the Oxford University Computing Laboratory in 2004 and the new edition is available at the http://www.usingcsp.com/).C. A. R. Hoare, Communicating Sequential Processes, Prentice Hall, Upper Saddle River, New Jersey, 1985, (This book was updated by Jim Davies at the Oxford University Computing Laboratory in 2004 and the new edition is available at the http://www.usingcsp.com/).Yu. G. Karpov, Model Checking. Verificaciya parallelnyh i raspredelennyh programmnyh system, BHV-Peterburg, Saint Petersburg, 2010, (In Russian).Yu. G. Karpov, Model Checking. Verificaciya parallelnyh i raspredelennyh programmnyh system, BHV-Peterburg, Saint Petersburg, 2010, (In Russian).V. E. Kotov, Seti Petri, Nauka, Moscow, Russia, 1987, (In Russian).V. E. Kotov, Seti Petri, Nauka, Moscow, Russia, 1987, (In Russian).Z. Manna, A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag,, New York, 1992.Z. Manna, A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag,, New York, 1992.T. S. Kuhn, The structure of Scientific Revolutions, Univ. of Chicago Press, Chicago and London, 1996, (3rd Edition).T. S. Kuhn, The structure of Scientific Revolutions, Univ. of Chicago Press, Chicago and London, 1996, (3rd Edition).R. Milner, Communicating and Mobile Systems: the Pi-Calculus, Cambridge University Press, Cambridge, England, 1999.R. Milner, Communicating and Mobile Systems: the Pi-Calculus, Cambridge University Press, Cambridge, England, 1999.R. Milner, A Calculus of Communicating Systems, Lecture Notes in Computer Science, 92, Springer-Verlag, Berlin, Heidelberg, 1980.R. Milner, A Calculus of Communicating Systems, Lecture Notes in Computer Science, 92, Springer-Verlag, Berlin, Heidelberg, 1980.J. L. Peterson, Petri Net Theory and the Modeling of Systems, Prentice Hall, Upper Saddle River, New Jersey, 1981.J. L. Peterson, Petri Net Theory and the Modeling of Systems, Prentice Hall, Upper Saddle River, New Jersey, 1981.W. Reisig, A Primer in Petri Net Design, Springer-Verlag, Berlin, Heidelberg, 1992.W. Reisig, A Primer in Petri Net Design, Springer-Verlag, Berlin, Heidelberg, 1992.P. van Roy, “Programming Paradigms for Dummies: What Every Programmer Should Know”, New Computational Paradigms for Computer Music,, eds. G. Assayag, A. Gerzso, IRCAM/Delatour, France, 2009, 9–38.P. van Roy, “Programming Paradigms for Dummies: What Every Programmer Should Know”, New Computational Paradigms for Computer Music,, eds. G. Assayag, A. Gerzso, IRCAM/Delatour, France, 2009, 9–38.N. V. Shilov, K. Yi, “How to Find a Coin: Propositional Program Logics Made Easy”, Current Trends in Theoretical Computer Science. V. 2, World Scientific, Singapore, 2004, 181–214.N. V. Shilov, K. Yi, “How to Find a Coin: Propositional Program Logics Made Easy”, Current Trends in Theoretical Computer Science. V. 2, World Scientific, Singapore, 2004, 181–214.N. V. Shilov et al., “Development of the Computer Language Classification Knowledge Portal”, Ershov Informatics Conference PSI’11, Lecture Notes in Computer Science, 7162, Springer-Verlag, Berlin, Heidelberg, 2012, 340–348.N. V. Shilov et al., “Development of the Computer Language Classification Knowledge Portal”, Ershov Informatics Conference PSI’11, Lecture Notes in Computer Science, 7162, Springer-Verlag, Berlin, Heidelberg, 2012, 340–348.C. Stirling, Modal and Temporal Properties of Processes, Springer-Verlag, New York, 2001.C. Stirling, Modal and Temporal Properties of Processes, Springer-Verlag, New York, 2001.

The authors declare that there are no conflicts of interest present.