Teaching Formal Models of Concurrency Specification and Analysis
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 opportun...
Saved in:
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2015-12-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/295 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849240833302200320 |
|---|---|
| author | N. V. Shilov |
| author_facet | N. V. Shilov |
| author_sort | N. V. Shilov |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-dd7df88bc0ee4448bd0f8e619d284cc1 |
| institution | Kabale University |
| issn | 1818-1015 2313-5417 |
| language | English |
| publishDate | 2015-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj-art-dd7df88bc0ee4448bd0f8e619d284cc12025-08-20T04:00:26ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172015-12-0122678379410.18255/1818-1015-2015-6-783-794273Teaching Formal Models of Concurrency Specification and AnalysisN. V. Shilov0A.P. Ershov Institute of Informatics Systems SD RASThere 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.https://www.mais-journal.ru/jour/article/view/295concurrency and parallelismformal methodsformal modelspetri netscalculi for communicating systemslabeled transition systemsreachability problemtemporal logicmodel checking |
| spellingShingle | N. V. Shilov Teaching Formal Models of Concurrency Specification and Analysis Моделирование и анализ информационных систем concurrency and parallelism formal methods formal models petri nets calculi for communicating systems labeled transition systems reachability problem temporal logic model checking |
| title | Teaching Formal Models of Concurrency Specification and Analysis |
| title_full | Teaching Formal Models of Concurrency Specification and Analysis |
| title_fullStr | Teaching Formal Models of Concurrency Specification and Analysis |
| title_full_unstemmed | Teaching Formal Models of Concurrency Specification and Analysis |
| title_short | Teaching Formal Models of Concurrency Specification and Analysis |
| title_sort | teaching formal models of concurrency specification and analysis |
| topic | concurrency and parallelism formal methods formal models petri nets calculi for communicating systems labeled transition systems reachability problem temporal logic model checking |
| url | https://www.mais-journal.ru/jour/article/view/295 |
| work_keys_str_mv | AT nvshilov teachingformalmodelsofconcurrencyspecificationandanalysis |