Course Catalog 2008-2009 Basic Basic Pori International Postgraduate Open University |Degrees|     |Study blocks|     |Courses|

Course´s person responsible

Corina Popescu, Jose Martinez Lastra

Implementations

	Lecture times and places	Target group recommended to
Implementation 1	Per 2 : Wednesday 9 - 11, K3114 Per 3 : Friday 9 - 11, K3114

Requirements

Written Exam AND Laboratory exercises AND course assignment(s)

Principles and baselines related to teaching and learning

-

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

Evaluation criteria for the course

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

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

Prerequisites

More precise information per implementation

	Description	Methods of instruction	Implementation
Implementation 1	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, timed automata, process algebras). Additionally, the student should have good knowledge of how choices made at modelling stage can influence the verification steps.

Last modified	13.08.2008
Modifier	Hanna Hämäläinen