Geodesic
Teaching formal models of concurrency specification and analysis
Modelirovanie i analiz informacionnyh sistem, Tome 22 (2015) no. 6, pp. 783-794.

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: concurrency and parallelism, formal methods, formal models, Petri nets, calculi for communicating systems, labeled transition systems, reachability problem, temporal logic, model checking. 
@article{MAIS_2015_22_6_a4,
     author = {N. V. Shilov},
     title = {Teaching formal models of concurrency specification and analysis},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {783--794},
     publisher = {mathdoc},
     volume = {22},
     number = {6},
     year = {2015},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2015_22_6_a4/}
}
TY  - JOUR
AU  - N. V. Shilov
TI  - Teaching formal models of concurrency specification and analysis
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2015
SP  - 783
EP  - 794
VL  - 22
IS  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2015_22_6_a4/
LA  - en
ID  - MAIS_2015_22_6_a4
ER  - 
%0 Journal Article
%A N. V. Shilov
%T Teaching formal models of concurrency specification and analysis
%J Modelirovanie i analiz informacionnyh sistem
%D 2015
%P 783-794
%V 22
%N 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2015_22_6_a4/
%G en
%F MAIS_2015_22_6_a4
N. V. Shilov. Teaching formal models of concurrency specification and analysis. Modelirovanie i analiz informacionnyh sistem, Tome 22 (2015) no. 6, pp. 783-794. http://geodesic.mathdoc.fr/item/MAIS_2015_22_6_a4/

[1] J. A. Bergstra, A. Ponse, S. A. Smolka (eds.), Handbook of Process Algebra, Elsevier, Amsterdam, 2001 | MR | Zbl

[2] L. Cardelli, A. D. Gordon, “Mobile ambient”, Lecture Notes in Computer Science, 1378, Springer-Verlag, Berlin–Heidelberg, 1998, 140–155 | DOI

[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 | Zbl

[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 | DOI

[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/d̃jg/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/ | MR | Zbl

[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, M., 1987 (In Russian) | MR

[10] Z. Manna, A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, New York, 1992 | MR

[11] T. S. Kuhn, The structure of Scientific Revolutions, 3rd Edition, Univ. of Chicago Press, Chicago–London, 1996

[12] R. Milner, Communicating and Mobile Systems: the Pi-Calculus, Cambridge University Press, Cambridge, England, 1999 | MR | Zbl

[13] R. Milner, A Calculus of Communicating Systems, Lecture Notes in Computer Science, 92, Springer-Verlag, Berlin–Heidelberg, 1980 | DOI | MR | Zbl

[14] J. L. Peterson, Petri Net Theory and the Modeling of Systems, Prentice Hall, Upper Saddle River, New Jersey, 1981 | MR

[15] W. Reisig, A Primer in Petri Net Design, Springer-Verlag, Berlin–Heidelberg, 1992 | Zbl

[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 | DOI

[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 | DOI

[19] C. Stirling, Modal and Temporal Properties of Processes, Springer-Verlag, New York, 2001