Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
didattica:magistrale:atse:ay_1718:main [2018/06/02 08:27] michele [Study Material] |
didattica:magistrale:atse:ay_1718:main [2020/09/17 16:55] (current) |
||
---|---|---|---|
Line 70: | Line 70: | ||
* Lecture 18/04/2018 [[https://unicam.webex.com/unicam/ldr.php?RCID=6dbc3969290337b53b00aed35dac0fd6 |View]][[https://unicam.webex.com/unicam/lsr.php?RCID=2d659b74913e116cc7e8ae8cef6bf881 |Download]] | * Lecture 18/04/2018 [[https://unicam.webex.com/unicam/ldr.php?RCID=6dbc3969290337b53b00aed35dac0fd6 |View]][[https://unicam.webex.com/unicam/lsr.php?RCID=2d659b74913e116cc7e8ae8cef6bf881 |Download]] | ||
* Lecture 09/05/2018 Statistical Analysis of Systems | * Lecture 09/05/2018 Statistical Analysis of Systems | ||
- | * Lecture 10/05/2018 {{ :didattica:magistrale:atse:ay_1718:1-s2.0-s1877050916319895-main.pdf |Hypothesis Testing}} | + | * Lecture 10/05/2018 {{ :didattica:magistrale:atse:ay_1718:10.1007_s10009-014-0350-1.pdf |Hypothesis Testing}} |
* Lecture 16/05/2018 A language for System monitoring (Part I) [[http://www-verimag.imag.fr/~maler/Papers/monitor-sttt.pdf|Reference]] | * Lecture 16/05/2018 A language for System monitoring (Part I) [[http://www-verimag.imag.fr/~maler/Papers/monitor-sttt.pdf|Reference]] | ||
- | * Lecture 17/05/2018 (3 h) A language for System monitoring (Part II) | + | * Lecture 17/05/2018 (3 h) A language for System monitoring (Part II) [[https://unicam.webex.com/unicam/ldr.php?RCID=bb6e552f99a7d64ce3fa2070023e8b4b|View]] [[https://unicam.webex.com/unicam/lsr.php?RCID=0a893445427b8a5586f5b02c17e41c1f |Download]] |
- | * Lecture 30/01/2018 Quantitative semantics of STL (Part I) [[http://www-verimag.imag.fr/~maler/Papers/STLRobustAlgo.pdf|Reference]] | + | * Lecture 30/01/2018 Quantitative semantics of STL (Part I) [[http://www-verimag.imag.fr/~maler/Papers/STLRobustAlgo.pdf|Reference]] [[https://unicam.webex.com/unicam/ldr.php?RCID=686ebc432a2d89bf827f95155a4dcbd4|View]] [[https://unicam.webex.com/unicam/lsr.php?RCID=af42661f9625c1f7bc4e64948fa4b428 |Download]] |
* Lecture 31/01/2018 (3 h) Quantitative semantics of STL (Part II) [[https://unicam.webex.com/unicam/ldr.php?RCID=6b376cb123e82dc6ca1c4a72d8391cdd|View]] [[https://unicam.webex.com/unicam/lsr.php?RCID=ad98f708709d092f8691d356cf7b2694 |Download]] | * Lecture 31/01/2018 (3 h) Quantitative semantics of STL (Part II) [[https://unicam.webex.com/unicam/ldr.php?RCID=6b376cb123e82dc6ca1c4a72d8391cdd|View]] [[https://unicam.webex.com/unicam/lsr.php?RCID=ad98f708709d092f8691d356cf7b2694 |Download]] | ||
+ | * Lecture 06/06/2018 Stochastic Process Algebras: ([[http://www.dcs.ed.ac.uk/pepa/|PEPA]]) ([[http://lanther.co.uk/papers/FM2009.pdf|paper]]) ([[http://www.dcs.ed.ac.uk/pepa/tools/plugin/index.html|Tool]]) [[https://unicam.webex.com/unicam/ldr.php?RCID=0f809f09cd3550ea7ea5374139e27926 |View]] [[https://unicam.webex.com/unicam/lsr.php?RCID=4126b9fe0d57c731623693eb02331ed7 |Download]] | ||
+ | * Lecture 06/06/2018 (4h) Stochastic Process Algebras: CARMA ({{ :didattica:magistrale:atse:ay_1718:slides_carma.pdf |slides}}) ([[http://lanther.co.uk/papers/FM2009.pdf|paper]]) ([[http://quanticol.github.io/CARMA/|Tool]]) ({{ :didattica:magistrale:atse:ay_1718:carmatutorial.pdf |docs}})[[https://unicam.webex.com/unicam/ldr.php?RCID=c3120e1b317e16fc658a2faaf7642e49 |View]] [[https://unicam.webex.com/unicam/lsr.php?RCID=e8ba63cfb73da0e51ba30fc4f9b886bc |Download]] | ||
- | **Textbooks** | ||
- | * Teacher's notes. | ||
</WRAP> | </WRAP> | ||
---- | ---- | ||
Line 83: | Line 83: | ||
<WRAP box round center 95%> | <WRAP box round center 95%> | ||
**Exam Dates** | **Exam Dates** | ||
+ | * 27/06/2018, 9.00 (Teacher Office) | ||
+ | * 10/07/2018, 9.00 (Teacher Office) | ||
+ | |||
+ | **Exam rules**: Each student select one of the following topics and produces a short report (between 5 and 10 pages) that will be presented at the exam: | ||
+ | * {{ :didattica:magistrale:atse:ay_1718:10.1007_s10009-014-0350-1.pdf |Statistical Model Checking}} | ||
+ | * [[https://arxiv.org/abs/1506.08234|Robust Online Monitoring of Signal Temporal Logic]] | ||
+ | * [[https://www.sciencedirect.com/science/article/pii/S0304397515002224?via%3Dihub| System design of stochastic models using robustness of temporal properties]] | ||
+ | * Use of PEPA ([[http://www.dcs.ed.ac.uk/pepa/tools/plugin/|link]]) to model one of the scenarios described below | ||
+ | * Use of CARMA ([[http://quanticol.github.io|link]])to model one of the scenarios described below | ||
+ | |||
+ | **Scenarios** | ||
+ | * [[https://en.wikipedia.org/wiki/Compartmental_models_in_epidemiology|Epidemic Model]] | ||
+ | * [[http://www.prismmodelchecker.org/casestudies/virus.phpVirus|Diffusion Model]] | ||
+ | * [[https://en.wikipedia.org/wiki/Lotka–Volterra_equations|Predator-Prey Model]] | ||
+ | * [[http://www.prismmodelchecker.org/casestudies/asynchronous_leader.php|Asynchronous Leader Election]] | ||
- | **Exam rules**: | ||
- | |||
** Results ** | ** Results ** | ||
* N/A | * N/A | ||
</WRAP> | </WRAP> | ||
- | |||
- |