Course Catalog 2012-2013
International

Basic Pori International Postgraduate Open University

|Degrees|     |Study blocks|     |Courses|    

Course Catalog 2012-2013

TTE-5406 Formal Methods in Factory Automation, 5 cr

Additional information

Suitable for postgraduate studies

Person responsible

Corina Popescu, Lastra Jose Martinez

Lessons

Study type P1 P2 P3 P4 Summer Implementations Lecture times and places
Lectures
Assignment
 2 h/week
 2 h/week
+2 h/week
+2 h/week


 


 


 
TTE-5406 2012-01 Thursday 8 - 11, TB224

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

Course Corresponds course  Description 
TTE-5406 Formal Methods in Factory Automation, 5 cr TTE-54006 Formal Methods in Factory Automation, 5 cr  

More precise information per implementation

Implementation Description Methods of instruction Implementation
TTE-5406 2012-01        

Last modified14.03.2012