Real-time systems (2006/2007)

Course Not running, not visible

Course code
4S01075
Name of lecturer
Tiziano Villa
Number of ECTS credits allocated
5
Other available courses
Academic sector
ING-INF/05 - INFORMATION PROCESSING SYSTEMS
Language of instruction
Italian
Location
VERONA
Period
1st quadrimester (for 2nd and 3rd years of degrees in IT, for the 2nd year of degrees in applied mathematics and for the 4th and 5th years of specialised degrees) dal Oct 2, 2006 al Dec 1, 2006.

Lesson timetable

Learning outcomes

The objective of the class is to introduce design methodologies and formal methods for analysis and synthesis of real-time electronic systems, with special reference to the design and verification of embedded systems.

Syllabus

Embedded system design
1. Introduction to embedded systems
2. Instruction set architectures for general-purpose and application-specific processors
3. CPUs and co-processors
4. Memories, peripherals, communication and interfacing
5. Concurrent processes, operating systems and scheduling algorithms
6. Control systems
7. Design methodologies

Real-time scheduling of aperiodic and periodic tasks

Formal methods for real-time systems
1. Transducive and reactive systems
2. Deterministic, pseudo-nondeterministic and non-deterministic state machines
3. Composition of state machines
4. Simulation, bisimulation, and determinization of state machines
5. Equivalence, containment and minimization of state machines
6. Timed and hybrid automata
7. Reachability analysis of hybrid automata
8. Controller synthesis for safety and progress

Reference books
Author Title Publisher Year ISBN Note
Wayne Wolf Computers as Components: Principles of Embedded System Design Morgan Kaufman Publishers 2005
Frank Vahid and Tony Givargis Embedded System Design: A Unified Hardware/Software Introduction John Wiley & Sons 2002

Assessment methods and criteria

Written exam and class project.

The class project of this year is about the formal verification of safety properties of systems modeled by hybrid automata, by using software packages that perform reachability analysis of hybrid automata

Teaching aids

Documents

Share