To show the organization of the course that includes this module, follow this link Course organization
|Tuesday||8:30 AM - 10:30 AM||lesson||Lecture Hall I|
|Thursday||10:30 AM - 12:30 PM||lesson||Lecture Hall I|
An introduction to formal methods for the specification, design and verification of hardware and software systems.
Such systems include heterogeneous and concurrent components defined at different levels of abstraction, to be implemented in hardware and software; they must satisfy functional and real time constraints, and may interact with physical systems (cyberphysical systems).
Prerequisites. The class is self-contained, however a student should have a good grasp of the basic notions of discrete mathematics, automata theory and differential equations.
Introduction to system theory.
Discrete systems and state machines (finite and infinite state machines).
Deterministic, observable and nondeterministic finite state machines.
Composition of finite state machines.
Minimization, determinization, equivalence and containment of finite state machines.
Simulation and bisimulation relations for finite state machines.
Sinthesis of finite state controllers for safety and liveness properties.
Supervisory control for regular automata and languages.
Languages for hardware specification.
|Edward Lee, Sanjit Seshia||Introduction to Embedded Systems - A Cyber-Physical Systems Approach (Edizione 1)||Lulu.com||2011||978-0-557-70857-4|
|Angela Di Febbraro, Alessandro Giua||Sistemi ad Eventi Discreti||MvGraw-Hill||2002||88-386-0863-6|