TTE-5406 FORMAL METHODS IN FACTORY AUTOMATION, 5 cr
|
Courses persons responsible
Jose Martinez Lastra
Lecturers
Andrei Lobov
Jose Martinez Lastra
Corina Popescu
Lecturetimes and places
Per II: Monday 14 - 16, K3114
Per II: Friday 10 - 12, K3114
Per III: Monday 14 - 16, K3202B
Per III: Friday 10 - 12, K3202B
Implementations
Period 1 | Period 2 | Period 3 | Period 4 | Period 5 | Summer | |
Lecture | - | 2 h/week | 2 h/week | - | - | - |
Exercise | - | 1 h/week | 1 h/week | - | - | - |
Objectives
Students will learn formal languages and methods that can be applied in factory automation in areas such as: control modeling, verification, validation, and manufacturing planning.
Content
Content | Core content | Complementary knowledge | Specialist knowledge |
1. | General introduction to formal languages and methods and their utilization in dynamic discrete systems. |   | |
2. | Formal languages for modeling factory automation systems | Petri Nets, Finite Automaton | |
3. | Application of formal methods in factory automation systems |   | |
4. | Formal verification and validation of factory automation systems:
Requirements specification languages, Model-checking, Theorem proving |
  |
Requirements for completing the course
Written Exam AND Laboratory exercises AND course assignment(s)
Evaluation criteria for the course
Study material
Type | Name | Auhor | ISBN | URL | Edition, availability... | Exam material | Language |
Book | Modeling, Simulation, and Control of Flexible Manufacturing Systems | Zhou, M; Venkatesh, K. | 981-02-3029-X | No | English | ||
Book | Software Verification and Validation for Practitioners and Managers | Rakitin, S. | 1-58053-296-9 | No | English | ||
Book | Discrete, Continuous, and Hybrid Petri Nets | David, R.; Alla, H. | 3-540-22480-7 | No | English | ||
Other literature | An Approach to the Formal Verification of Automated Manufacturing Systems with Programmable Control | Lobov, A. | TUT Library | No | English | ||
Book | Development and Implementation of Hierarchical Control Structures of Flexible Production Systems Using High-Level Petri Nets | Colombo, A.W. | 3-87525-109-1 | No | English |
Prerequisites
Code | Course | Credits | M/R |
MAT-41176 | MAT-41176 Theory of Automata | 5 | Recommendable |
MAT-41180 | MAT-41180 Formal Languages | 6 | Recommendable |
Prequisite relations (Sign up to TUT Intranet required)
Remarks
The course gives an introduction to the utilization of formal methods in the domain of factory automation. Different perspectives of factory artifacts modeling are given to students. Students learn how and where to apply formal methods.
Scaling
Methods of instruction | Hours |
Lectures | 60 |
Exercises | 24 |
Assignments | 28 |
Laboratory assignments | 11 |
Other contact teaching | 5 |
Other scaled | Hours |
New tools and study methods | 4 |
Preparation for exam | 4 |
Exam/midterm exam | 3 |
Total sum | 139 |
Last modified | 28.08.2006 |
Modified by | Jorma Vihinen |