|
|
|||||||||||||||||
Course Catalog 2010-2011
TTE-5406 Formal Methods in Factory Automation, 5 cr |
Person responsible
Corina Popescu, Lastra Jose Martinez
Requirements
Written Exam AND Laboratory exercises AND course assignment(s)
Principles and baselines related to teaching and learning
-
Learning outcomes
Students will learn formal languages and methods that can be applied in factory automation in areas such as: control modelling, verification, validation, and manufacturing planning. The course addresses the modelling, verification and validation of factory automation systems. At the end of the course the student should be able to model a factory automation system using any of the modelling languages presented during the course (i.e. Petri Nets and timed automata). Additionally, the student should have good knowledge of how choices made at modelling stage can influence the verification steps.
Content
| Content | Core content | Complementary knowledge | Specialist knowledge |
| 1. | System modelling with Petri Nets and Timed Automata | Structural analysis of Petri nets. P and T invariants | |
| 2. | Requirements specification. Temporal logic | ||
| 3. | Model checking | Techniques to cope with the state space explosion problem. | |
| 4. | Performance analysis based on Petri net models | ||
| 5. | Scheduling search on Petri Nets | ||
| 6. | Deadlock handling: graph-based and Petri nets-based methods |
Evaluation criteria for the course
The grade will be calculated as: 40% final examination, 30% course exercise works and 30% course assignments.
Assessment scale:
Numerical evaluation scale (1-5) will be used on the course
Study material
| Type | Name | Author | ISBN | URL | Edition, availability, ... | Examination material | Language |
| - | A Calculus of Communicating Systems | Milner R. | 978-3-540-10235-9 | Lecture Notes in Computer Science, vol. 92, 1980 | English | ||
| Book | Model checking | Clarke, Grumberg and Peled | MIT press 2001 | English | |||
| Book | Modeling, Simulation, and Control of Flexible Manufacturing Systems | Zhou, M; Venkatesh, K. | 981-02-3029-X | English | |||
| Book | Petri Nets for Systems Engineering | Girault and Valk | Springer 2003 | English | |||
| Book | Petri Nets in Flexible and Agile Automation | Zhou M. | Kluwer 1995 | English | |||
| Book | Principles of Automated Theorem Proving | Duffy D. | Wiley 1991 | English | |||
| Book | Principles of Model Checking | Baier and Katoen | 978-0-262-02649-9 | MIT press 2008 | English | ||
| Lecture slides | English | ||||||
| Other literature | selected papers | English |
Prerequisite relations (Requires logging in to POP)
Correspondence of content
There is no equivalence with any other courses
Additional information
Will not be lectured year 2011-2012.
Suitable for postgraduate studies