Please note! Course description is confirmed for two academic years, which means that in general, e.g. Learning outcomes, assessment methods and key content stays unchanged. However, via course syllabus, it is possible to specify or change the course execution in each realization of the course, such as how the contact sessions are organized, assessment methods weighted or materials used.
LEARNING OUTCOMES
After completing the course, a student will understand: benefits of formal methods application for automation systems analysis and synthesis; correctness of system's behaviour, compliance with performance and safety requirements; formal modelling of cyber-physical systems, including code-based model generation; formal synthesis of discrete event systems.
Credits: 5
Schedule: 03.03.2021 - 28.05.2021
Teacher in charge (valid 01.08.2020-31.07.2022): Pekka Aarnio, Valeriy Vyatkin
Teacher in charge (applies in this implementation): Pekka Aarnio, Valeriy Vyatkin
Contact information for the course (valid 10.02.2021-21.12.2112):
Polina Ovsiannikova, polina.ovsiannikova@aalto.fi
Valeriy Vyatkin, valeriy.vyatkin@aalto.fi
CEFR level (applies in this implementation):
Language of instruction and studies (valid 01.08.2020-31.07.2022):
Teaching language: English
Languages of study attainment: English
CONTENT, ASSESSMENT AND WORKLOAD
Content
Valid 01.08.2020-31.07.2022:
The students will acquire theoretical background and practical experience of formal methods application for validation and synthesis of hardware, software and reactive embedded systems
Applies in this implementation:
The main focus of the course is a particular formal verification method called model checking. The analysis itself is performed by software tools but their use requires general undertanding of model checking, which is taught during the course. In addition, a significant part of the course is devoted to modeling industrial automation systems (controllers and plants) and requirements to these systems so that model checking could be applied.
Covered topics in detail:
- Formal methods in automation and the scope of their use, their application for safety-critical systems.
- Modelling of cyber-physical systems, including modelling of plants, controllers, distribution and modularity.
- Specifying safety and correctness of systems using finite-state machines.
- Formal specification languages: LTL, CTL.
- Formulating natural language requirements in LTL and CTL.
- Formal verification of safety and correctness by means of model checking, basic ideas behind model checking algorithms.
- Software tools to model and model-check automation systems: UPPAAL, NuSMV.
- User-friendly model checking.
- Advanced modelling of time: timed automata, timed temporal logics.
The course comprises lectures, exercise sessions and individual work.
The main aim of the course is to develop skills of ensuring safety and correctness of industrial automation systems using formal methods such as model checking and formal synthesis. After completing the course, a student will understand:
- the benefits of applying formal methods of automation systems analysis and synthesis;
- formal modelling of cyber-physical systems as modular systems composed of finite-state machines;
- means of formally specifying safety and correctness of automation systems;
- means of checking such formal specification automatically with software tools.
Assessment Methods and Criteria
Valid 01.08.2020-31.07.2022:
The course is problem solving driven. The students will receive necessary knowledge for the problem solution via lectures and reading. The students will acquire practical skills of software tools during lab exercises. Exam.
Applies in this implementation:
The major part of the course grade is the result of completing several assignments that are supposed so be completed individually or in pairs. These assignments are often based on practical skills (e.g., working with software tools, modelling) obtained on exercise sessions and theoretical knowledge given on lectures. The exam assesses both theoretical knowledge and practical skills.
All graded activities (e.g., homework assignment) contribute to the overall grade of the course. Typically, the teachers provide written or spoken feedback for all graded activities except the exam. The fraction of the overall grade is specified for each graded activity when it is announced. Tentative partition of the overall grade:
- 50%: course project (composed of three assignments);
- 20%: other assignments, including completion of tutorials;
- 30%: exam.
Workload
Valid 01.08.2020-31.07.2022:
Lectures 10. Reading 5. Individual problem solving 40. Laboratory sessions in small groups 5. Team work 20. Tutorials and other supervised activity in PC classroom, including audits 12. Report preparation and final audit 20. Reflection 20.
Contact hours: 30
Independent study: 100
Applies in this implementation:
Practical (individual or in pairs) work constitutes a significant fraction of time. There is some time to do it during exercise sessions, but out-of-class work will likely require more time.
DETAILS
Study Material
Valid 01.08.2020-31.07.2022:
Slides and handouts
Applies in this implementation:
Lecture slides and other supporting materials (e.g., scientific papers on the topic, software tools to be used) are usually made open at the day of the corresponding lecture or exercise session. Most of lecture slides are based on information that can be found in public sources.
Prerequisites
Valid 01.08.2020-31.07.2022:
Required: Automation 1 and 2 or similar knowledge. Software development practice. Useful: Discrete mathematics
FURTHER INFORMATION
Details on the schedule
Applies in this implementation:
Typically, there will be a homework assignment every week or two weeks.
- Teacher: Buzhinskii Igor
- Teacher: Ovsiannikova Polina
- Teacher: Vyatkin Valeriy