Universitatea Babeş-Bolyai Cluj-Napoca
Facultatea de Matematică şi Informatică
Ciclul de studii: Licenţă
Domeniul: Informatică
Programul de studii: Informatică - în limba engleză
Limba de predare: Engleză

SYLLABUS

I. General data
Code	Subject	
MID0042	Computational Models for Embeded Systems	

Semester	Hours: C+S+L+P	Category	Status	
5	2+0+1+0	speciality	optional	

II. Full status faculty members
Name and	Scientific	Didactic	Chair	Type of activity	
surname	title	title		C	S	L	
VESCAN Andreea	Ph.D.	Lect.	Programming  Languages and Methods	*			

Associated faculty members
Name and	Scientific	Institution	Type of	Type of activity	
surname	title		position	C	S	L	

III. Course objectives
Modeling is an essential technique and serves various purposes, so it is important to understand its fundamental concepts. These concepts relate basically to the way a modeling paradigm allows one to deal with the great properties of system: time, computation, data and communication.

In general, when modeling a system, we want to be able to formulate particular questions on it:
-	Will a system ever enter a particular state?
-	Will it always be able to avoid a particular dangerous state?
-	Will it always eventually reach some desired state?
The classical theory of computation focuses on the function that a program computes. To understand embedded computation, we need to focus on the reactive nature of the interaction of a component with its environement and requirements concerning safety, timeliness, stability, and performance.

The main objectives of this cours are to provide an understanding of the fundamentals concepts of software modeling, more precise for embedded computation; to develop skills in modeling and to describe and verify safety and liveness properties of the system being modeled.

IV. Course contents
1.	Model: Why?what? how? Types of systems.
2.	Requirements and Safety Requirements
3.	Finite State Machines
4.	Statecharts 
5.	Petri Nets
6.	Communication paradigms 
    7. Asynchronous message passing
    8. Synchronous message passing
    9. Model checking
    10. LTL (Linear temporal logic)
    11. Computation tree logic (CTL)	

V. Bibliography
[1] C. Baier, J.-P. Katoen, Principles of Model Checking, ISBN 978-0-262-02649-9, 2008
[2] M. Ben-Ari, Principles of the Spin Model Checker, ISBN 978-1-84628-769-5
[3] Taylor Booth (1967) Sequential Machines and Automata Theory, John Wiley and Sons, New York. Library of Congress Catalog Card Number: 67-25924.
[4] D. Harel, "Statecharts: A Visual Formalism for Complex Systems", Sci. Comput. Programming 8 (1987), 231-274
[5] Petri, CA (1966) Communication with automata. DTIC Research Report AD0630125
[6] Hoare, CAR (2004) (1985), Communicating Sequential Processes, Prentice Hall International
Optional references 
Internet resources and conferences	

VI. Thematic of didactic activities per weeks
Schedule of courses 
       1.Introduction  (lecture 1) 
1.1 Model – why?what? how?
1.2 Types of systems:static/dynamic,time-varying/time-invariant,continous/discrete, linear/non-linear, deterministic/non-deterministic, time-driven/event-driven.
      2. Requirements and Safety Requirements (lecture 2)
2.1. Requirements types
2.2. Formal requirements languages
       3. Finite State Machines (lecture 3)
3.1. Finite State Machines: Moore, Mealy
      4. Statecharts (lecture 4)
4.1. Statecharts: state and history mechanism, timers
      5. Petri Nets (lecture 5)
5.1. Control flow, concurrency, deadlocks
5.2. Timed Petri Nets
5.3 Colored Petri Nets
       6. Communication paradigms  (lecture 6)
6.1. Message passing
6.2. Non-blocking communication
6.3. Blocking communication, rendez-vous-based communication
6.4. Shared memory
        7. Asynchronous message passing (lecture 7)
7.1. Kahn process networks
7.2. Synchronous data flow (SDF)
       8. Synchronous message passing (lecture 8)
8.1. CSP (communicating sequential processes)
8.2. ADA
      9. Model checking  (lecture 9)
9.1. Describing safety and liveness properties
     10. LTL (Linear temporal logic) (lecture 10)
10.1. SPIN 
      11. Computation tree logic (CTL) (lecture 11)
      12. Graded paper (lecture 12)

Schedule of laboratory activities and project activities 
Theme 1 (lab 1-2, weeks 1-4) 
       Specifying safety requirements for a given embedded system 
Theme 2 (lab 3-4, weeks 5-8) 
       Using Finite State Machines, Statecharts, PetriNets to model an embedded system
Theme 3 (lab 5-6, weeks 9-12) 
      Asynchronous message passing (Synchronous data flow SDF), 
      Synchronous message passing (CSP), Model checking	

VII. Didactic methods used
Presentation – for lectures and seminars;
Conversation – for seminars and lectures;
Didactic demonstration – for lectures;
Problematizations – for lectures and laboratory work;
Discovery – for laboratory work;
Other methods – individual study, exercices – for laboratory work.	

VIII. Assessment
The final grade is determined as follows: 
-	GA=Grade Activity = lab activity = 20% 
-	GP=GradeProjects = documentations, programs and projects developed = 20% 
-	GF=GradeFinal = graded paper at the final exam, during lecture 12=60%. 
Passing the final exam is conditioned by the grade GF being at least 5.
  The official webpage of the course is http://www.cs.ubbcluj.ro/~avescan, section Teaching	

IX. Additional references

	Dean,							Chair head,
Prof. Leon Tambulea, PhD				Prof. Bazil Parv, PhD	

	Date,							Course responsible,
	1.10.2010						Lect. VESCAN Andreea, Ph.D.