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.