Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision | ||
|
didattica:magistrale:fmsis:main [2018/03/06 10:59] 127.0.0.1 external edit |
— (current) | ||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== Formal Modeling of Software Intensive Systems ====== | ||
| - | ---- | ||
| - | ===== News ===== | ||
| - | <WRAP center round important 95%> | ||
| - | * <wrap em>March 6th: first lecture</wrap> | ||
| - | </WRAP> | ||
| - | ---- | ||
| - | ===== General Info ===== | ||
| - | <WRAP box round 95% center> | ||
| - | **Teacher**: | ||
| - | * [[http://docenti.unicam.it/pdett.aspx?ids=N&tv=d&UteId=990&ru=PA|Francesco Tiezzi]] | ||
| - | |||
| - | **Lessons schedule**: | ||
| - | * Tuesday 11 - 13 (LA1 room) | ||
| - | * Wednesday 9 - 11 (LA1 room) | ||
| - | |||
| - | **Students Office hours**: | ||
| - | * on appointment (via email), second floor of Polo Lodovici, via Madonna delle Carceri 9, Camerino | ||
| - | </WRAP> | ||
| - | ---- | ||
| - | ===== Course Objectives ===== | ||
| - | |||
| - | <WRAP box round 95% center> | ||
| - | D1 – KNOWLEDGE AND UNDERSTANDING\\ | ||
| - | At the end of the course, the student should be able to:\\ | ||
| - | - Have the knowledge of the issues concerning concurrent/distributed programming and the modelling of hardware/software systems as software-intensive systems. | ||
| - | - Have the knowledge of the semantics of the operators of the process algebras CCS, CSP and ACP. | ||
| - | - Have the knowledge of the syntax and the semantics of the modal logic Hennessy-Milner Logic (HML), with and without recursion, and of the ACTL logic. | ||
| - | - Have the knowledge of the main observational behavioural equivalences, weak and strong. | ||
| - | - Have the knowledge of the tools for the automatic verification of software-intensive systems modelled by means of process algebras. | ||
| - | |||
| - | D2 – APPLYING KNOWLEDGE AND UNDERSTANDING\\ | ||
| - | At the end of the course, the student should be able to:\\ | ||
| - | - Modelling a software-intensive system using the formal languages presented in the course, using a compositional approach. | ||
| - | - Derive the labelled transition system associated to a process. | ||
| - | - Decide if one or more state of a labelled transition system are stong or weak bisimilar, providing a suitable bisimulation relation whereas possible. | ||
| - | - Decide if one or more states of a labelled transition system satisfy formulas of HML and ACTL logics. | ||
| - | - Define temporal properties of a software-intensive system using the HML and ACTL logics. | ||
| - | - Use a specific software tool for the analysis of software-intensive systems modelled using the CCS language or other formalism. | ||
| - | |||
| - | D3 – MAKING JUDGEMENTS\\ | ||
| - | At the end of the course, the student should be able to:\\ | ||
| - | - Identify the best model suitable for describing a system using a given formalism. | ||
| - | |||
| - | D4 - COMMUNICATION SKILLS\\ | ||
| - | At the end of the course, the student should be able to:\\ | ||
| - | - Write a clear report on the modelling and analysis of a system under study using a formal style. | ||
| - | - Write a brief survey and state of the art about a given research topic by searching the scientific literature. | ||
| - | |||
| - | D5 – LEARNING SKILLS\\ | ||
| - | At the end of the course, the student should be able to:\\ | ||
| - | - Search the scientific literature for specific advances in formalisms and tools aimed at modelling and verifying software-intensive systems. | ||
| - | - Autonomously understand and learn to use new features added to tools for modelling and verifying software-intensive systems. | ||
| - | </WRAP> | ||
| - | |||
| - | ---- | ||
| - | ===== Course Contents ===== | ||
| - | |||
| - | <WRAP round 95% center box> | ||
| - | * Introductory concepts: concurrent, reactive and software-intensive systems | ||
| - | * Preliminary mathematical concepts | ||
| - | * Semantics of the operators of the process algebras CCS, CSP and ACP | ||
| - | * The Maude toolset | ||
| - | * Main behavioural equivalences, weak and strong | ||
| - | * Hennessy-Milner Logic and ACTL | ||
| - | * Software tools for the automatic verification of software-intensive systems modelled by means of process algebras: TAPAs and muCRL2 | ||
| - | </WRAP> | ||
| - | ---- | ||
| - | ===== Study material ===== | ||
| - | <WRAP box round center 95%> | ||
| - | **Course Slides** | ||
| - | * Introduction and general information | ||
| - | * Preliminaries | ||
| - | |||
| - | |||
| - | **Lectures** | ||
| - | * 6 March | ||
| - | |||
| - | **Reference books**\\ | ||
| - | The main material of the course consists of: | ||
| - | * Rocco De Nicola. A gentle introduction to Process Algebras. Notes obtained by the restructuring of two entries (Process Algebras - Behavioural Equivalences) of Encyclopedia of Parallel Computing, David A. Padua (Ed.). Springer 2011; pp. 120-127 and pp. 1624-1636. | ||
| - | * Luca Aceto, Anna Ingolfsdottir, Kim Guldstrand Larsen and Jiri Srba, "Reactive Systems. Modelling, Specification and Verification", Cambridge University Press, 2007. ISBN: 9780521875462. Website of the book with additional material available: http://rsbook.cs.aau.dk | ||
| - | |||
| - | Morover, lecture notes, papers and slides may be provided in this website. | ||
| - | |||
| - | The Maude tool can be downloaded for free for academic use, together with documentation and tutorials, from the website: http://maude.cs.illinois.edu/ | ||
| - | |||
| - | The TAPAs tool can be downloaded for free for academic use, together with documentation and tutorials, from the website: http://rap.dsi.unifi.it/tapas/ | ||
| - | |||
| - | The mCRL2 tool can be downloaded for free for academic use, together with documentation and tutorials, from the website: http://www.mcrl2.org/release/user_manual/index.html | ||
| - | |||
| - | </WRAP> | ||
| - | ---- | ||
| - | ===== Exams ===== | ||
| - | <WRAP box round center 95%> | ||
| - | **Exam Dates A.Y. 2016/2017** | ||
| - | * Appello I: 28/02/2017 ore 14:00 - Polo Lodovici - AB1 | ||
| - | * Appello II: 16/03/2017 ore 14:00 - Polo Lodovici - AB1 | ||
| - | * Appello III: 05/06/2017 ore 10:00 - Polo Lodovici | ||
| - | * Appello IV: 07/07/2017 ore 10:00 - Polo Lodovici | ||
| - | * Appello V: 21/07/2017 ore 10:00 - Polo Lodovici | ||
| - | * Appello VI: 06/09/2017 ore 10:00 - Polo Lodovici | ||
| - | * Appello VII: 20/09/2017 ore 10:00 - Polo Lodovici | ||
| - | * Appello VIII: 02/10/2017 ore 10:00 - Polo Lodovici | ||
| - | |||
| - | **Results of the written in itinere test of 3/2/2017** | ||
| - | * 098875: 30 | ||
| - | * 098434: 30 | ||
| - | * 099978: 30 | ||
| - | * 098702: 30 | ||
| - | * 098443: 29 | ||
| - | * 098543: 29 | ||
| - | * 098442: 27 | ||
| - | * 098541: 27 | ||
| - | * 098438: 25 | ||
| - | * 097946: 25 | ||
| - | * 098431: 21 | ||
| - | * 098437: 19 | ||
| - | |||
| - | **Results of the written in itinere test of 3/2/2017** | ||
| - | * 098875 26 | ||
| - | * 098434 26 | ||
| - | * 099978 30 | ||
| - | * 098702 27 | ||
| - | * 098443 26 | ||
| - | * 098543 26 | ||
| - | * 098442 23 | ||
| - | * 098541 26 | ||
| - | * 098438 23 | ||
| - | * 097946 28 | ||
| - | * 098431 25 | ||
| - | * 098437 27 | ||
| - | * 093700 25 | ||
| - | |||
| - | **Exam rules**: | ||
| - | * **Written test**. On the exam date a written test takes place, it has a mixed structure: solution of exercises, and open/close answer questionnaire. During the course in itinere tests take place; in case they are evaluated positively, they replace the written test of the exam date. | ||
| - | * Realisation of a **project** with a software tool presented during the course, or writing of a report. There is an **oral discussion**. | ||
| - | |||
| - | ** Exam Results ** | ||
| - | * N/A | ||
| - | </WRAP> | ||
