Differences

This shows you the differences between two versions of the page.

--- didattica:magistrale:fmsis:main [2018/03/06 11:01]
tiezzi [Exams]
+++ — (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**
-  * {{ :didattica:magistrale:fmsis:ay_1718:fmsis_intro_1718.pdf |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. 2017/2018**
-  * ...
-**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>