Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
didattica:magistrale:dsfl:main [2017/11/13 13:51] tiezzi [Study material] |
— (current) | ||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== Domain Specific Formal Languages ====== | ||
| - | ---- | ||
| - | ===== News ===== | ||
| - | <WRAP center round important 95%> | ||
| - | * <wrap em>November 6th, 2017: first in-itinere test</wrap> | ||
| - | * October 16th, 2017: the lecture is postponed | ||
| - | * October 2nd, 2017: first lecture | ||
| - | </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**: | ||
| - | * Monday 14 - 17 (room AB2) | ||
| - | * Wednesday 11 - 14 (room AB2) | ||
| - | |||
| - | **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 syntax and semantics of the formal languages at the basis of the DSL introduced in the course, i.e. CCS and pi-calculus. | ||
| - | - Have the knowledge of DSLs and related tools for distributed systems, service-oriented systems, access control policies, cloud computing systems, autonomic systems, and business process modelling. | ||
| - | |||
| - | D2 – APPLYING KNOWLEDGE AND UNDERSTANDING\\ | ||
| - | At the end of the course, the student should be able to:\\ | ||
| - | - Model a system using the appropriate formal language among those presented in the course. | ||
| - | - Derive the labelled transition system associated to a formal specification. | ||
| - | - Use software tools specific for the analysis and development of the considered classes of systems. | ||
| - | |||
| - | D3 – MAKING JUDGEMENTS\\ | ||
| - | At the end of the course, the student should be able to:\\ | ||
| - | - Identify the best language suitable for describing a given system. | ||
| - | |||
| - | D4 - COMMUNICATION SKILLS\\ | ||
| - | At the end of the course, the student should be able to:\\ | ||
| - | - Present the modelling and analysis of a system under study using a formal style. | ||
| - | |||
| - | 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 software tools aimed at modelling and verifying systems. | ||
| - | - Autonomously learn to define formalisms for different application domains. | ||
| - | </WRAP> | ||
| - | |||
| - | ---- | ||
| - | ===== Course Contents ===== | ||
| - | |||
| - | <WRAP round 95% center box> | ||
| - | * Brief introduction to preliminary mathematical concepts at the basis of the topic faced in the course. | ||
| - | * Domain Specific Languages (DSL) | ||
| - | * From CCS to pi-calculus: syntax and semantics | ||
| - | * DSL for distributed systems: Dpi, Djoin, Ambient, Klaim/Klava | ||
| - | * DSL for service-oriented systems: COWS/SocL/CMC, CaSPiS, SOCK/Jolie, Blite/BliteC | ||
| - | * DSL for access control policies: FACPL | ||
| - | * DSL for cloud computing systems: SLAC/dSLAC, Mobica | ||
| - | * DSL for autonomic systems: SCEL/jRESP | ||
| - | * DSL for business process modelling: BPMN formalisation | ||
| - | |||
| - | **Prerequisites**\\ | ||
| - | Content from the FORMAL MODELLING OF SOFTWARE INTENSIVE SYSTEMS course, such as finite state automata; context-free grammars; inference systems; syntax and semantics of CCS. These topics will be anyway briefly illustrated at the beginning of the course. | ||
| - | </WRAP> | ||
| - | ---- | ||
| - | ===== Study material ===== | ||
| - | <WRAP box round center 95%> | ||
| - | **Course Slides** | ||
| - | * {{ :didattica:magistrale:dsfl:ay_1718:dsfl_intro_17-18.pdf |General information and introduction}} | ||
| - | * {{ :didattica:magistrale:dsfl:ay_1718:preliminaries.pdf |Preliminaries}} | ||
| - | * {{ :didattica:magistrale:dsfl:ay_1718:slides_ccs.pdf |CCS}} | ||
| - | * {{ :didattica:magistrale:dsfl:ay_1718:parrow--an_introduction_to_the_pi-calculus.pdf |J. Parrow. An introduction to the pi- | ||
| - | calculus}} | ||
| - | * {{ :didattica:magistrale:dsfl:ay_1718:pi-calculus_notes.pdf |Pi-calculus personal notes}} | ||
| - | * {{ :didattica:magistrale:dsfl:facpl_long.pdf |FACPL}} | ||
| - | * {{ :didattica:magistrale:dsfl:ay_1718:klaim_1718.pdf |Klaim}} | ||
| - | |||
| - | * {{ :didattica:magistrale:dsfl:ay_1718:foundational_calculi_for_network_aware_programming_.pdf |Calculi for network-aware programming}} | ||
| - | * {{ :didattica:magistrale:dsfl:ay_1718:soc.pdf |An overview of SOC}} | ||
| - | * {{ :didattica:magistrale:dsfl:ay_1718:cows.pdf |COWS}} | ||
| - | * {{ :didattica:magistrale:dsfl:ay_1718:analysis_with_cows.pdf |Analysis of SOC systems with COWS}} | ||
| - | |||
| - | **Tools** | ||
| - | * {{ :didattica:magistrale:dsfl:ay_1718:klava-2b.jar.zip |Klava}} | ||
| - | |||
| - | **Lectures** | ||
| - | * 2 October 2017: General information and introduction. | ||
| - | * 4 October 2017: Sw intensive systems; process algebraic approach; formal methods for reactive systems. Preliminary notions. | ||
| - | * 9 October 2017: CCS syntax and semantics; CCS examples. | ||
| - | * 11 October 2017: external and internal choice; Value passing CCS. Pi-calculus syntax and structural congruence. | ||
| - | * 18 October 2017: Pi-calculus reduction semantics; examples. | ||
| - | * 23 October 2017: Pi-calculus labelled semantics; examples. | ||
| - | * 25 October 2017: Examples on Pi-calculus labelled semantics. Intro to access control systems. | ||
| - | * 30 October 2017: FACPL syntax, semantics and examples. | ||
| - | * 06 November 2017: in itinere test. | ||
| - | * 08 November 2017: analysis of FACPL policies; FACPL toolchain. | ||
| - | * 13 November 2017: Klaim syntax and semantics. | ||
| - | |||
| - | |||
| - | |||
| - | |||
| - | **Reference books** | ||
| - | * The teaching material of the course consists of lecture notes, papers and slides provided by the teacher in this website. | ||
| - | </WRAP> | ||
| - | ---- | ||
| - | ===== Exams ===== | ||
| - | <WRAP box round center 95%> | ||
| - | **Exam Dates A.Y. 2017/2018** | ||
| - | * Appello I: 07/02/2018 ore 14:00 - Polo Lodovici | ||
| - | * Appello II: 28/02/2018 ore 14:00 - Polo Lodovici | ||
| - | * Appello III: 13/06/20178 ore 14:00 - Polo Lodovici | ||
| - | * Appello IV: 3/07/2018 ore 14:00 - Polo Lodovici | ||
| - | * Appello V: 18/07/2018 ore 14:00 - Polo Lodovici | ||
| - | * Appello VI: 12/09/2018 ore 14:00 - Polo Lodovici | ||
| - | * Appello VII: 26/09/2018 ore 14:00 - Polo Lodovici | ||
| - | * Appello VIII: 27/02/2019 ore 14:00 - Polo Lodovici | ||
| - | |||
| - | **Exam rules**:\\ | ||
| - | Learning outcomes are assessed using two different tests: | ||
| - | * **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> | ||
