====== Domain Specific Formal Languages ======
----
===== News =====
<WRAP center round important 95%>
  * January 17th, 2018: second in-itinere test
  * November 6th, 2017: first in-itinere test
  * 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**
  * [[http://facpl.sourceforge.net|FACPL]]
  * {{ :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.
  * 15 November 2017: Introduction to the service-oriented computing domain; intro to COWS.
  * 27 November 2017: COWS.
  * 29 November 2017: From simple sensors to intelligent sensors in the Internet of Things ...and how Machine Learning comes into the picture.
  * 17 January 2018: in itinere test. 




**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>