Teaching Formal Models of Concurrency Specification and Analysis
https://doi.org/10.18255/1818-1015-2015-6-783-794
Abstract
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.
About the Author
N. V. Shilov
A.P. Ershov Institute of Informatics Systems SD RAS
Russian Federation
PhD, Lavrent’ev av., 6, Novosibirsk, 630090
Russian Federation
PhD, Lavrent’ev av., 6, Novosibirsk, 630090
References
1. Handbook of Process Algebra, eds. J. A. Bergstra, A. Ponse, S. A. Smolka, Elsevier, Amsterdam, 2001.
2. L. Cardelli, A. D. Gordon, “Mobile ambient”, Lecture Notes in Computer Science, 1378, Springer-Verlag, Berlin, Heidelberg, 1998, 140–155.
3. 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.
4. E. M. Jr. Clarke, O. Grumberg, D. A. Peled, Model Checking, MIT Press, Cambridge, Massachusetts, 1999.
5. R.W. Floyd, “The paradigms of Programming”, Communications of ACM, 22 (1979), 455–460.
6. 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.
7. 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/).
8. Yu. G. Karpov, Model Checking. Verificaciya parallelnyh i raspredelennyh programmnyh system, BHV-Peterburg, Saint Petersburg, 2010, (In Russian).
9. V. E. Kotov, Seti Petri, Nauka, Moscow, Russia, 1987, (In Russian).
10. Z. Manna, A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag,, New York, 1992.
11. T. S. Kuhn, The structure of Scientific Revolutions, Univ. of Chicago Press, Chicago and London, 1996, (3rd Edition).
12. R. Milner, Communicating and Mobile Systems: the Pi-Calculus, Cambridge University Press, Cambridge, England, 1999.
13. R. Milner, A Calculus of Communicating Systems, Lecture Notes in Computer Science, 92, Springer-Verlag, Berlin, Heidelberg, 1980.
14. J. L. Peterson, Petri Net Theory and the Modeling of Systems, Prentice Hall, Upper Saddle River, New Jersey, 1981.
15. W. Reisig, A Primer in Petri Net Design, Springer-Verlag, Berlin, Heidelberg, 1992.
16. 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.
17. 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.
18. 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.
19. C. Stirling, Modal and Temporal Properties of Processes, Springer-Verlag, New York, 2001.
Review
For citations:
Shilov N.V. Teaching Formal Models of Concurrency Specification and Analysis. Modeling and Analysis of Information Systems. 2015;22(6):783-794. (In Russ.) https://doi.org/10.18255/1818-1015-2015-6-783-794
Views:
1046
Email this article 