Domain Specific Formal Languages

Teacher:

• 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

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
• Preliminaries
• 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
• FACPL

Tools

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

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