Laajuus: 5
Aikataulu: 25.02.2019 - 24.05.2019
Opetusperiodi (voimassa 01.08.2018-31.07.2020):
IV-V (autumn) 2018 - 2019
IV-V (autumn) 2019 - 2020
Osaamistavoitteet (voimassa 01.08.2018-31.07.2020):
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.
Sisältö (voimassa 01.08.2018-31.07.2020):
The students will acquire theoretical background and practical experience of formal methods application for validation and synthesis of hardware, software and reactive embedded systems
Tarkennukset kurssin sisältöön (koskee tätä kurssikertaa):
Covered topics:
- 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.
- Formal synthesis: supervisory controller synthesis, LTL synthesis (including work with the tool G4LTL-ST).
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;
- means of automatic generation of formal models based on specification.
Toteutus, työmuodot ja arvosteluperusteet (voimassa 01.08.2018-31.07.2020):
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.
Tarkennetut arviointiperusteet ja -menetelmät ja tutustuminen arviointiin (koskee tätä kurssikertaa):
The major part of the course grade is the result of completing individual assignments. 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.
Työmäärä toteutustavoittain (voimassa 01.08.2018-31.07.2020):
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
Oppimateriaali (voimassa 01.08.2018-31.07.2020):
Slides and handouts
Kurssin kotisivu (voimassa 01.08.2018-31.07.2020):
https://mycourses.aalto.fi/course/search.php?search=ELEC-E8110
Esitiedot (voimassa 01.08.2018-31.07.2020):
Required: Automation 1 and 2 or similar knowledge. Software development practice. Useful: Discrete mathematics
Arvosteluasteikko (voimassa 01.08.2018-31.07.2020):
1-5
Lisätietoja (voimassa 01.08.2018-31.07.2020):
language class 3: English