Course Catalog 2013-2014
Postgraduate

Basic Pori International Postgraduate Open University

|Degrees|     |Study blocks|     |Courses|    

Course Catalog 2013-2014

TTE-54006 Formal Methods in Factory Automation, 5 cr

Additional information

Suitable for postgraduate studies
Will not be lectured year 2013-2014

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     

Instructions for students on how to achieve the learning outcomes

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   No    English  
Book   Model checking   Clarke, Grumberg and Peled       MIT press 2001   No    English  
Book   Modeling, Simulation, and Control of Flexible Manufacturing Systems   Zhou, M; Venkatesh, K.   981-02-3029-X       No    English  
Book   Petri Nets for Systems Engineering   Girault and Valk       Springer 2003   No    English  
Book   Petri Nets in Flexible and Agile Automation   Zhou M.       Kluwer 1995   No    English  
Book   Principles of Automated Theorem Proving   Duffy D.       Wiley 1991   No    English  
Book   Principles of Model Checking   Baier and Katoen   978-0-262-02649-9     MIT press 2008   No    English  
Lecture slides             Yes    English  
Other literature           selected papers   No    English  

Prerequisite relations (Requires logging in to POP)



Correspondence of content

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

Last modified22.01.2013