PROCESS ALGEBRAS
In order to fruitfully attend the course of Process Algebras the student is required to have familiarity with the basic notions in the realm of formal languages. This requisite is surely respected by students with a 3-years degree in Mathematics or Computer Science
The scope of the exam is to certify that students have all knowledge and ability explained above, by evaluating the knowledge skill and, mainly, the ability to understand and evaluate the novelty in the area proposed in scientific papers.
The exam consists in an oral discussion in a classroom. This is, normally, a 30 mins discussion requiring, normally, to exposing the content of a scientific paper. The evaluation focuses on the ability to understand the results and the ability to understand how these results compare with respect the literature and can be applied in practice.
The knowledge of the technical terminology is implicitly checked since the questions and specifications of problems use such a terminology.
The aim of the course is to allow students to know the theory of process algebras. Students will learn how this formalism can be employed in the formal modelling of concurrent processes, how this instrument provides algebraic laws allowing for process descriptions to be manipulated and analysed and how the formalism allows for formal reasoning about equivalences over processes.
At the end of the course, the student will be able to:
1. Recognise in which context process algebras can be applied.
2. Provide formal specifications of simple systems.
3. Reason in terms of equivalences over processes.
4. Learn how tools based on process algebra work and can be used
5. Enlarge their knowledge to extensions of process algebra dealing with time, probability, and other features.
Further, the student will be able to specify simple systems with process algebras, to recognise when syntactically different specifications may be considered undistinguishable under a proper level of abstraction.
The student will be also required to develop autonomy of judgement in recognising the main challenges of employment of process algebras.
Finally, the student will get a proper knowledge of (possibly standard) technical terminology used in the context of process algebras.
The course is organised as follows:
Background:
• Introduction and Regular Expressions, seen as a preliminary case study (4h, ability 1)
• The operational semantics of a simple “while” language (6h, ability 1)
• The denotational semantics of a simple “while” language (6h, ability 1)
The kernel e of process algebras:
• Models for concurrency (6h, ability 2)
• Main operators of process calculi (4h, ability 2)
• Equivalences between processes (6h, ability 3)
• Case study: ABP protocol (4h, ability 1,2,3,4)
• CCS (4h, ability 1,2,3,4)
Formal reasoning:
• Axiomatisations (4h, ability 3)
• Modal logic (4h, ability 2)
Extensions to quantitative aspects:
• Probabilistic process algebras (6h, abiilty 5)
• Timing aspects (6h, ability 5)
• Hybrid models (4h, ability 5)
The course is organised in frontal lessons (64 h).
Frontal lessons are dedicated to illustrating the essence and principles of process algebras mentioned in the “Contents” section. In detail, frontal lessons are dedicated to describing the typical usage of process algebras, by illustrating what can be properly specified by using this formalism. Then, properties of these specifications will be discussed as well as the connections between the syntax of specifications and their meaning. The notion of equivalence and the way in which it can support verification will be also illustrated. Students will be required to interact with the teacher, to comment some definitions/results and to challenge the teacher with questions.
Professors
Borrowers
-
Degree course in: COMPUTER SCIENCE
-
Degree course in: MATHEMATICS
-
Degree course in: COMPUTER SCIENCE