====== Advanced Topics in Software Engineering - Software testing ======
----
===== News =====
<WRAP center round important 95%>
  * **<wrap em>29/03/2018</wrap>** All the students that want to give this exams in the Academic Year 17/18, must send an email to the teacher! 
  * **<wrap em>29/03/2018</wrap>** No lecture today! 
  * **07/03/2018** Lectures start! 
</WRAP>

----
===== General Information =====
<WRAP box round 95% center>
**Teacher**: 
  * Michele Loreti
**Lessons schedule**:
  * Wednesday, 11.00 - 13.00, Room AB1, Polo Lodovici;
  * Thursday, 11.00 - 13.00,  Room AB1, Polo Lodovici.
</WRAP>
----
===== Course Objectives =====

<WRAP box round 95% center>
In the course various aspects of computer-aided modelling for performance evaluation of (stochastic) dynamic systems will be introduced. The emphasis is on stochastic modelling of computer systems and communication networks; however other dynamic systems such as Collective Adaptive Systems and Cyber Physical Systems  will also be considered. Different tools and techniques will be introduced to predict (or monitoring) system performance at the different stages of development. 
</WRAP>

----
===== Course Contents =====

<WRAP round 95% center box>
  - Modelling and Simulation
  - Operational Laws
  - Constructing and Solving Markov Processes
  - More Complex Markov Processes
  - Queueing Networks
  - Population Models
  - Specification languages: Stochastic process Algebras
  - Simulation Models: Introduction and Motivation
  - Random Variables and Simulation
  - Property specification
  - Statistical Analysis of Systems
  - Scalable analysis techniques
  - Model Validation and Verification
  - Parameterisation and Workload Characterisation
  - Monitoring and Runtime Verification
</WRAP>
----
===== Study Material =====
<WRAP box round center 95%>
**Course Slides**
  * {{ :didattica:magistrale:atse:ay_1718:01slides_v2.pdf | Slides 01: Introduction and Basic Principles of Performance Modelling.}}
  * {{ :didattica:magistrale:atse:ay_1718:02slides_v2.pdf | Slides 02: Operational Laws.}}
  * {{ :didattica:magistrale:atse:ay_1718:03slides.pdf | Slides 03: Markov Chains. }}

**Lectures**
  * Lecture 7/3/2018 [[https://unicam.webex.com/unicam/ldr.php?RCID=fbb0bc80fc57089833c0c4c1300560a8|View]] [[https://unicam.webex.com/unicam/lsr.php?RCID=e788d0f4f567f3e63ca2d69b5407647a |Download]]
  * Lecture 8/3/2018 [[https://unicam.webex.com/unicam/ldr.php?RCID=392d5c3e73545129ea5b30aeacebbc8f|View]] [[https://unicam.webex.com/unicam/lsr.php?RCID=947969c9c30c82a67bbdfe083ce0a060 |Download]]
  * Lecture 14/3/2018 [[https://unicam.webex.com/unicam/ldr.php?RCID=b2064b1672051cddb16cf3e5c81728cb|View]] [[https://unicam.webex.com/unicam/lsr.php?RCID=abe6cb338c52a7296059da035e5c7ba2 |Download]]
  * Lecture 21/3/2018 [[https://unicam.webex.com/unicam/ldr.php?RCID=0f6d3ea736f5072ec73c0dc3897d0421 |View]] [[https://unicam.webex.com/unicam/lsr.php?RCID=03e7e9ed7d39613fd33d5799a9788854 |Download]]
  * Lecture 22/3/2018 [[https://unicam.webex.com/unicam/ldr.php?RCID=11c7e16f6a9d66fb651692652fa592b9 |View]] [[https://unicam.webex.com/unicam/lsr.php?RCID=687811445aaf477889b63070a3710e75 |Download]]
    * C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008 (Sec. 10.1).
  * Lecture 4/4/2018 [[https://unicam.webex.com/unicam/ldr.php?RCID=ab9c15cc18506cf0ebb087b3eb3a5428 |View]] [[https://unicam.webex.com/unicam/lsr.php?RCID=e57e85fcd59117560c2d80f092fde4a2 |Download]]
    * [[http://www.columbia.edu/~ww2040/6711F13/CTMCnotes120413.pdf|CTMC Transient Analysis, Chapters 1-5]]
    * [[https://web.stanford.edu/~glynn/papers/1988/FG88.pdf|Fox-Glynn algorithm and Uniformization]]
  * Lecture 5/4/2018 [[https://unicam.webex.com/unicam/ldr.php?RCID=01e2c42f9fc2078048237fd6cf409322 |View]] [[https://unicam.webex.com/unicam/lsr.php?RCID=0bc883220b682205c814efcdccfd4e2f |Download]]
    * {{ :didattica:magistrale:atse:ay_1718:lecture_18_4_5.pdf | Whiteboard }}
    * [[https://www.sciencedirect.com/science/article/pii/S0166531613000023?via%3Dihub|Population Models]] (Sections 3.1 and 3.2).
  * Lecture 12/04/2018 [[https://unicam.webex.com/unicam/ldr.php?RCID=374a4fb0172c8db5511832b2f6921dd9| View]] [[https://unicam.webex.com/unicam/lsr.php?RCID=78ff351173183d20f4fa089afad6795c |Download]] 
    * [[https://en.wikipedia.org/wiki/Inverse_transform_sampling|Inverse transform sampling]]
    * [[https://en.wikipedia.org/wiki/Kinetic_Monte_Carlo|Kinetic Monte Carlo]]
  * 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 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 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]] [[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 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]]

</WRAP>
----
===== Exams =====
<WRAP box round center 95%>
**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]]


** Results **
  * N/A
</WRAP>