Domain Specific Formal Languages

Teacher:

• Francesco Tiezzi

Lessons schedule:

• Monday 15 - 17 (D. M. Ritchie room)
• Tuesday 9 - 11 (D. M. Ritchie room)

Students Office hours:

• on appointment (via email), room CS 08, second floor of Polo Tecnologico Palazzo Battibocca, via del Bastione 1, Camerino

D1 – KNOWLEDGE AND UNDERSTANDING
At the end of the course, the student should be able to:

1. 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.
2. 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:

1. Model a system using the appropriate formal language among those presented in the course.
2. Derive the labelled transition system associated to a formal specification.
3. 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:

1. 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:

1. 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:

1. Search the scientific literature for specific advances in formalisms and software tools aimed at modelling and verifying systems.
2. Autonomously learn to define formalisms for different application domains.

• 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.

Course Slides

• General information and introduction
• CCS
• J. Parrow. An introduction to the pi-calculus
• Klaim
• Calculi for network-aware programming
• An overview of SOC
• COWS
• Analysis of SOC systems with COWS

Tools

• Klava

Lectures

• 13 December
• 16 December
• 20 December (password: pBGM3hmq)
• 23 December (password: gYevPmJ2)
• 13 January (password: tPbbSnN2)
• 27 January (password: kJF4Yxf9)
• 2 February (password: gYEQ6a6c)

Reference books

• The teaching material of the course consists of lecture notes, papers and slides provided by the teacher in this website.

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: 19/06/2017 ore 10:00 - Polo Lodovici
• Appello IV: 10/07/2017 ore 10:00 - Polo Lodovici
• Appello V: 26/07/2017 ore 10:00 - Polo Lodovici
• Appello VI: 8/09/2017 ore 10:00 - Polo Lodovici
• Appello VII: 22/09/2017 ore 10:00 - Polo Lodovici
• Appello VIII: 20/10/2017 ore 10: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