D1 – KNOWLEDGE AND UNDERSTANDING
At the end of the course, the student should be able to:
Have the knowledge of the issues concerning concurrent/distributed programming and the modelling of hardware/software systems as software-intensive systems.
Have the knowledge of the semantics of the operators of the process algebras CCS, CSP and ACP.
Have the knowledge of the syntax and the semantics of the modal logic Hennessy-Milner Logic (HML), with and without recursion, and of the ACTL logic.
Have the knowledge of the main observational behavioural equivalences, weak and strong.
Have the knowledge of the tools for the automatic verification of software-intensive systems modelled by means of process algebras.
D2 – APPLYING KNOWLEDGE AND UNDERSTANDING
At the end of the course, the student should be able to:
Modelling a software-intensive system using the formal languages presented in the course, using a compositional approach.
Derive the labelled transition system associated to a process.
Decide if one or more state of a labelled transition system are stong or weak bisimilar, providing a suitable bisimulation relation whereas possible.
Decide if one or more states of a labelled transition system satisfy formulas of HML and ACTL logics.
Define temporal properties of a software-intensive system using the HML and ACTL logics.
Use a specific software tool for the analysis of software-intensive systems modelled using the CCS language or other formalism.
D3 – MAKING JUDGEMENTS
At the end of the course, the student should be able to:
Identify the best model suitable for describing a system using a given formalism.
D4 - COMMUNICATION SKILLS
At the end of the course, the student should be able to:
Write a clear report on the modelling and analysis of a system under study using a formal style.
Write a brief survey and state of the art about a given research topic by searching the scientific literature.
D5 – LEARNING SKILLS
At the end of the course, the student should be able to:
Search the scientific literature for specific advances in formalisms and tools aimed at modelling and verifying software-intensive systems.
Autonomously understand and learn to use new features added to tools for modelling and verifying software-intensive systems.