Course Catalog 2011-2012
Basic

Basic Pori International Postgraduate Open University

|Degrees|     |Study blocks|     |Courses|    

Course Catalog 2011-2012

TTE-5406 Formal Methods in Factory Automation, 5 cr

Additional information

Will not be lectured year 2011-2012. Next course implementation comes in 2012-2013 academic year.
Suitable for postgraduate studies
Will not be lectured year 2011-2012

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

Last modified18.03.2011