Domain Specific Formal Languages

News

  • 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

General Info

Teacher:

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

Course Objectives

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.

Course Contents

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

Study material

Course Slides

Tools

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.

Exams

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