Course Catalog 2006-2007

TTE-5406 FORMAL METHODS IN FACTORY AUTOMATION, 5 cr
Formal Methods in Factory Automation

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 - - -
(Timetable for academic year 2006-2007)

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

  • Course assingment gives 30% of the final grade Laboratory works: 30% Exam: 40%

  • Used assessment scale is numeric (1-5)

  • 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.

  • The course is suitable for postgraduate studies.

  • Scaling
    Methods of instructionHours
    Lectures 60
    Exercises 24
    Assignments 28
    Laboratory assignments 11
    Other contact teaching 5

    Other scaledHours
    New tools and study methods 4
    Preparation for exam 4
    Exam/midterm exam 3
    Total sum 139

    Course homepage

    Last modified 28.08.2006
    Modified byJorma Vihinen